From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 14 Dec 2017 02:05:20 +0000 (+0100)
Subject: Add yosys-smtbmc VCD writer support for memories with async writes
X-Git-Tag: yosys-0.8~247
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9419de3e371451f7f0eb51e89cab3fa8bebba26c;p=yosys.git

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

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 5c3ce3753..e6e969011 100644
--- 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 560e39d86..c86b520a2 100644
--- 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 61ac14c82..ec5253205 100644
--- 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])