diff options
| -rw-r--r-- | backends/smt2/smt2.cc | 4 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 12 | ||||
| -rw-r--r-- | backends/smt2/smtio.py | 2 | ||||
| -rw-r--r-- | passes/sat/clk2fflogic.cc | 2 |
4 files changed, 12 insertions, 8 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]) diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index d334cf7d9..7e952e99b 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -126,7 +126,7 @@ struct Clk2fflogicPass : public Pass { SigSpec clock_edge = module->Eqx(NEW_ID, {clk, SigSpec(past_clk)}, clock_edge_pattern); - SigSpec en_q = module->addWire(NEW_ID, GetSize(addr)); + SigSpec en_q = module->addWire(NEW_ID, GetSize(en)); module->addFf(NEW_ID, en, en_q); SigSpec addr_q = module->addWire(NEW_ID, GetSize(addr)); |