From 302166dd59d8f04aacec30223868fce13a3094dd Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 15 Oct 2015 15:08:41 +0200
Subject: Improvements in yosys-smtbmc

---
 backends/smt2/smt2.cc   | 1 +
 backends/smt2/smtbmc.py | 8 ++++++--
 backends/smt2/smtio.py  | 2 ++
 3 files changed, 9 insertions(+), 2 deletions(-)

(limited to 'backends/smt2')

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)
 
-- 
cgit v1.2.3