From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 1 Jul 2017 00:13:32 +0000 (+0200)
Subject: Fix smtbmc vlogtb bug in $anyseq handling
X-Git-Tag: yosys-0.8~409
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7d2fb6e2fc8e2cdd9eebe40cd04256be8f590012;p=yosys.git

Fix smtbmc vlogtb bug in $anyseq handling
---

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index ceca5b3f8..096097594 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -755,11 +755,11 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
 
             for info in anyseqs:
                 if info[3] is not None:
-                    modstate = smt.net_expr(topmod, "s%d" % steps_start, info[0])
+                    modstate = smt.net_expr(topmod, "s%d" % i, info[0])
                     value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
-                    print("    UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
+                    print("    UUT.%s <= %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
 
-        print("    genclock = 0;", file=f)
+        print("    genclock <= 0;", file=f)
         print("  end", file=f)
 
         print("endmodule", file=f)