|
| 1 | +#------------------------------------------------------------------------------- |
| 2 | +# formal_verifier.py |
| 3 | +# |
| 4 | +# |
| 5 | +# Copyright (C) 2015, Ryosuke Fukatani |
| 6 | +# License: Apache 2.0 |
| 7 | +#------------------------------------------------------------------------------- |
| 8 | + |
| 9 | +import sys |
| 10 | +import os |
| 11 | + |
| 12 | +sys.path.insert(0, os.path.dirname(os.path.dirname(os.path.dirname(os.path.abspath(__file__))))) |
| 13 | + |
| 14 | +from pyverilog.utils.util import * |
| 15 | +from pyverilog.dataflow.dataflow import * |
| 16 | +from pyverilog_toolbox.verify_tool.dataflow_facade import * |
| 17 | +from pyverilog_toolbox.verify_tool.bindlibrary import * |
| 18 | +from sympy import * |
| 19 | +from types import MethodType |
| 20 | + |
| 21 | +import pyverilog.controlflow.splitter as splitter |
| 22 | +import pyverilog.utils.op2mark as op2mark |
| 23 | + |
| 24 | +class FormalVerifier(dataflow_facade): |
| 25 | + |
| 26 | + def __init__(self, code_file_name, topmodule=''): |
| 27 | + dataflow_facade.__init__(self, code_file_name, topmodule=topmodule) |
| 28 | + |
| 29 | + DFBranch.tocode_org = MethodType(DFBranch.tocode, None, DFBranch) |
| 30 | + DFBranch.tocode = MethodType(DFBranch_tocode_for_sympy, None, DFBranch) |
| 31 | + DFOperator.tocode_org = MethodType(DFOperator.tocode, None, DFOperator) |
| 32 | + DFOperator.tocode = MethodType(DFOperator_tocode_for_sympy, None, DFOperator) |
| 33 | + DFOperator.is_reduction = MethodType(DFOperator_is_reduction, None, DFOperator) |
| 34 | + DFTerminal.scope_dict = self.binds.scope_dict |
| 35 | + DFTerminal.terms = self.binds._terms |
| 36 | + DFTerminal.get_bind = MethodType(DFTerminal_get_terms, None, DFTerminal) |
| 37 | + |
| 38 | + def write_back_DFmethods(self): |
| 39 | + DFBranch.tocode = MethodType(DFBranch.tocode_org, None, DFBranch) |
| 40 | + DFOperator.tocode = MethodType(DFOperator.tocode_org, None, DFOperator) |
| 41 | + del DFOperator.tocode_org |
| 42 | + del DFOperator.is_reduction |
| 43 | + del DFTerminal.scope_dict |
| 44 | + del DFTerminal.terms |
| 45 | + del DFTerminal.get_bind |
| 46 | + |
| 47 | + def calc_truth_table(self, var_name): |
| 48 | + """[FUNCTIONS] |
| 49 | + """ |
| 50 | + for tv, tk, bvi, bit, term_lsb in self.binds.walk_reg_each_bit(): |
| 51 | + target_tree = self.makeTree(tk) |
| 52 | + if str(tk) != var_name: continue |
| 53 | + trees = self.binds.extract_all_dfxxx(target_tree, set([]), 0, DFTerminal) |
| 54 | + tree_names = [str(tree[0]) for tree in trees] |
| 55 | + |
| 56 | + ns = {} |
| 57 | + for tree in tree_names: |
| 58 | + symbol_name = tree.replace('.','_') |
| 59 | + scope = self.binds.scope_dict[tree] |
| 60 | + term = self.terms[scope] |
| 61 | + msb = eval_value(term.msb) |
| 62 | + lsb = eval_value(term.lsb) |
| 63 | + if msb == lsb: |
| 64 | + ns[symbol_name] = Symbol(symbol_name) |
| 65 | + else: |
| 66 | + for i in range(lsb, msb + 1): |
| 67 | + symbol_name_bit = get_bus_name(symbol_name, i) |
| 68 | + ns[symbol_name_bit] = Symbol(symbol_name_bit) |
| 69 | + |
| 70 | + f = self.to_sympy_expr(target_tree.tocode()) |
| 71 | + expr = sympify(f, ns, convert_xor=False) |
| 72 | + |
| 73 | + truth_table = {} |
| 74 | + for result, var_state in self.walk_truth_table(ns, expr): |
| 75 | + truth_table[str(var_state)] = result |
| 76 | + print('result:' + str(result) + '@' + str(var_state)) |
| 77 | + return truth_table |
| 78 | + |
| 79 | + def walk_truth_table(self, ns, expr): |
| 80 | + init_expr = expr |
| 81 | + for cnt in range(0, 2 ** len(ns.keys())): |
| 82 | + expr = init_expr |
| 83 | + var_state = [] |
| 84 | + for i, var in enumerate(sorted(ns.keys() ,key=lambda t:str(t))): |
| 85 | + value = (format(cnt, 'b').zfill(len(ns.keys()))[i]) == '1' |
| 86 | + var_state.append(var + ': ' + str(value)) |
| 87 | + expr = expr.subs(var, value) |
| 88 | + yield expr, var_state |
| 89 | + |
| 90 | + def to_sympy_expr(self, expr): |
| 91 | + """ [FUNCTIONS] |
| 92 | + verilog operators |
| 93 | + [] : implemented (convert [i] to __i__) |
| 94 | + ! ~ : implemented |
| 95 | + * / % : unsupported |
| 96 | + + - |
| 97 | + << >> |
| 98 | + == != : implemented |
| 99 | + < <= > => |
| 100 | + & : implemented |
| 101 | + ^ ^~ : implemented |
| 102 | + | : implemented |
| 103 | + && : implemented |
| 104 | + || : implemented |
| 105 | + ? : implemented |
| 106 | + reduction : implemented |
| 107 | + """ |
| 108 | + replace_words = (('!', '~'), ('||', '|'), ('&&', '&'), ('==','^~'), |
| 109 | + ('!=', '^'), ) |
| 110 | + for comb in replace_words: |
| 111 | + expr = expr.replace(comb[0], comb[1]) |
| 112 | + return expr |
| 113 | + |
| 114 | +def DFBranch_tocode_for_sympy(self, dest='dest', always=''): |
| 115 | + ret = '(' |
| 116 | + if self.condnode is not None: ret += '(' + self.condnode.tocode(dest) + ')' |
| 117 | + ret += '& ' |
| 118 | + if self.truenode is not None: ret += self.truenode.tocode(dest) |
| 119 | + else: ret += dest |
| 120 | + ret += " | " |
| 121 | + if self.falsenode is not None: |
| 122 | + ret += '(~' + self.condnode.tocode(dest) + '&' |
| 123 | + ret += self.falsenode.tocode(dest) + ')' |
| 124 | + else: ret += dest |
| 125 | + ret += ")" |
| 126 | + return ret |
| 127 | + |
| 128 | +def DFOperator_is_reduction(self): |
| 129 | + if self.operator in ('Uand', 'Uor', 'Uxor', 'Uxnor'): |
| 130 | + return len(self.nextnodes) == 1 |
| 131 | + else: |
| 132 | + return False |
| 133 | + |
| 134 | +def DFOperator_tocode_for_sympy(self): |
| 135 | + if not self.is_reduction(): |
| 136 | + return self.tocode_org() |
| 137 | + else: |
| 138 | + if isinstance(self.nextnodes[0], DFPartselect): #TODO |
| 139 | + term = self.nextnodes[0].var |
| 140 | + msb = eval_value(self.nextnodes[0].msb) |
| 141 | + lsb = eval_value(self.nextnodes[0].lsb) |
| 142 | + elif isinstance(self.nextnodes[0], DFTerminal): |
| 143 | + term = self.nextnodes[0].get_bind() |
| 144 | + msb = eval_value(term.msb) |
| 145 | + lsb = eval_value(term.lsb) |
| 146 | + else: |
| 147 | + raise Exception('Unexpected exception.') |
| 148 | + mark = op2mark.op2mark(self.operator) |
| 149 | + return mark.join([get_bus_name(term, i).replace('.', '_') for i in range(lsb, msb + 1)]) |
| 150 | + |
| 151 | +def DFTerminal_get_terms(self): |
| 152 | + scope = DFTerminal.scope_dict[str(self)] |
| 153 | + return DFTerminal.terms[scope] |
| 154 | + |
| 155 | +def get_bus_name(signal, bit): |
| 156 | + return str(signal) + '__' + str(bit) + '__' |
| 157 | + |
| 158 | +if __name__ == '__main__': |
| 159 | + fv = FormalVerifier("../testcode/fv_test.v") |
| 160 | + #fv.calc_truth_table('TOP.A') |
| 161 | + #fv.calc_truth_table('TOP.C') |
| 162 | + #fv.calc_truth_table('TOP.E') |
| 163 | + a=fv.calc_truth_table('TOP.G') |
| 164 | + fv.write_back_DFmethods() |
| 165 | + pass |
0 commit comments