Formal verifier supported algebra operator (but it has trial verision yet.)

Author: fukatani

pyverilog_toolbox/testcode/fv_test.v

@@ -1,6 +1,6 @@
 module TOP(CLK);
   input CLK;
-  reg A,B,C,D,E,F,G;
+  reg A,B,C,D,E,F,G,H;
   reg [2:0] multi;
 
   always @(posedge CLK) begin
@@ -26,6 +26,9 @@ module TOP(CLK);
   always @(posedge CLK) begin
     G <= &multi[1:0];
   end
+  always @(posedge CLK) begin
+    H <= F+G;
+  end
 
 endmodule
 

pyverilog_toolbox/testcode/test_ra.py

@@ -173,8 +173,7 @@ def test_comb_loop4(self):
     def test_formal_verifier(self):
         if sys.version_info[0] == 2:
             fv = FormalVerifier("../testcode/fv_test.v")
-            t_table = fv.calc_truth_table('TOP.G')
-            fv.write_back_DFmethods()
+            t_table = fv._calc_truth_table('TOP.G')
             self.assertEqual(t_table["['TOP_multi__0__: False', 'TOP_multi__1__: False', 'TOP_multi__2__: False']"],
                              False)
             self.assertEqual(t_table["['TOP_multi__0__: False', 'TOP_multi__1__: False', 'TOP_multi__2__: True']"],
@@ -191,6 +190,9 @@ def test_formal_verifier(self):
                              True)
             self.assertEqual(t_table["['TOP_multi__0__: True', 'TOP_multi__1__: True', 'TOP_multi__2__: True']"],
                              True)
+            t_table = fv.calc_truth_table('TOP.H')
+            self.assertEqual(str(t_table["['TOP_F: False', 'TOP_G: False']"]),
+                             "TOP_F_ + TOP_G_")
 
 if __name__ == '__main__':
     unittest.main()

pyverilog_toolbox/verify_tool/formal_verifier.py

@@ -25,26 +25,35 @@ class FormalVerifier(dataflow_facade):
 
     def __init__(self, code_file_name, topmodule=''):
         dataflow_facade.__init__(self, code_file_name, topmodule=topmodule)
+        t_manager = term_manager()
+        t_manager.set_scope_dict(self.binds.scope_dict)
+        t_manager.set_terms(self.binds._terms)
 
         DFBranch.tocode_org = MethodType(DFBranch.tocode, None, DFBranch)
-        DFBranch.tocode = MethodType(DFBranch_tocode_for_sympy, None, DFBranch)
+        DFBranch.tocode = MethodType(DFBranch_tocode, None, DFBranch)
         DFOperator.tocode_org = MethodType(DFOperator.tocode, None, DFOperator)
-        DFOperator.tocode = MethodType(DFOperator_tocode_for_sympy, None, DFOperator)
+        DFOperator.tocode = MethodType(DFOperator_tocode, None, DFOperator)
         DFOperator.is_reduction = MethodType(DFOperator_is_reduction, None, DFOperator)
-        DFTerminal.scope_dict = self.binds.scope_dict
-        DFTerminal.terms = self.binds._terms
-        DFTerminal.get_bind = MethodType(DFTerminal_get_terms, None, DFTerminal)
+        DFOperator.is_algebra = MethodType(DFOperator_is_algebra, None, DFOperator)
+        DFTerminal.tocode_org = MethodType(DFTerminal.tocode, None, DFTerminal)
+        DFTerminal.tocode = MethodType(DFTerminal_tocode, None, DFTerminal)
 
     def write_back_DFmethods(self):
+        DFTerminal.tocode = MethodType(DFTerminal.tocode_org, None, DFTerminal)
         DFBranch.tocode = MethodType(DFBranch.tocode_org, None, DFBranch)
         DFOperator.tocode = MethodType(DFOperator.tocode_org, None, DFOperator)
         del DFOperator.tocode_org
         del DFOperator.is_reduction
-        del DFTerminal.scope_dict
-        del DFTerminal.terms
-        del DFTerminal.get_bind
+        del DFOperator.is_algebra
 
     def calc_truth_table(self, var_name):
+        try:
+            truth_table = self._calc_truth_table(var_name)
+        finally:
+            self.write_back_DFmethods()
+        return truth_table
+
+    def _calc_truth_table(self, var_name):
         """[FUNCTIONS]
         """
         for tv, tk, bvi, bit, term_lsb in self.binds.walk_reg_each_bit():
@@ -64,12 +73,22 @@ def calc_truth_table(self, var_name):
                     ns[symbol_name] = Symbol(symbol_name)
                 else:
                     for i in range(lsb, msb + 1):
-                        symbol_name_bit = get_bus_name(symbol_name, i)
+                        symbol_name_bit = term_manager().publish_new_name(symbol_name, i)
                         ns[symbol_name_bit] = Symbol(symbol_name_bit)
 
+            term_manager().flash_renamed_signals()
             f = self.to_sympy_expr(target_tree.tocode())
+            for signal in term_manager().renamed_signals:
+                signal = signal.replace('.','_')
+                ns[signal] = Symbol(signal)
+
+            #TODO delete renamed signals
             expr = sympify(f, ns, convert_xor=False)
 
+            for signal in term_manager().renamed_signals:
+                signal = signal.replace('.','_')
+                ns.pop(signal)
+
             truth_table = {}
             for result, var_state in self.walk_truth_table(ns, expr):
                 truth_table[str(var_state)] = result
@@ -111,7 +130,7 @@ def to_sympy_expr(self, expr):
             expr = expr.replace(comb[0], comb[1])
         return expr
 
-def DFBranch_tocode_for_sympy(self, dest='dest', always=''):
+def DFBranch_tocode(self, dest='dest', always=''):
     ret = '('
     if self.condnode is not None: ret += '(' + self.condnode.tocode(dest) + ')'
     ret += '& '
@@ -131,35 +150,86 @@ def DFOperator_is_reduction(self):
     else:
         return False
 
-def DFOperator_tocode_for_sympy(self):
-    if not self.is_reduction():
-        return self.tocode_org()
+def DFOperator_is_algebra(self):
+    if self.operator in ('Plus', 'Minus', 'LessThan', 'GreaterThan', 'LessEq', 'GreaterEq'):
+        return True
+    else:
+        return False
+
+def DFTerminal_tocode(self, dest='dest'):
+    if term_manager().is_under_algebra:
+        return term_manager().publish_new_name(str(self)).replace('.','_')
     else:
-        if isinstance(self.nextnodes[0], DFPartselect):  #TODO
+        return self.tocode_org()
+
+def DFOperator_tocode(self):
+    if self.is_algebra():  #if operator is algebra, nextnodes aren't sweeped.
+        term_manager().set_is_under_algebra(True)
+        code = self.tocode_org()
+        term_manager().set_is_under_algebra(False)
+        return code
+    elif self.is_reduction():
+        if isinstance(self.nextnodes[0], DFPartselect):
             term = self.nextnodes[0].var
             msb = eval_value(self.nextnodes[0].msb)
             lsb = eval_value(self.nextnodes[0].lsb)
         elif isinstance(self.nextnodes[0], DFTerminal):
-            term = self.nextnodes[0].get_bind()
+            term = term_manager().get_term(str(self.nextnodes[0]))
             msb = eval_value(term.msb)
             lsb = eval_value(term.lsb)
         else:
             raise Exception('Unexpected exception.')
         mark = op2mark.op2mark(self.operator)
-        return mark.join([get_bus_name(term, i).replace('.', '_') for i in range(lsb, msb + 1)])
+        return mark.join([term_manager().publish_new_name(str(term), i).replace('.', '_') for i in range(lsb, msb + 1)])
+    else:
+        return self.tocode_org()
+
+class term_manager(object):
+    """ [CLASSES]
+        Singleton class for manage terminals for DFxxx.
+    """
+    _singleton = None
+    def __new__(cls, *argc, **argv):
+        if cls._singleton == None:
+            cls._singleton = object.__new__(cls)
+            cls.is_under_algebra = False
+            cls.exclude_signals = []
+            cls.renamed_signals = []
+        return cls._singleton
+
+    def set_scope_dict(self, scope_dict):
+        self.scope_dict = scope_dict
+
+    def set_terms(self, terms):
+        self.terms = terms
+
+    def get_term(self, signal):
+        scope = self.scope_dict[signal]
+        return self.terms[scope]
+
+    def set_is_under_algebra(self, flag=False):
+        self.is_under_algebra = flag
+
+    def publish_new_name(self, signal, bit=None):
+        if bit is None:
+            new_name = signal + '_'
+        else:
+            new_name = signal + '__' + str(bit) + '__'
+        while(new_name in self.scope_dict.keys()):
+            new_name += '_'
+        if bit is None:
+            self.renamed_signals.append(new_name)
+        return new_name
 
-def DFTerminal_get_terms(self):
-    scope = DFTerminal.scope_dict[str(self)]
-    return DFTerminal.terms[scope]
+    def flash_renamed_signals(self):
+        self.renamed_signals = []
 
-def get_bus_name(signal, bit):
-    return str(signal) + '__' + str(bit) + '__'
+    def flash_exclude_signals(self):
+        self.exclude_signals = []
 
 if __name__ == '__main__':
     fv = FormalVerifier("../testcode/fv_test.v")
     #fv.calc_truth_table('TOP.A')
     #fv.calc_truth_table('TOP.C')
     #fv.calc_truth_table('TOP.E')
-    a=fv.calc_truth_table('TOP.G')
-    fv.write_back_DFmethods()
-    pass
+    fv.calc_truth_table('TOP.H')