From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 15 Oct 2015 13:08:41 +0000 (+0200)
Subject: Improvements in yosys-smtbmc
X-Git-Tag: yosys-0.6~106
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=302166dd59d8f04aacec30223868fce13a3094dd;p=yosys.git

Improvements in yosys-smtbmc
---

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index a51a82709..a748ca05d 100644
--- 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 65729efa9..60cd9775e 100644
--- 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 799efa88c..6e8bded77 100644
--- 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)