Improvements in yosys-smtbmc

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index a51a827098c3c10ea1356e032bcfa275e25d9905..a748ca05dded4841ed2c5314d73e709d2135536e 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -631,6 +631,7 @@ struct Smt2Worker
                for (auto it : decls)
                        f << it;
 
+               f << stringf("; yosys-smt2-module %s\n", log_id(module));
                f << stringf("(define-fun |%s_t| ((state |%s_s|) (next_state |%s_s|)) Bool ", log_id(module), log_id(module), log_id(module));
                if (GetSize(trans) > 1) {
                        f << "(and\n";

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 65729efa94b33b3f0974118dea24b279ef743065..60cd9775ee90fee07fc307ac0a38e2a73551df30 100644 (file)
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -26,7 +26,7 @@ num_steps = 20
 vcdfile = None
 tempind = False
 assume_skipped = None
-topmod = "main"
+topmod = None
 so = smtopts()
 
 
@@ -49,7 +49,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
         instead of BMC run temporal induction
 
     -m <module_name>
-        name of the top module, default: main
+        name of the top module
 """ + so.helpmsg())
     sys.exit(1)
 
@@ -97,8 +97,12 @@ with open(args[0], "r") as f:
         match = debug_nets_re.match(line)
         if match:
             debug_nets.add(match.group(2))
+        if line.startswith("; yosys-smt2-module") and topmod is None:
+            topmod = line.split()[2]
         smt.write(line)
 
+assert topmod is not None
+
 
 def write_vcd_model(steps):
     print("%s Writing model to VCD file." % smt.timestamp())

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 799efa88c5ae8dcf39b33fa0f6d38eaeab36f69d..6e8bded771a11b7707b63edcb94088177bc881f3 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -313,6 +313,7 @@ class mkvcd:
         assert t >= self.t
         if t != self.t:
             if self.t == -1:
+                print("$var event 1 ! smt_clock $end", file=self.f)
                 for name in sorted(self.nets):
                     key, width = self.nets[name]
                     print("$var wire %d %s %s $end" % (width, key, name), file=self.f)
@@ -320,4 +321,5 @@ class mkvcd:
             self.t = t
             assert self.t >= 0
             print("#%d" % self.t, file=self.f)
+            print("1!", file=self.f)