Added "yosys-smtbmc --dump-constr"

2 files changed, 62 insertions, 2 deletions

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 170671483..bd3e237ab 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
+outconstr = None
 gentrace = False
 tempind = False
 assume_skipped = None
@@ -63,12 +64,15 @@ yosys-smtbmc [options] <yosys_smt2_output>
 
     --dump-vlogtb <verilog_filename>
         write trace as Verilog test bench
+
+    --dump-constr <constr_filename>
+        write trace as constraints file
 """ + so.helpmsg())
     sys.exit(1)
 
 
 try:
-    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:igm:", so.longopts + ["dump-vcd=", "dump-vlogtb="])
+    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:igm:", so.longopts + ["dump-vcd=", "dump-vlogtb=", "dump-constr="])
 except:
     usage()
 
@@ -88,6 +92,8 @@ for o, a in opts:
         vcdfile = a
     elif o == "--dump-vlogtb":
         vlogtbfile = a
+    elif o == "--dump-constr":
+        outconstr = a
     elif o == "-i":
         tempind = True
     elif o == "-g":
@@ -237,6 +243,57 @@ def write_vlogtb_trace(steps):
         print("endmodule", file=f)
 
 
+def write_constr_trace(steps):
+    print("%s Writing trace to constraints file." % smt.timestamp())
+
+    with open(outconstr, "w") as f:
+        primary_inputs = list()
+
+        for name in smt.modinfo[topmod].inputs:
+            width = smt.modinfo[topmod].wsize[name]
+            primary_inputs.append((name, width))
+
+        for k in range(steps):
+            if k != 0:
+                print("", file=f)
+
+            print("state %d" % k, file=f)
+
+            if k == 0:
+                regnames = sorted(smt.hiernets(topmod, regs_only=True))
+                regvals = smt.get_net_list(topmod, regnames, "s0")
+
+                for name, val in zip(regnames, regvals):
+                    print("assume (= [%s] %s)" % (".".join(name), val), file=f)
+
+                mems = sorted(smt.hiermems(topmod))
+                for mempath in mems:
+                    abits, width, ports = smt.mem_info(topmod, "s0", mempath)
+                    mem = smt.mem_expr(topmod, "s0", mempath)
+
+                    addr_expr_list = list()
+                    for i in range(steps):
+                        for j in range(ports):
+                            addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, j))
+
+                    addr_list = set()
+                    for val in smt.get_list(addr_expr_list):
+                        addr_list.add(smt.bv2int(val))
+
+                    expr_list = list()
+                    for i in addr_list:
+                        expr_list.append("(select %s #b%s)" % (mem, format(i, "0%db" % abits)))
+
+                    for i, val in zip(addr_list, smt.get_list(expr_list)):
+                        print("assume (= (select [%s] #b%s) %s)" % (".".join(mempath), format(i, "0%db" % abits), val), file=f)
+
+            pi_names = [[name] for name, _ in primary_inputs]
+            pi_values = smt.get_net_list(topmod, pi_names, "s%d" % k)
+
+            for name, val in zip(pi_names, pi_values):
+                print("assume (= [%s] %s)" % (".".join(name), val), file=f)
+
+
 def write_trace(steps):
     if vcdfile is not None:
         write_vcd_trace(steps)
@@ -244,6 +301,9 @@ def write_trace(steps):
     if vlogtbfile is not None:
         write_vlogtb_trace(steps)
 
+    if outconstr is not None:
+        write_constr_trace(steps)
+
 
 def print_failed_asserts(mod, state, path):
     assert mod in smt.modinfo
diff --git a/examples/smtbmc/Makefile b/examples/smtbmc/Makefile
index 649c3f69b..711be712b 100644
--- a/examples/smtbmc/Makefile
+++ b/examples/smtbmc/Makefile
@@ -6,7 +6,7 @@ demo1: demo1.smt2
 	yosys-smtbmc -i --dump-vcd demo1.vcd demo1.smt2
 
 demo2: demo2.smt2
-	yosys-smtbmc -g --dump-vcd demo2.vcd --dump-vlogtb demo2_tb.v demo2.smt2
+	yosys-smtbmc -g --dump-vcd demo2.vcd --dump-vlogtb demo2_tb.v --dump-constr demo2.smtc demo2.smt2
 	iverilog -g2012 -o demo2_tb demo2_tb.v demo2.v
 	vvp demo2_tb +vcd=demo2_tb.vcd