Add "yosys-smtbmc --smtc-init --smtc-top --noinit"

1 files changed, 66 insertions, 20 deletions

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index a2bb3d6e4..c8151c266 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -45,6 +45,9 @@ final_only = False
 topmod = None
 noinfo = False
 presat = False
+smtcinit = False
+smtctop = None
+noinit = False
 so = SmtOpts()
 
 
@@ -124,6 +127,16 @@ yosys-smtbmc [options] <yosys_smt2_output>
     --dump-smtc <constr_filename>
         write trace as constraints file
 
+    --smtc-init
+        write just the last state as initial constraint to smtc file
+
+    --smtc-top <old>[:<new>]
+        replace <old> with <new> in constraints dumped to smtc
+        file and only dump object below <old> in design hierarchy.
+
+    --noinit
+        do not assume initial conditions in state 0
+
     --dump-all
         when using -g or -i, create a dump file for each
         step. The character '%' is replaces in all dump
@@ -140,7 +153,8 @@ yosys-smtbmc [options] <yosys_smt2_output>
 try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
             ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat",
-             "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append="])
+             "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
+             "smtc-init", "smtc-top=", "noinit"])
 except:
     usage()
 
@@ -183,12 +197,22 @@ for o, a in opts:
         vlogtbtop = a
     elif o == "--dump-smtc":
         outconstr = a
+    elif o == "--smtc-init":
+        smtcinit = True
+    elif o == "--smtc-top":
+        smtctop = a.split(":")
+        if len(smtctop) == 1:
+            smtctop.append("")
+        assert len(smtctop) == 2
+        smtctop = tuple(smtctop)
     elif o == "--dump-all":
         dumpall = True
     elif o == "--presat":
         presat = True
     elif o == "--noinfo":
         noinfo = True
+    elif o == "--noinit":
+        noinit = True
     elif o == "--append":
         append_steps = int(a)
     elif o == "-i":
@@ -826,34 +850,49 @@ def write_constr_trace(steps_start, steps_stop, index):
     filename = outconstr.replace("%", index)
     print_msg("Writing trace to constraints file: %s" % (filename))
 
+    constr_topmod = topmod
+    constr_state = "s@@step_idx@@"
+    constr_prefix = ""
+
+    if smtctop is not None:
+        for item in smtctop[0].split("."):
+            assert item in smt.modinfo[constr_topmod].cells
+            constr_state = "(|%s_h %s| %s)" % (constr_topmod, item, constr_state)
+            constr_topmod = smt.modinfo[constr_topmod].cells[item]
+        if smtctop[1] != "":
+            constr_prefix = smtctop[1] + "."
+
+    if smtcinit:
+        steps_start = steps_stop - 1
+
     with open(filename, "w") as f:
         primary_inputs = list()
 
-        for name in smt.modinfo[topmod].inputs:
-            width = smt.modinfo[topmod].wsize[name]
+        for name in smt.modinfo[constr_topmod].inputs:
+            width = smt.modinfo[constr_topmod].wsize[name]
             primary_inputs.append((name, width))
 
-        if steps_start == 0:
+        if steps_start == 0 or smtcinit:
             print("initial", file=f)
         else:
             print("state %d" % steps_start, file=f)
 
-        regnames = sorted(smt.hiernets(topmod, regs_only=True))
-        regvals = smt.get_net_list(topmod, regnames, "s%d" % steps_start)
+        regnames = sorted(smt.hiernets(constr_topmod, regs_only=True))
+        regvals = smt.get_net_list(constr_topmod, regnames, constr_state.replace("@@step_idx@@", str(steps_start)))
 
         for name, val in zip(regnames, regvals):
-            print("assume (= [%s] %s)" % (".".join(name), val), file=f)
+            print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
 
-        mems = sorted(smt.hiermems(topmod))
+        mems = sorted(smt.hiermems(constr_topmod))
         for mempath in mems:
-            abits, width, rports, wports = smt.mem_info(topmod, mempath)
+            abits, width, rports, wports = smt.mem_info(constr_topmod, mempath)
 
             addr_expr_list = list()
             data_expr_list = list()
             for i in range(steps_start, steps_stop):
                 for j in range(rports):
-                    addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
-                    data_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
+                    addr_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
+                    data_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))
 
             addr_list = smt.get_list(addr_expr_list)
             data_list = smt.get_list(data_expr_list)
@@ -864,17 +903,18 @@ def write_constr_trace(steps_start, steps_stop, index):
                     addr_data[addr] = data
 
             for addr, data in addr_data.items():
-                print("assume (= (select [%s] %s) %s)" % (".".join(mempath), addr, data), file=f)
+                print("assume (= (select [%s%s] %s) %s)" % (constr_prefix, ".".join(mempath), addr, data), file=f)
 
         for k in range(steps_start, steps_stop):
-            print("", file=f)
-            print("state %d" % k, file=f)
+            if not smtcinit:
+                print("", file=f)
+                print("state %d" % k, file=f)
 
             pi_names = [[name] for name, _ in sorted(primary_inputs)]
-            pi_values = smt.get_net_list(topmod, pi_names, "s%d" % k)
+            pi_values = smt.get_net_list(constr_topmod, pi_names, constr_state.replace("@@step_idx@@", str(k)))
 
             for name, val in zip(pi_names, pi_values):
-                print("assume (= [%s] %s)" % (".".join(name), val), file=f)
+                print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
 
 
 def write_trace(steps_start, steps_stop, index):
@@ -1034,8 +1074,11 @@ elif covermode:
         smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
 
         if step == 0:
-            smt.write("(assert (|%s_i| s0))" % (topmod))
-            smt.write("(assert (|%s_is| s0))" % (topmod))
+            if noinit:
+                smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
+            else:
+                smt.write("(assert (|%s_i| s0))" % (topmod))
+                smt.write("(assert (|%s_is| s0))" % (topmod))
 
         else:
             smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step))
@@ -1114,8 +1157,11 @@ else:  # not tempind, covermode
         smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
 
         if step == 0:
-            smt.write("(assert (|%s_i| s0))" % (topmod))
-            smt.write("(assert (|%s_is| s0))" % (topmod))
+            if noinit:
+                smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
+            else:
+                smt.write("(assert (|%s_i| s0))" % (topmod))
+                smt.write("(assert (|%s_is| s0))" % (topmod))
 
         else:
             smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step))