diff options
| -rw-r--r-- | backends/smt2/smtbmc.py | 77 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 21 |
2 files changed, 94 insertions, 4 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index bd3e237ab..a11fed2d5 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -26,6 +26,7 @@ step_size = 1 num_steps = 20 vcdfile = None vlogtbfile = None +inconstr = list() outconstr = None gentrace = False tempind = False @@ -57,6 +58,9 @@ yosys-smtbmc [options] <yosys_smt2_output> -m <module_name> name of the top module + --constr <constr_filename> + read constraints file + --dump-vcd <vcd_filename> write trace to this VCD file (hint: use 'write_smt2 -wires' for maximum @@ -72,7 +76,7 @@ yosys-smtbmc [options] <yosys_smt2_output> try: - opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:igm:", so.longopts + ["dump-vcd=", "dump-vlogtb=", "dump-constr="]) + opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:igm:", so.longopts + ["constr=", "dump-vcd=", "dump-vlogtb=", "dump-constr="]) except: usage() @@ -88,6 +92,8 @@ for o, a in opts: assume_skipped = int(a) elif o == "-S": step_size = int(a) + elif o == "--constr": + inconstr.append(a) elif o == "--dump-vcd": vcdfile = a elif o == "--dump-vlogtb": @@ -109,6 +115,65 @@ if len(args) != 1: usage() +if tempind and len(inconstr) != 0: + print("Error: options -i and --constr are exclusive."); + sys.exit(1) + + +constr_asserts = dict() +constr_assumes = dict() + +for fn in inconstr: + current_state = None + + with open(fn, "r") as f: + for line in f: + tokens = line.split() + + if len(tokens) == 0: + continue + + if tokens[0] == "initial": + current_state = 0 + continue + + if tokens[0] == "state": + current_state = int(tokens[1]) + continue + + if tokens[0] == "assert": + assert current_state is not None + + if current_state not in constr_asserts: + constr_asserts[current_state] = list() + + constr_asserts[current_state].append(" ".join(tokens[1:])) + continue + + if tokens[0] == "assume": + assert current_state is not None + + if current_state not in constr_assumes: + constr_assumes[current_state] = list() + + constr_assumes[current_state].append(" ".join(tokens[1:])) + continue + + assert 0 + + +def get_constr_expr(db, state): + if state not in db: + return "true" + + expr_list = list() + for expr in db[state]: + expr = re.sub(r'\[([^\]]+)\]', lambda match: smt.net_expr(topmod, "s%d" % state, smt.get_path(topmod, match.group(1))), expr) + expr_list.append(expr) + + return "(and %s)" % " ".join(expr_list) + + smt = smtio(opts=so) print("%s Solver: %s" % (smt.timestamp(), so.solver)) @@ -358,6 +423,7 @@ if tempind: retstatus = True break + elif gentrace: retstatus = True for step in range(num_steps): @@ -365,6 +431,8 @@ elif gentrace: smt.write("(assert (%s_u s%d))" % (topmod, step)) smt.write("(assert (%s_a s%d))" % (topmod, step)) smt.write("(assert (%s_h s%d))" % (topmod, step)) + smt.write("(assert %s)" % get_constr_expr(constr_asserts, step)) + smt.write("(assert %s)" % get_constr_expr(constr_assumes, step)) if step == 0: smt.write("(assert (%s_i s0))" % (topmod)) @@ -391,6 +459,7 @@ else: # not tempind, not gentrace smt.write("(declare-fun s%d () %s_s)" % (step, topmod)) smt.write("(assert (%s_u s%d))" % (topmod, step)) smt.write("(assert (%s_h s%d))" % (topmod, step)) + smt.write("(assert %s)" % get_constr_expr(constr_assumes, step)) if step == 0: smt.write("(assert (%s_i s0))" % (topmod)) @@ -404,6 +473,7 @@ else: # not tempind, not gentrace if assume_skipped is not None and step >= assume_skipped: print("%s Skipping step %d (and assuming pass).." % (smt.timestamp(), step)) smt.write("(assert (%s_a s%d))" % (topmod, step)) + smt.write("(assert %s)" % get_constr_expr(constr_asserts, step)) else: print("%s Skipping step %d.." % (smt.timestamp(), step)) step += 1 @@ -416,6 +486,7 @@ else: # not tempind, not gentrace smt.write("(assert (%s_u s%d))" % (topmod, step+i)) smt.write("(assert (%s_h s%d))" % (topmod, step+i)) smt.write("(assert (%s_t s%d s%d))" % (topmod, step+i-1, step+i)) + smt.write("(assert %s)" % get_constr_expr(constr_assumes, step+i)) last_check_step = step+i if last_check_step == step: @@ -424,7 +495,8 @@ else: # not tempind, not gentrace print("%s Checking asserts in steps %d to %d.." % (smt.timestamp(), step, last_check_step)) smt.write("(push 1)") - smt.write("(assert (not (and %s)))" % " ".join(["(%s_a s%d)" % (topmod, i) for i in range(step, last_check_step+1)])) + smt.write("(assert (not (and %s)))" % " ".join(["(%s_a s%d)" % (topmod, i) for i in range(step, last_check_step+1)] + + [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)])) if smt.check_sat() == "sat": print("%s BMC failed!" % smt.timestamp()) @@ -437,6 +509,7 @@ else: # not tempind, not gentrace smt.write("(pop 1)") for i in range(step, last_check_step+1): smt.write("(assert (%s_a s%d))" % (topmod, i)) + smt.write("(assert %s)" % get_constr_expr(constr_asserts, i)) step += step_size diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 8480891b0..0b2263338 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -322,11 +322,28 @@ class smtio: self.write("(get-value (%s))" % " ".join(expr_list)) return [n[1] for n in self.parse(self.read())] + def get_path(self, mod, path): + assert mod in self.modinfo + path = path.split(".") + + for i in range(len(path)-1): + first = ".".join(path[0:i+1]) + second = ".".join(path[i+1:]) + + if first in self.modinfo[mod].cells: + nextmod = self.modinfo[mod].cells[first] + return [first] + self.get_path(nextmod, second) + + return [".".join(path)] + def net_expr(self, mod, base, path): if len(path) == 1: assert mod in self.modinfo - assert path[0] in self.modinfo[mod].wsize - return "(|%s_n %s| %s)" % (mod, path[0], base) + if path[0] in self.modinfo[mod].wsize: + return "(|%s_n %s| %s)" % (mod, path[0], base) + if path[0] in self.modinfo[mod].memories: + return "(|%s_m %s| %s)" % (mod, path[0], base) + assert 0 assert mod in self.modinfo assert path[0] in self.modinfo[mod].cells |