Init

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()

MTCodes/generate.cpp

@@ -0,0 +1,26 @@
+#include <lorina/aiger.hpp>
+#include <mockturtle/mockturtle.hpp>
+
+int main() {
+  mockturtle::mig_network mig;
+
+  std::vector<mockturtle::signal<mockturtle::mig_network>> a;
+  std::vector<mockturtle::signal<mockturtle::mig_network>> 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;
+}
+

MTCodes/passAig.cpp

@@ -0,0 +1,17 @@
+#include <lorina/aiger.hpp>
+#include <mockturtle/mockturtle.hpp>
+
+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;
+}

MTCodes/passMig.cpp

@@ -0,0 +1,34 @@
+#include <lorina/aiger.hpp>
+#include <lorina/bench.hpp>
+#include <lorina/blif.hpp>
+#include <lorina/pla.hpp>
+#include <lorina/verilog.hpp>
+#include <mockturtle/mockturtle.hpp>
+#include <lorina/diagnostics.hpp>
+
+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;
+}

MTCodes/resubstitution.cpp

@@ -0,0 +1,33 @@
+#include <lorina/aiger.hpp>
+#include <mockturtle/mockturtle.hpp>
+
+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;
+}

MTCodes/rewriting.cpp

@@ -0,0 +1,31 @@
+#include <lorina/aiger.hpp>
+#include <mockturtle/mockturtle.hpp>
+
+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;
+}

formal.ys

@@ -0,0 +1,4 @@
+read_verilog mig.v
+hierarchy
+proc; opt; memory; opt; techmap; opt
+write_blif formal.blif

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

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 <lorina/aiger.hpp>
+#include <mockturtle/mockturtle.hpp>
+
+int main() {
+  mockturtle::mig_network mig;
+
+  std::vector<mockturtle::signal<mockturtle::mig_network>> a;
+  std::vector<mockturtle::signal<mockturtle::mig_network>> 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 <lorina/aiger.hpp>
+#include <mockturtle/mockturtle.hpp>
+
+int main() {
+  mockturtle::mig_network mig;
+
+  std::vector<mockturtle::signal<mockturtle::mig_network>> a;
+  std::vector<mockturtle::signal<mockturtle::mig_network>> 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()

toAig.ys

@@ -0,0 +1,8 @@
+read_verilog mig.v
+proc
+opt
+techmap
+opt
+abc
+aigmap
+write_aiger aig.aig

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