diff options
| author | Clifford Wolf <clifford@clifford.at> | 2015-10-15 15:08:41 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2015-10-15 15:10:33 +0200 |
| commit | 302166dd59d8f04aacec30223868fce13a3094dd (patch) | |
| tree | 380cfbd7bdbfdb41f6bf25c92f5f6bcb18d51d80 | |
| parent | 1d83854d84b7a0a23ee14b72c1a289b50becdeca (diff) | |
Improvements in yosys-smtbmc
| -rw-r--r-- | backends/smt2/smt2.cc | 1 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 8 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 2 |
3 files changed, 9 insertions, 2 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a51a8270..a748ca05 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 65729efa..60cd9775 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 799efa88..6e8bded7 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) |