yosys-smtbmc: improved --dump-vlogtb handling of memories

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 9acbfbeb8bb40f7610b4f32cb2c300a9a5fa845a..aaafc3f9a2ace725beba47b74bc8c36e512fe613 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -460,19 +460,23 @@ struct Smt2Worker
                        decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
                                        log_id(module), arrayid, log_id(module), abits, width, log_id(cell)));
 
-                       decls.push_back(stringf("; yosys-smt2-memory %s %d %d\n", log_id(cell), abits, width));
+                       decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d\n", log_id(cell), abits, width, rd_ports));
                        decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s#%d#0| state))\n",
                                        log_id(module), log_id(cell), log_id(module), abits, width, log_id(module), arrayid));
 
                        for (int i = 0; i < rd_ports; i++)
                        {
-                               std::string addr = get_bv(cell->getPort("\\RD_ADDR").extract(abits*i, abits));
+                               SigSpec addr_sig = cell->getPort("\\RD_ADDR").extract(abits*i, abits);
                                SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
+                               std::string addr = get_bv(addr_sig);
 
                                if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
                                        log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
                                                        "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
 
+                               decls.push_back(stringf("(define-fun |%s_m:%d %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+                                               log_id(module), i, log_id(cell), log_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+
                                decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s#%d#0| state) %s)) ; %s\n",
                                                log_id(module), idcounter, log_id(module), width, log_id(module), arrayid, addr.c_str(), log_signal(data_sig)));
                                register_bv(data_sig, idcounter++);

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index a6e8bf67a7ed81b9cb84ea9ccde1861205d11ce5..1706714838293758861714c75454fee91b23f781 100644 (file)
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -200,13 +200,23 @@ def write_vlogtb_trace(steps):
 
         mems = sorted(smt.hiermems(topmod))
         for mempath in mems:
-            mem, abits, width = smt.mem_expr(topmod, "s0", mempath)
+            abits, width, ports = smt.mem_info(topmod, "s0", mempath)
+            mem = smt.mem_expr(topmod, "s0", mempath)
+
+            addr_expr_list = list()
+            for i in range(steps):
+                for j in range(ports):
+                    addr_expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, j))
+
+            addr_list = set()
+            for val in smt.get_list(addr_expr_list):
+                addr_list.add(smt.bv2int(val))
 
             expr_list = list()
-            for i in range(2**abits):
+            for i in addr_list:
                 expr_list.append("(select %s #b%s)" % (mem, format(i, "0%db" % abits)))
 
-            for i, val in enumerate(smt.get_list(expr_list)):
+            for i, val in zip(addr_list, smt.get_list(expr_list)):
                 val = smt.bv2bin(val)
                 print("    UUT.%s[%d] = %d'b%s;" % (".".join(mempath), i, len(val), val), file=f)
 

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 24c28182a1556b134a0bd0169fc338d906670519..8480891b04d6f2ab7fe81912602611767fedc0f1 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -128,7 +128,7 @@ class smtio:
             self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
 
         if fields[1] == "yosys-smt2-memory":
-            self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4]))
+            self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4]), int(fields[5]))
 
         if fields[1] == "yosys-smt2-wire":
             self.modinfo[self.curmod].wires.add(fields[2])
@@ -309,6 +309,9 @@ class smtio:
             return "".join(digits)
         assert False
 
+    def bv2int(self, v):
+        return int(self.bv2bin(v), 2)
+
     def get(self, expr):
         self.write("(get-value (%s))" % (expr))
         return self.parse(self.read())[0][1]
@@ -342,11 +345,13 @@ class smtio:
         assert net_path[-1] in self.modinfo[mod].wsize
         return self.modinfo[mod].wsize[net_path[-1]]
 
-    def mem_expr(self, mod, base, path):
+    def mem_expr(self, mod, base, path, portidx=None, infomode=False):
         if len(path) == 1:
             assert mod in self.modinfo
             assert path[0] in self.modinfo[mod].memories
-            return "(|%s_m %s| %s)" % (mod, path[0], base), self.modinfo[mod].memories[path[0]][0], self.modinfo[mod].memories[path[0]][1]
+            if infomode:
+                return self.modinfo[mod].memories[path[0]]
+            return "(|%s_m%s %s| %s)" % (mod, "" if portidx is None else ":%d" % portidx, path[0], base)
 
         assert mod in self.modinfo
         assert path[0] in self.modinfo[mod].cells
@@ -355,6 +360,9 @@ class smtio:
         nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
         return self.mem_expr(nextmod, nextbase, path[1:])
 
+    def mem_info(self, mod, base, path):
+        return self.mem_expr(mod, base, path, infomode=True)
+
     def get_net(self, mod_name, net_path, state_name):
         return self.get(self.net_expr(mod_name, state_name, net_path))