From b7f83bfed25314fc48a749b586abe06271979b4b Mon Sep 17 00:00:00 2001 From: Lukas Plevac Date: Sat, 16 Nov 2024 21:06:27 +0100 Subject: [PATCH] Init --- MTCodes/CMakeLists.txt | 11 + MTCodes/generate.cpp | 26 ++ MTCodes/passAig.cpp | 17 ++ MTCodes/passMig.cpp | 34 +++ MTCodes/resubstitution.cpp | 33 +++ MTCodes/rewriting.cpp | 31 +++ formal.ys | 4 + setup.sh | 18 ++ test.py | 510 +++++++++++++++++++++++++++++++++++++ toAig.ys | 8 + yosys_equiv_check.sh | 200 +++++++++++++++ 11 files changed, 892 insertions(+) create mode 100644 MTCodes/CMakeLists.txt create mode 100644 MTCodes/generate.cpp create mode 100644 MTCodes/passAig.cpp create mode 100644 MTCodes/passMig.cpp create mode 100644 MTCodes/resubstitution.cpp create mode 100644 MTCodes/rewriting.cpp create mode 100644 formal.ys create mode 100644 setup.sh create mode 100644 test.py create mode 100644 toAig.ys create mode 100644 yosys_equiv_check.sh diff --git a/MTCodes/CMakeLists.txt b/MTCodes/CMakeLists.txt new file mode 100644 index 0000000..08d2b9a --- /dev/null +++ b/MTCodes/CMakeLists.txt @@ -0,0 +1,11 @@ +file(GLOB FILENAMES *.cpp) + +foreach(filename ${FILENAMES}) + get_filename_component(basename ${filename} NAME_WE) + add_executable(${basename} ${filename}) + target_link_libraries(${basename} PUBLIC mockturtle) + + if(EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${basename}.cmake") + include(${basename}.cmake) + endif() +endforeach() diff --git a/MTCodes/generate.cpp b/MTCodes/generate.cpp new file mode 100644 index 0000000..c494d55 --- /dev/null +++ b/MTCodes/generate.cpp @@ -0,0 +1,26 @@ +#include +#include + +int main() { + mockturtle::mig_network mig; + + std::vector> a; + std::vector> b; + + for (unsigned i = 0; i < 8; i++) { + a.push_back(mig.create_pi()); + b.push_back(mig.create_pi()); + } + + auto out = mockturtle::carry_ripple_multiplier(mig, a, b); + + for (unsigned i = 0; i < out.size(); i++) { + mig.create_po(out[i]); + } + + // output + mockturtle::write_verilog(mig, "mig.v"); + + return 0; +} + diff --git a/MTCodes/passAig.cpp b/MTCodes/passAig.cpp new file mode 100644 index 0000000..6d2230d --- /dev/null +++ b/MTCodes/passAig.cpp @@ -0,0 +1,17 @@ +#include +#include + +int main() { + mockturtle::mig_network mig; + + auto const result = lorina::read_aiger("aig.aig", mockturtle::aiger_reader(mig) ); + if ( result != lorina::return_code::success ) { + std::cout << "Read AIG failed\n"; + return -1; + } + + // output + mockturtle::write_verilog(mig, "mig.v"); + + return 0; +} \ No newline at end of file diff --git a/MTCodes/passMig.cpp b/MTCodes/passMig.cpp new file mode 100644 index 0000000..a32b4da --- /dev/null +++ b/MTCodes/passMig.cpp @@ -0,0 +1,34 @@ +#include +#include +#include +#include +#include +#include +#include + +class diagnostics : public lorina::diagnostic_consumer +{ + public: + void handle_diagnostic( lorina::diagnostic_level level, std::string const& message ) const override { + printf("[%d] %s\n", int(level), message.c_str()); + } +}; /* diagnostics */ + + +int main() { + mockturtle::mig_network mig; + + diagnostics consumer; + lorina::diagnostic_engine diag( &consumer ); + + auto const result = lorina::read_verilog("adder.v", mockturtle::verilog_reader(mig), &diag); + if ( result != lorina::return_code::success ) { + std::cout << "Read Verilog failed " << int(result) << "\n"; + return 1; + } + + // output + mockturtle::write_verilog(mig, "mig.v"); + + return 0; +} \ No newline at end of file diff --git a/MTCodes/resubstitution.cpp b/MTCodes/resubstitution.cpp new file mode 100644 index 0000000..38995d7 --- /dev/null +++ b/MTCodes/resubstitution.cpp @@ -0,0 +1,33 @@ +#include +#include + +int main() { + mockturtle::mig_network mig; + + auto const result = lorina::read_aiger("aig.aig", mockturtle::aiger_reader(mig) ); + if ( result != lorina::return_code::success ) { + std::cout << "Read AIG failed\n"; + return -1; + } + + //apply rewriring + //mockturtle::mig_algebraic_depth_rewriting(mig); + + mockturtle::resubstitution_params ps; + mockturtle::resubstitution_stats st; + + ps.max_pis = 8u; + ps.max_inserts = 1u; + ps.progress = false; + + mockturtle::depth_view depth_mig{ mig }; + mockturtle::fanout_view fanout_mig{ depth_mig }; + + mockturtle::mig_resubstitution( fanout_mig, ps, &st ); + mig = mockturtle::cleanup_dangling( mig ); + + // output + mockturtle::write_verilog(mig, "mig.v"); + + return 0; +} \ No newline at end of file diff --git a/MTCodes/rewriting.cpp b/MTCodes/rewriting.cpp new file mode 100644 index 0000000..7c5fa07 --- /dev/null +++ b/MTCodes/rewriting.cpp @@ -0,0 +1,31 @@ +#include +#include + +int main() { + mockturtle::mig_network mig; + + auto const result = lorina::read_aiger("aig.aig", mockturtle::aiger_reader(mig) ); + if ( result != lorina::return_code::success ) { + std::cout << "Read AIG failed\n"; + return -1; + } + + //apply rewriring + //mockturtle::mig_algebraic_depth_rewriting(mig); + + mockturtle::mig_algebraic_depth_rewriting_params rp; + + //rp.strategy = mockturtle::mig_algebraic_depth_rewriting_params::aggressive; + //rp.overhead = 1.5; + + mockturtle::depth_view depth_mig{ mig }; + mockturtle::fanout_view fanout_mig{ depth_mig }; + + mockturtle::mig_algebraic_depth_rewriting(fanout_mig, rp); + mig = mockturtle::cleanup_dangling( mig ); + + // output + mockturtle::write_verilog(mig, "mig.v"); + + return 0; +} \ No newline at end of file diff --git a/formal.ys b/formal.ys new file mode 100644 index 0000000..94d5522 --- /dev/null +++ b/formal.ys @@ -0,0 +1,4 @@ +read_verilog mig.v +hierarchy +proc; opt; memory; opt; techmap; opt +write_blif formal.blif \ No newline at end of file diff --git a/setup.sh b/setup.sh new file mode 100644 index 0000000..1404df0 --- /dev/null +++ b/setup.sh @@ -0,0 +1,18 @@ +git clone https://github.com/ehw-fit/ariths-gen +git clone https://github.com/Lukas0025/ariths-gen-mig +git clone https://github.com/lsils/mockturtle + +rm -rf mockturtle/examples/* +cp MTCodes/* mockturtle/examples/ +cd mockturtle +mkdir build +cd build +cmake .. +make +cd ../.. + +python3 test.py + +rm -rf ariths-gen +rm -rf ariths-gen-mig +rm -rf mockturtle \ No newline at end of file diff --git a/test.py b/test.py new file mode 100644 index 0000000..40fa340 --- /dev/null +++ b/test.py @@ -0,0 +1,510 @@ +#!/usr/bin/env python +# coding: utf-8 + +import pyverilog +from pyverilog.dataflow.dataflow_analyzer import VerilogDataflowAnalyzer + +import graphviz +import networkx as nx +import os +import numpy as np + +def toOrientedGraph(nodes): + tmp = [] + for node in nodes.values(): + for ins in node.getIns(): + opts = {'style': 'solid'} + + if ins["inv"]: + opts['style'] = 'dashed' + + tmp.append( + ( + ins["node"], + node.getName(), + opts + ) + ) + return tmp + +depthBuffer = {} + +def getSubDelay(node, nodes, depth): + global depthBuffer + + if str(node.getName()) in depthBuffer: + return depthBuffer[str(node.getName())] + + maxLen = 0 + if depth >= 100: + maxLen = np.inf + else: + for ins in node.getIns(): + subLen = getSubDelay(nodes[str(ins["node"])], nodes, depth + 1) + if subLen > maxLen: + maxLen = subLen + + depthBuffer[str(node.getName())] = maxLen + 1 + + return maxLen + 1 + +def getDelay(nodes): + global depthBuffer + + depthBuffer.clear() # clear deph buffer + + maxLen = 0 + for node in nodes.values(): + if node.isOutput(): + subLen = getSubDelay(node, nodes, 0) + if subLen > maxLen: + maxLen = subLen + return maxLen - 2 # exclude input and output node + +def countGates(nodes): + count = 0 + for node in nodes.values(): + if node.tree is not None and node.tree.__class__.__name__ == "DFOperator": + count += 1 + return count + +class node: + def __init__(self, name, types): + self.name = name + self.types = types + self.tree = None + self.ins = [] + + # ((a >> 0) & 0x01) & ((b >> 0) & 0x01)) | (((b >> 0) & 0x01) & (0x01)) | (((a >> 0) & 0x01) & (0x01)) + def addMajiIn(self, tree, pos1, pos2, pos3): + a = None + aInv = False + + if not(str(tree) == "Or" and str(tree.nextnodes[0]) == "Or" and str(tree.nextnodes[1]) == "And" and str(tree.nextnodes[0].nextnodes[0]) == "And" and str(tree.nextnodes[0].nextnodes[1]) == "And"): + return a, aInv + + if tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3].__class__.__name__ == "DFOperator": # is classic input + if tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3].operator == "Unot": + if tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3].nextnodes[0].__class__.__name__ == "DFIntConst": # is constant + a = str(tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3].nextnodes[0]) + else: + a = tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3].nextnodes[0].nextnodes[0].nextnodes[0].name + aInv = True + else: + a = tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3].nextnodes[0].nextnodes[0].name + elif tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3].__class__.__name__ == "DFIntConst": # is constant + a = str(tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3]) + else: + return None, False + + return a, aInv + + # ( ~x0 & n18 ) | ( ~x0 & n19 ) | ( n18 & n19 ) + def addMTMaji(self, tree, pos1, pos2, pos3): + a = None + aInv = False + + if not(str(tree) == "Or" and str(tree.nextnodes[0]) == "Or" and str(tree.nextnodes[1]) == "And" and str(tree.nextnodes[0].nextnodes[0]) == "And" and str(tree.nextnodes[0].nextnodes[1]) == "And"): + return a, aInv + + if tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3].__class__.__name__ == "DFOperator": # is classic input + if tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3].operator == "Unot": + a = str(tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3].nextnodes[0]) + aInv = True + else: + return None, False + else: + a = str(tree.nextnodes[pos1].nextnodes[pos2].nextnodes[pos3]) + + return a, aInv + + def parseMaji(self, tree): + if tree.__class__.__name__ == "DFOperator": + a, aInv, b, bInv, c, cInv = None, None, None, None, None, None + + try: + a, aInv = self.addMajiIn(tree, 0, 0, 0) + b, bInv = self.addMajiIn(tree, 0, 0, 1) + c, cInv = self.addMajiIn(tree, 0, 1, 1) + except: + a, aInv, b, bInv, c, cInv = None, None, None, None, None, None + + try: + if a is None or b is None or c is None: + a, aInv = self.addMTMaji(tree, 0, 0, 0) + b, bInv = self.addMTMaji(tree, 0, 0, 1) + c, cInv = self.addMTMaji(tree, 0, 1, 1) + except: + a, aInv, b, bInv, c, cInv = None, None, None, None, None, None + + if a is None or b is None or c is None: + self.addInFromTree(tree, False) + else: + self.addIn(a, aInv) + self.addIn(b, bInv) + self.addIn(c, cInv) + else: + self.addInFromTree(tree, False) + + def addInFromTree(self, tree, invert = False): + if tree.__class__.__name__ == "DFOperator": + for node in tree.nextnodes: + self.addInFromTree(node, invert) + elif tree.__class__.__name__ == "DFIntConst": + self.addIn(str(tree), invert) + else: + self.addIn(tree.name, invert) + + def isInput(self): + return "Input" in self.types + + def isOutput(self): + return "Output" in self.types + + def getIns(self): + return self.ins + + def getName(self): + return self.name + + def addIn(self, name, invert = False): + self.ins.append({ + "node": name, + "inv": invert + }) + +def getNodes(file, top = "top"): + nodes = {} + + nodes['0'] = node('0', {"Input"}) + nodes['1'] = node('1', {"Input"}) + + + analyzer = VerilogDataflowAnalyzer([file], top) + analyzer.generate() + + # First create nodes + terms = analyzer.getTerms() + for tk, tv in sorted(terms.items(), key=lambda x: str(x[0])): + nodes[str(tv.name)] = node(tv.name, tv.termtype) + + # Create connections between nodes + binddict = analyzer.getBinddict() + for bk, bv in sorted(binddict.items(), key=lambda x: str(x[0])): + for bvi in bv: + nodes[str(bvi.dest)].parseMaji(bvi.tree) + nodes[str(bvi.dest)].tree = bvi.tree + + return nodes + +def plotNodes(nodes, name): + # create a directed multi-graph + G = nx.MultiDiGraph() + G.add_edges_from(toOrientedGraph(nodes)) + # plot the graph + a = nx.nx_agraph.to_agraph(G) + src = graphviz.Source(a.to_string()) + src.render(name) + +def generateAg(name): + return """from io import StringIO +import os, sys + +DIR_PATH = os.path.dirname(os.path.abspath(__file__)) +sys.path.insert(0, os.path.join(DIR_PATH, '..')) + +from ariths_gen.core.arithmetic_circuits import GeneralCircuit +from ariths_gen.multi_bit_circuits.adders import UnsignedRippleCarryAdder, UnsignedCarryLookaheadAdder, UnsignedBrentKungAdder, UnsignedCarryIncrementAdder, UnsignedCarrySkipAdder, UnsignedCarrySelectAdder, UnsignedConditionalSumAdder, UnsignedHanCarlsonAdder, UnsignedKnowlesAdder, UnsignedKoggeStoneAdder, UnsignedLadnerFischerAdder, UnsignedPGRippleCarryAdder, UnsignedSklanskyAdder +from ariths_gen.multi_bit_circuits.multipliers import UnsignedArrayMultiplier, UnsignedCarrySaveMultiplier, UnsignedDaddaMultiplier, UnsignedWallaceMultiplier +from ariths_gen.wire_components import Bus + +from ariths_gen.pdk import * +import os + +if __name__ == "__main__": + uut = """ + name + """ + maji = uut(Bus("a", 8), Bus("b", 8), prefix="", name="top") + + maji.get_v_code_flat(open("mig.v", "w")) +""" + +def generateMT(name, outputA = True): + if outputA: + return """#include +#include + +int main() { + mockturtle::mig_network mig; + + std::vector> a; + std::vector> b; + auto cin = mig.get_constant(false); + + for (unsigned i = 0; i < 8; i++) { + a.push_back(mig.create_pi()); + b.push_back(mig.create_pi()); + } + + mockturtle::""" + name + """(mig, a, b, cin); + + auto out = a; + + for (unsigned i = 0; i < out.size(); i++) { + mig.create_po(out[i]); + } + + // output + mockturtle::write_verilog(mig, "mig.v"); + + return 0; +} +""" + else: + return """#include +#include + +int main() { + mockturtle::mig_network mig; + + std::vector> a; + std::vector> b; + + for (unsigned i = 0; i < 8; i++) { + a.push_back(mig.create_pi()); + b.push_back(mig.create_pi()); + } + + auto out = mockturtle::""" + name + """(mig, a, b); + + for (unsigned i = 0; i < out.size(); i++) { + mig.create_po(out[i]); + } + + // output + mockturtle::write_verilog(mig, "mig.v"); + + return 0; +} +""" + +# https://mockturtle.readthedocs.io/en/latest/generators/arithmetic.html#addition-and-subtraction +circs = [ + # ADDRS + { + "name": "UnsignedRippleCarryAdder", + "ag": "UnsignedRippleCarryAdder", + "mt": "carry_ripple_adder_inplace", + "mtAOut": True + }, + { + "name": "UnsignedCarryLookaheadAdder", + "ag": "UnsignedCarryLookaheadAdder", + "mt": "carry_lookahead_adder_inplace", + "mtAOut": True + }, + { + "name": "UnsignedBrentKungAdder", + "ag": "UnsignedBrentKungAdder", + "mt": None + }, + { + "name": "UnsignedCarryIncrementAdder", + "ag": "UnsignedCarryIncrementAdder", + "mt": None + }, + { + "name": "UnsignedCarrySkipAdder", + "ag": "UnsignedCarrySkipAdder", + "mt": None + }, + { + "name": "UnsignedCarrySelectAdder", + "ag": "UnsignedCarrySelectAdder", + "mt": None + }, + { + "name": "UnsignedConditionalSumAdder", + "ag": "UnsignedConditionalSumAdder", + "mt": None + }, + { + "name": "UnsignedHanCarlsonAdder", + "ag": "UnsignedHanCarlsonAdder", + "mt": None + }, + { + "name": "UnsignedKnowlesAdder", + "ag": "UnsignedKnowlesAdder", + "mt": None + }, + { + "name": "UnsignedKoggeStoneAdder", + "ag": "UnsignedKoggeStoneAdder", + "mt": None + }, + { + "name": "UnsignedLadnerFischerAdder", + "ag": "UnsignedLadnerFischerAdder", + "mt": None + }, + { + "name": "UnsignedPGRippleCarryAdder", + "ag": "UnsignedPGRippleCarryAdder", + "mt": None + }, + { + "name": "UnsignedSklanskyAdder", + "ag": "UnsignedSklanskyAdder", + "mt": None + }, + # MULS + { + "name": "UnsignedArrayMultiplier", + "ag": "UnsignedArrayMultiplier", + "mt": "carry_ripple_multiplier", + "mtAOut": False + }, + { + "name": "UnsignedCarrySaveMultiplier", + "ag": "UnsignedCarrySaveMultiplier", + "mt": None + }, + { + "name": "UnsignedDaddaMultiplier", + "ag": "UnsignedDaddaMultiplier", + "mt": None + }, + { + "name": "UnsignedWallaceMultiplier", + "ag": "UnsignedWallaceMultiplier", + "mt": None + } +] + +# +# Begin main +# + +MT_PATH = "./mockturtle/" +AGM_PATH = "./ariths-gen-mig/" +AG_PATH = "./ariths-gen/" +PWD = os.getcwd() + +table = open(f"{PWD}/compare.csv", "w") + +print("type;MT (GATES);MT (DELAY);ariths-gen->AIG->MT (GATES);ariths-gen->AIG->MT (DELAY);ariths-gen->AIG->MT+RESUBSTITUTION (GATES);ariths-gen->AIG->MT+RESUBSTITUTION (DELAY);ariths-gen-mig (GATES);ariths-gen-mig (DELAY);ariths-gen-mi->AIG->MT+RESUBSTITUTION (GATES);ariths-gen-mi->AIG->MT+RESUBSTITUTION (DELAY)", file=table) + +for circ in circs: + + MTDirectGates = "-" + MTDirectDelay = "-" + + ## MockTurtle direct generator + + if circ["mt"] is not None: + + with open(f"{MT_PATH}/examples/generate.cpp", "w") as Vfile: + print(generateMT(circ["mt"], circ["mtAOut"]), file=Vfile) + + os.system(f"cd {MT_PATH}/build/examples && make && ./generate && cp mig.v {PWD}/mig.v") + + # generate blif for verification + os.system(f"yosys formal.ys") + + os.system(f"mv formal.blif formalMT.blif && mv mig.v {circ['name']}_MT.v") + + nodes = getNodes(f"{circ['name']}_MT.v") + + MTDirectGates = countGates(nodes) + MTDirectDelay = getDelay(nodes) + + plotNodes(nodes, f"{circ['name']}_MT") + + ## ArithsGen + + with open(f"{AG_PATH}/generate.py", "w") as Vfile: + print(generateAg(circ["ag"]), file=Vfile) + + os.system(f"cd {AG_PATH} && python3 ./generate.py && cp mig.v {PWD}/mig.v") + + os.system(f"sed -i -e 's/0x00/0/g' mig.v && sed -i -e 's/0x01/1/g' mig.v") # 0x00 and 0x01 to 0 and 1 + + # generate blif for verification + os.system(f"yosys formal.ys") + + os.system(f"yosys toAig.ys") # yosys VERILOG to AIG + + os.system(f"./{MT_PATH}/build/examples/passAig") # aig.aig to mig.v + + os.system(f"mv mig.v {circ['name']}_AG.v") + + os.system(f"./{MT_PATH}/build/examples/resubstitution") # aig.aig to mig.v (resubstitution) + + os.system(f"mv mig.v {circ['name']}_AG_RE.v") + + nodes = getNodes(f"{circ['name']}_AG.v") + + print(f"Working on {circ['name']}_AG") + + AGDirectGates = countGates(nodes) + AGDirectDelay = getDelay(nodes) + + plotNodes(nodes, f"{circ['name']}_AG") + + nodes = getNodes(f"{circ['name']}_AG_RE.v") + + print(f"Working on {circ['name']}_AG_RE") + + AGREDirectGates = countGates(nodes) + AGREDirectDelay = getDelay(nodes) + + plotNodes(nodes, f"{circ['name']}_AG_RE") + + ## ArithsGenMig + + with open(f"{AGM_PATH}/generate.py", "w") as Vfile: + print(generateAg(circ["ag"]), file=Vfile) + + os.system(f"cd {AGM_PATH} && python3 ./generate.py && cp mig.v {PWD}/{circ['name']}_AGM.v") + + os.system(f"sed -i -e 's/0x00/0/g' {circ['name']}_AGM.v && sed -i -e 's/0x01/1/g' {circ['name']}_AGM.v") # 0x00 and 0x01 to 0 and 1 + + nodes = getNodes(f"{circ['name']}_AGM.v") + + print(f"Working on {circ['name']}_AGM") + + AGMDirectGates = countGates(nodes) + AGMDirectDelay = getDelay(nodes) + + plotNodes(nodes, f"{circ['name']}_AGM") + + os.system(f"cp {circ['name']}_AGM.v mig.v") + + os.system(f"yosys toAig.ys") # yosys VERILOG to AIG + + os.system(f"./{MT_PATH}/build/examples/resubstitution") # aig.aig to mig.v (resubstitution) + + os.system(f"mv mig.v {circ['name']}_AGM_RE.v") + + nodes = getNodes(f"{circ['name']}_AGM_RE.v") + + print(f"Working on {circ['name']}_AGM_RE") + + AGMREDirectGates = countGates(nodes) + AGMREDirectDelay = getDelay(nodes) + + plotNodes(nodes, f"{circ['name']}_AGM_RE") + + ec = os.system(f"bash yosys_equiv_check.sh -v {circ['name']}_AGM.v -b formal.blif -m sat") + if ec != 0: + print("Formal verification fail") + exit(1) + + print(f"{circ['name']};{MTDirectGates};{MTDirectDelay};{AGDirectGates};{AGDirectDelay};{AGREDirectGates};{AGREDirectDelay};{AGMDirectGates};{AGMDirectDelay};{AGMREDirectGates};{AGMREDirectDelay}", file=table) + +os.system("zip data.zip *.pdf *.v") +os.system("mkdir stash") +os.system("mv toAig.ys stash && mv test.py stash && mv compare.csv stash && mv setup.sh stash && mv data.zip stash && mv yosys_equiv_check.sh stash && mv formal.ys stash") +os.system("rm -f *") +os.system("mv stash/* . && rm -rf stash") +table.close() \ No newline at end of file diff --git a/toAig.ys b/toAig.ys new file mode 100644 index 0000000..5499421 --- /dev/null +++ b/toAig.ys @@ -0,0 +1,8 @@ +read_verilog mig.v +proc +opt +techmap +opt +abc +aigmap +write_aiger aig.aig \ No newline at end of file diff --git a/yosys_equiv_check.sh b/yosys_equiv_check.sh new file mode 100644 index 0000000..91520ba --- /dev/null +++ b/yosys_equiv_check.sh @@ -0,0 +1,200 @@ +#!/bin/bash + +# Script enables formal verification and equivalence of Verilog/BLIF circuit designs +# using Yosys Open SYnthesis Suite by Claire Xenia Wolf. +# For more information, please visit: http://bygone.clairexen.net/yosys/documentation.html + +# Echo script help +help () { + echo "–––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––" + echo "––– HELP –––" + echo "–––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––" + echo "– SCRIPT FOR CHECKING FORMAL EQUIVALENCE BETWEEN VERILOG AND BLIF DESIGNS USING YOSYS –" + echo + echo "Input files should have the same name used for corresponding file types filenames as well" + echo "as for their inner design's top module names." + echo "Formal verification and equivalence of Verilog/BLIF circuit designs achieved using Yosys" + echo "Open SYnthesis Suite." + echo "–––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––––" + echo "Input parameters:" + echo "-h, --help" + echo " help information" + echo "-v 'verilog_file', --verilog_file 'verilog_file'" + echo " specifies input Verilog design file" + echo "-b 'blif_file', --blif_file 'blif_file'" + echo " specifies input BLIF design file" + echo "-m 'method', --mode 'method'" + echo " specifies chosen formal equivalence method (sat|equiv)" + echo "-H, --hier" + echo " specifies whether designs are in hierarchical representation (default is flat)" +} + +# No input parameters present, echo help and exit. +if [[ "$#" -eq 0 ]]; then + help + exit 0 +fi + +# Defaultly flat designs are considered +HIERARCHICAL=false + +# Parsing and extraction of input parameters and their arguments into variables. +while [[ "$#" -gt 0 ]] ; do + case "$1" in + "-v" | "--verilog_file") + if [[ -f "$2" && "$2" == *.v ]]; then + VERILOG_FILE=$2 + else + echo "$2 is not a Verilog file!"; + exit 1 + fi + shift 2;; + + "-b" | "--blif_file") + if [[ -f "$2" && "$2" == *.blif ]]; then + BLIF_FILE="$2" + else + echo "$2 is not a BLIF file!"; + exit 1 + fi + shift 2;; + + "-m" | "--mode") + if [[ "$2" == "sat" || "$2" == "equiv" ]]; then + METHOD="$2" + else + echo "$2 is not a supported formal equivalence method!"; + echo + echo "Type -h | --help for more information." + exit 1 + fi + shift 2;; + + "-H" | "--hier") + HIERARCHICAL=true + shift 1;; + "-h" | "--help") + help + exit 0;; + *) + echo "Unknown input parameter $1!" + echo + echo "Type -h | --help for more information." + exit 1;; + esac +done + +# Check if both files compulsory parameters are set and if they have the same name. +# To proper equiv check both designs top modules must be of same names (assumption that filename == top module name) +if [[ -z "$VERILOG_FILE" || -z "$BLIF_FILE" || -z "$METHOD" ]]; then + [ -z "$VERILOG_FILE" ] && echo "Missing compulsory Verilog file for comparison!" + [ -z "$BLIF_FILE" ] && echo "Missing compulsory BLIF file for comparison!" + [ -z "$METHOD" ] && echo "Missing choice of formal equivalence method!" + echo + echo "Type -h | --help for more information." + exit 1 +fi + +TOP_MODULE="top" + + +# Formal verification with equiv_* for flat designs +if [ "$METHOD" = "equiv" ]; then + if [ "$HIERARCHICAL" = false ]; then + yosys -p " + # Gold design + read_verilog $VERILOG_FILE + prep -top $TOP_MODULE + splitnets -ports;; + design -stash gold + + # Gate design + read_blif $BLIF_FILE + prep -top $TOP_MODULE + design -stash gate + + # Prove equivalence + design -copy-from gold -as gold $TOP_MODULE + design -copy-from gate -as gate $TOP_MODULE + + equiv_make gold gate equiv + hierarchy -top equiv + equiv_simple + equiv_status -assert + " + # Formal verification with equiv_* for hierarchical designs + else + yosys -p " + # Gold design + read_verilog $VERILOG_FILE + prep -top $TOP_MODULE + flatten + splitnets -ports;; + design -stash gold + + # Gate design + read_blif $BLIF_FILE + prep -top $TOP_MODULE + flatten + splitnets -ports;; + design -stash gate + + # Prove equivalence + design -copy-from gold -as gold $TOP_MODULE + design -copy-from gate -as gate $TOP_MODULE + + equiv_make gold gate equiv + hierarchy -top equiv + equiv_simple + equiv_status -assert + " + fi +else + if [ "$HIERARCHICAL" = false ]; then + yosys -p " + # Gold design + read_verilog $VERILOG_FILE + prep -top $TOP_MODULE + splitnets -ports;; + design -stash gold + + # Gate design + read_blif $BLIF_FILE + prep -top $TOP_MODULE + design -stash gate + + # Prove equivalence + design -copy-from gold -as gold $TOP_MODULE + design -copy-from gate -as gate $TOP_MODULE + + miter -equiv -flatten gold gate miter + hierarchy -top miter + sat -verify -tempinduct -prove trigger 0 + " + # Formal verification with equiv_* for hierarchical designs + else + yosys -p " + # Gold design + read_verilog $VERILOG_FILE + prep -top $TOP_MODULE + flatten + splitnets -ports;; + design -stash gold + + # Gate design + read_blif $BLIF_FILE + prep -top $TOP_MODULE + flatten + splitnets -ports;; + design -stash gate + + # Prove equivalence + design -copy-from gold -as gold $TOP_MODULE + design -copy-from gate -as gate $TOP_MODULE + + miter -equiv -flatten gold gate miter + hierarchy -top miter + sat -verify -tempinduct -prove trigger 0 + " + fi +fi