From 9419de3e371451f7f0eb51e89cab3fa8bebba26c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 14 Dec 2017 03:05:20 +0100 Subject: [PATCH] Add yosys-smtbmc VCD writer support for memories with async writes --- backends/smt2/smt2.cc | 4 ++-- backends/smt2/smtbmc.py | 12 ++++++++---- backends/smt2/smtio.py | 2 +- 3 files changed, 11 insertions(+), 7 deletions(-) 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]) -- 2.30.2