Add yosys-smtbmc VCD writer support for memories with async writes

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 5c3ce3753b0a4eaa003d6b34004a5e0f2111bec2..e6e96901189227f5606b8da580692d1ff5ac9b3c 100644 (file)
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -554,8 +554,6 @@ struct Smt2Worker
                        int rd_ports = cell->getParam("\\RD_PORTS").as_int();
                        int wr_ports = cell->getParam("\\WR_PORTS").as_int();
 
-                       decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d\n", get_id(cell), abits, width, rd_ports, wr_ports));
-
                        bool async_read = false;
                        if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_ones()) {
                                if (!cell->getParam("\\WR_CLK_ENABLE").is_fully_zero())
@@ -563,6 +561,8 @@ struct Smt2Worker
                                async_read = true;
                        }
 
+                       decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(cell), abits, width, rd_ports, wr_ports, async_read ? "async" : "sync"));
+
                        string memstate;
                        if (async_read) {
                                memstate = stringf("%s#%d#final", get_id(module), arrayid);

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 560e39d863807fe67be7db445173e27667a76a46..c86b520a2eb7bef68431105c10147c27bbd65718 100644 (file)
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -594,7 +594,7 @@ def write_vcd_trace(steps_start, steps_stop, index):
 
         mem_trace_data = dict()
         for mempath in sorted(smt.hiermems(topmod)):
-            abits, width, rports, wports = smt.mem_info(topmod, mempath)
+            abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath)
 
             expr_id = list()
             expr_list = list()
@@ -666,7 +666,8 @@ def write_vcd_trace(steps_start, steps_stop, index):
                                     else:
                                         buf[k] = tdata[i][k]
 
-                    tdata.append(data[:])
+                    if not asyncwr:
+                        tdata.append(data[:])
 
                     for j_data in wdata[i]:
                         if j_data["A"] != addr:
@@ -679,6 +680,9 @@ def write_vcd_trace(steps_start, steps_stop, index):
                             if M[k] == "1":
                                 data[k] = D[k]
 
+                    if asyncwr:
+                        tdata.append(data[:])
+
                 assert len(tdata) == len(rdata)
 
                 netpath = mempath[:]
@@ -785,7 +789,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
 
         mems = sorted(smt.hiermems(vlogtb_topmod))
         for mempath in mems:
-            abits, width, rports, wports = smt.mem_info(vlogtb_topmod, mempath)
+            abits, width, rports, wports, asyncwr = smt.mem_info(vlogtb_topmod, mempath)
 
             addr_expr_list = list()
             data_expr_list = list()
@@ -888,7 +892,7 @@ def write_constr_trace(steps_start, steps_stop, index):
 
         mems = sorted(smt.hiermems(constr_topmod))
         for mempath in mems:
-            abits, width, rports, wports = smt.mem_info(constr_topmod, mempath)
+            abits, width, rports, wports, asyncwr = smt.mem_info(constr_topmod, mempath)
 
             addr_expr_list = list()
             data_expr_list = list()

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 61ac14c82b7d467846a59547980b4b415e5170b4..ec5253205ab98827665e1f454b8152ec2001c4b4 100644 (file)
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -387,7 +387,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]), int(fields[5]), int(fields[6]))
+            self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4]), int(fields[5]), int(fields[6]), fields[7] == "async")
 
         if fields[1] == "yosys-smt2-wire":
             self.modinfo[self.curmod].wires.add(fields[2])