Added "yosys-smtbmc -g"

1 files changed, 40 insertions, 6 deletions

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 3ad184190..ca5fb0ae9 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -25,6 +25,8 @@ skip_steps = 0
 step_size = 1
 num_steps = 20
 vcdfile = None
+vlogtbfile = None
+gentrace = False
 tempind = False
 assume_skipped = None
 topmod = None
@@ -44,6 +46,10 @@ yosys-smtbmc [options] <yosys_smt2_output>
     -S <step_size>
         prove <step_size> time steps at once
 
+    -g
+        generate an arbitrary trace that satisfies
+        all assertions and assumptions.
+
     -i
         instead of BMC run temporal induction
 
@@ -51,7 +57,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
         name of the top module
 
     --dump-vcd <vcd_filename>
-        write counter-example to this VCD file
+        write trace to this VCD file
         (hint: use 'write_smt2 -wires' for maximum
         coverage of signals in generated VCD file)
 """ + so.helpmsg())
@@ -59,7 +65,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
 
 
 try:
-    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:im:", so.longopts + ["dump-vcd="])
+    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:u:S:igm:", so.longopts + ["dump-vcd=", "dump-vlogtb="])
 except:
     usage()
 
@@ -79,6 +85,8 @@ for o, a in opts:
         vcdfile = a
     elif o == "-i":
         tempind = True
+    elif o == "-g":
+        gentrace = True
     elif o == "-m":
         topmod = a
     elif so.handle(o, a):
@@ -107,7 +115,7 @@ assert topmod is not None
 assert topmod in smt.modinfo
 
 
-def write_vcd_model(steps):
+def write_vcd_trace(steps):
     print("%s Writing model to VCD file." % smt.timestamp())
 
     vcd = mkvcd(open(vcdfile, "w"))
@@ -172,15 +180,41 @@ if tempind:
                 print("%s Temporal induction failed!" % smt.timestamp())
                 print_failed_asserts(topmod, "s%d" % step, topmod)
                 if vcdfile is not None:
-                    write_vcd_model(num_steps+1)
+                    write_vcd_trace(num_steps+1)
 
         else:
             print("%s Temporal induction successful." % smt.timestamp())
             retstatus = True
             break
 
+elif gentrace:
+    retstatus = True
+    for step in range(num_steps):
+        smt.write("(declare-fun s%d () %s_s)" % (step, topmod))
+        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))
+
+        if step == 0:
+            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))
+            smt.write("(assert (not (%s_is s%d)))" % (topmod, step))
+
+    print("%s Creating trace of length %d.." % (smt.timestamp(), num_steps))
+
+    if smt.check_sat() == "sat":
+        if vcdfile is not None:
+            write_vcd_trace(num_steps)
+
+    else:
+        print("%s Creating trace failed!" % smt.timestamp())
+        retstatus = False
+
 
-else: # not tempind
+else: # not tempind, not gentrace
     step = 0
     retstatus = True
     while step < num_steps:
@@ -226,7 +260,7 @@ else: # not tempind
             print("%s BMC failed!" % smt.timestamp())
             print_failed_asserts(topmod, "s%d" % step, topmod)
             if vcdfile is not None:
-                write_vcd_model(step+step_size)
+                write_vcd_trace(step+step_size)
             retstatus = False
             break