Improvements in yosys-smtbmc

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";

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())

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)