From 9fdedf4d1c5b1715f98ad107d322966eaee91f20 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Marcelina=20Ko=C5=9Bcielnicka?= Date: Tue, 10 Aug 2021 19:42:10 +0200 Subject: [PATCH] memory_dff: Recognize soft transparency logic. --- passes/memory/memory_dff.cc | 458 +++++++++++++++++- tests/memories/trans_sdp.v | 21 + tests/memories/trans_sp.v | 21 + tests/opt/memory_dff_trans.ys | 862 ++++++++++++++++++++++++++++++++++ 4 files changed, 1355 insertions(+), 7 deletions(-) create mode 100644 tests/memories/trans_sdp.v create mode 100644 tests/memories/trans_sp.v create mode 100644 tests/opt/memory_dff_trans.ys diff --git a/passes/memory/memory_dff.cc b/passes/memory/memory_dff.cc index 8ad131c7c..21962c238 100644 --- a/passes/memory/memory_dff.cc +++ b/passes/memory/memory_dff.cc @@ -19,7 +19,9 @@ #include "kernel/yosys.h" #include "kernel/sigtools.h" +#include "kernel/modtools.h" #include "kernel/ffinit.h" +#include "kernel/qcsat.h" #include "kernel/mem.h" #include "kernel/ff.h" #include "kernel/ffmerge.h" @@ -27,27 +29,317 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN +struct MuxData { + int base_idx; + int size; + bool is_b; + SigSpec sig_s; + std::vector sig_other; +}; + +struct PortData { + bool relevant; + std::vector uncollidable_mask; + std::vector transparency_mask; + std::vector collision_x_mask; + bool final_transparency; + bool final_collision_x; +}; + +// A helper with some caching for transparency-related SAT queries. +// Bound to a single memory read port in the process of being converted +// from async to sync.. +struct MemQueryCache +{ + QuickConeSat &qcsat; + // The memory. + Mem &mem; + // The port, still async at this point. + MemRd &port; + // The virtual FF that will end up merged into this port. + FfData &ff; + // An ezSAT variable that is true when we actually care about the data + // read from memory (ie. the FF has enable on and is not in reset). + int port_ren; + // Some caches. + dict, bool> cache_can_collide_rdwr; + dict, bool> cache_can_collide_together; + dict, bool> cache_is_w2rbyp; + dict, bool> cache_impossible_with_ren; + + MemQueryCache(QuickConeSat &qcsat, Mem &mem, MemRd &port, FfData &ff) : qcsat(qcsat), mem(mem), port(port), ff(ff) { + // port_ren is an upper bound on when we care about the value fetched + // from memory this cycle. + int ren = ezSAT::CONST_TRUE; + if (ff.has_en) { + ren = qcsat.importSigBit(ff.sig_en); + if (!ff.pol_en) + ren = qcsat.ez->NOT(ren); + } + if (ff.has_srst) { + int nrst = qcsat.importSigBit(ff.sig_srst); + if (ff.pol_srst) + nrst = qcsat.ez->NOT(nrst); + ren = qcsat.ez->AND(ren, nrst); + } + port_ren = ren; + } + + // Returns ezSAT variable that is true iff the two addresses are the same. + int addr_eq(SigSpec raddr, SigSpec waddr) { + int abits = std::max(GetSize(raddr), GetSize(waddr)); + raddr.extend_u0(abits); + waddr.extend_u0(abits); + return qcsat.ez->vec_eq(qcsat.importSig(raddr), qcsat.importSig(waddr)); + } + + // Returns true if a given write port bit can be active at the same time + // as this read port and at the same address. + bool can_collide_rdwr(int widx, SigBit wen) { + std::pair key(widx, wen); + auto it = cache_can_collide_rdwr.find(key); + if (it != cache_can_collide_rdwr.end()) + return it->second; + auto &wport = mem.wr_ports[widx]; + int aeq = addr_eq(port.addr, wport.addr); + int wen_sat = qcsat.importSigBit(wen); + qcsat.prepare(); + bool res = qcsat.ez->solve(aeq, wen_sat, port_ren); + cache_can_collide_rdwr[key] = res; + return res; + } + + // Returns true if both given write port bits can be active at the same + // time as this read port and at the same address (three-way collision). + bool can_collide_together(int widx1, int widx2, int bitidx) { + auto &wport1 = mem.wr_ports[widx1]; + auto &wport2 = mem.wr_ports[widx2]; + SigBit wen1 = wport1.en[bitidx]; + SigBit wen2 = wport2.en[bitidx]; + std::tuple key(widx1, widx2, wen1, wen2); + auto it = cache_can_collide_together.find(key); + if (it != cache_can_collide_together.end()) + return it->second; + int aeq1 = addr_eq(port.addr, wport1.addr); + int aeq2 = addr_eq(port.addr, wport2.addr); + int wen1_sat = qcsat.importSigBit(wen1); + int wen2_sat = qcsat.importSigBit(wen2); + qcsat.prepare(); + bool res = qcsat.ez->solve(wen1_sat, wen2_sat, aeq1, aeq2, port_ren); + cache_can_collide_together[key] = res; + return res; + } + + // Returns true if the given mux selection signal is a valid data-bypass + // signal in soft transparency logic for a given write port bit. + bool is_w2rbyp(int widx, SigBit wen, SigBit sel, bool neg_sel) { + std::tuple key(widx, wen, sel, neg_sel); + auto it = cache_is_w2rbyp.find(key); + if (it != cache_is_w2rbyp.end()) + return it->second; + auto &wport = mem.wr_ports[widx]; + int aeq = addr_eq(port.addr, wport.addr); + int wen_sat = qcsat.importSigBit(wen); + int sel_expected = qcsat.ez->AND(aeq, wen_sat); + int sel_sat = qcsat.importSigBit(sel); + if (neg_sel) + sel_sat = qcsat.ez->NOT(sel_sat); + qcsat.prepare(); + bool res = !qcsat.ez->solve(port_ren, qcsat.ez->XOR(sel_expected, sel_sat)); + cache_is_w2rbyp[key] = res; + return res; + } + + // Returns true if the given mux selection signal can never be true + // when this port is active. + bool impossible_with_ren(SigBit sel, bool neg_sel) { + std::tuple key(sel, neg_sel); + auto it = cache_impossible_with_ren.find(key); + if (it != cache_impossible_with_ren.end()) + return it->second; + int sel_sat = qcsat.importSigBit(sel); + if (neg_sel) + sel_sat = qcsat.ez->NOT(sel_sat); + qcsat.prepare(); + bool res = !qcsat.ez->solve(port_ren, sel_sat); + cache_impossible_with_ren[key] = res; + return res; + } + + // Helper for data_eq: walks up a multiplexer when the value of its + // sel signal is constant under the assumption that this read port + // is active and a given other mux sel signal is true. + bool walk_up_mux_cond(SigBit sel, bool neg_sel, SigBit &bit) { + auto &drivers = qcsat.modwalker.signal_drivers[qcsat.modwalker.sigmap(bit)]; + if (GetSize(drivers) != 1) + return false; + auto driver = *drivers.begin(); + if (!driver.cell->type.in(ID($mux), ID($pmux))) + return false; + log_assert(driver.port == ID::Y); + SigSpec sig_s = driver.cell->getPort(ID::S); + int sel_sat = qcsat.importSigBit(sel); + if (neg_sel) + sel_sat = qcsat.ez->NOT(sel_sat); + bool all_0 = true; + int width = driver.cell->parameters.at(ID::WIDTH).as_int(); + for (int i = 0; i < GetSize(sig_s); i++) { + int sbit = qcsat.importSigBit(sig_s[i]); + qcsat.prepare(); + if (!qcsat.ez->solve(port_ren, sel_sat, qcsat.ez->NOT(sbit))) { + bit = driver.cell->getPort(ID::B)[i * width + driver.offset]; + return true; + } + if (qcsat.ez->solve(port_ren, sel_sat, sbit)) + all_0 = false; + } + if (all_0) { + bit = driver.cell->getPort(ID::A)[driver.offset]; + return true; + } + return false; + } + + // Returns true if a given data signal is equivalent to another, under + // the assumption that this read port is active and a given mux sel signal + // is true. Used to match transparency logic data with write port data. + // The walk_up_mux_cond part is necessary because write ports in yosys + // tend to be connected to things like (wen ? wdata : 'x). + bool data_eq(SigBit sel, bool neg_sel, SigBit dbit, SigBit odbit) { + if (qcsat.modwalker.sigmap(dbit) == qcsat.modwalker.sigmap(odbit)) + return true; + while (walk_up_mux_cond(sel, neg_sel, dbit)); + while (walk_up_mux_cond(sel, neg_sel, odbit)); + return qcsat.modwalker.sigmap(dbit) == qcsat.modwalker.sigmap(odbit); + } +}; + struct MemoryDffWorker { Module *module; - SigMap sigmap; + ModWalker modwalker; FfInitVals initvals; FfMergeHelper merger; - MemoryDffWorker(Module *module) : module(module), sigmap(module) + MemoryDffWorker(Module *module) : module(module), modwalker(module->design) { - initvals.set(&sigmap, module); + modwalker.setup(module); + initvals.set(&modwalker.sigmap, module); merger.set(&initvals, module); } - void handle_rd_port(Mem &mem, int idx) + // Starting from the output of an async read port, as long as the data + // signal's only user is a mux data signal, passes through the mux + // and remembers information about it. Conceptually works on every + // bit separately, but coalesces the result when possible. + SigSpec walk_muxes(SigSpec data, std::vector &res) { + bool did_something; + do { + did_something = false; + int prev_idx = -1; + Cell *prev_cell = nullptr; + bool prev_is_b = false; + for (int i = 0; i < GetSize(data); i++) { + SigBit bit = modwalker.sigmap(data[i]); + auto &consumers = modwalker.signal_consumers[bit]; + if (GetSize(consumers) != 1 || modwalker.signal_outputs.count(bit)) + continue; + auto consumer = *consumers.begin(); + bool is_b; + if (consumer.cell->type == ID($mux)) { + if (consumer.port == ID::A) { + is_b = false; + } else if (consumer.port == ID::B) { + is_b = true; + } else { + continue; + } + } else if (consumer.cell->type == ID($pmux)) { + if (consumer.port == ID::A) { + is_b = false; + } else { + continue; + } + } else { + continue; + } + SigSpec y = consumer.cell->getPort(ID::Y); + int mux_width = GetSize(y); + SigBit ybit = y.extract(consumer.offset); + if (prev_cell != consumer.cell || prev_idx+1 != i || prev_is_b != is_b) { + MuxData md; + md.base_idx = i; + md.size = 0; + md.is_b = is_b; + md.sig_s = consumer.cell->getPort(ID::S); + md.sig_other.resize(GetSize(md.sig_s)); + prev_cell = consumer.cell; + prev_is_b = is_b; + res.push_back(md); + } + auto &md = res.back(); + md.size++; + for (int j = 0; j < GetSize(md.sig_s); j++) { + SigBit obit = consumer.cell->getPort(is_b ? ID::A : ID::B).extract(j * mux_width + consumer.offset); + md.sig_other[j].append(obit); + } + prev_idx = i; + data[i] = ybit; + did_something = true; + } + } while (did_something); + return data; + } + + // Merges FF and possibly soft transparency logic into an asynchronous + // read port, making it into a synchronous one. + // + // There are three moving parts involved here: + // + // - the async port, which we start from, whose data port is input to... + // - an arbitrary chain of $mux and $pmux cells implementing soft transparency + // logic (ie. bypassing write port's data iff the write port is active and + // writing to the same address as this read port), which in turn feeds... + // - a final FF + // + // The async port and the mux chain are not allowed to have any users that + // are not part of the above. + // + // The algorithm is: + // + // 1. Walk through the muxes. + // 2. Recognize the final FF. + // 3. Knowing the FF's clock and read enable, make a list of write ports + // that we'll run transparency analysis on. + // 4. For every mux bit, recognize it as one of: + // - a transparency bypass mux for some port + // - a bypass mux that feeds 'x instead (this will result in collision + // don't care behavior being recognized) + // - a mux that never selects the other value when read port is active, + // and can thus be skipped (this is necessary because this could + // be a transparency bypass mux for never-colliding port that other + // passes failed to optimize) + // - a mux whose other input is 'x, and can thus be skipped + // 5. When recognizing transparency bypasses, take care to preserve priority + // behavior — when two bypasses are sequential muxes on the chain, they + // effectively have priority over one another, and the transform can + // only be performed when either a) their corresponding write ports + // also have priority, or b) there can never be a three-way collision + // between the two write ports and the read port. + // 6. Check consistency of per-bit transparency masks, merge them into + // per-port transparency masks + // 7. If everything went fine in the previous steps, actually perform + // the merge. + void handle_rd_port(Mem &mem, QuickConeSat &qcsat, int idx) { auto &port = mem.rd_ports[idx]; log("Checking read port `%s'[%d] in module `%s': ", mem.memid.c_str(), idx, module->name.c_str()); + std::vector muxdata; + SigSpec data = walk_muxes(port.data, muxdata); FfData ff; pool> bits; - if (!merger.find_output_ff(port.data, ff, bits)) { + if (!merger.find_output_ff(data, ff, bits)) { log("no output FF found.\n"); return; } @@ -60,6 +352,144 @@ struct MemoryDffWorker log("output FF has both set and reset, not supported.\n"); return; } + + // Construct cache. + MemQueryCache cache(qcsat, mem, port, ff); + + // Prepare information structure about all ports, recognize port bits + // that can never collide at all and don't need to be checked. + std::vector portdata; + for (int i = 0; i < GetSize(mem.wr_ports); i++) { + PortData pd; + auto &wport = mem.wr_ports[i]; + pd.relevant = true; + if (!wport.clk_enable) + pd.relevant = false; + if (wport.clk != ff.sig_clk) + pd.relevant = false; + if (wport.clk_polarity != ff.pol_clk) + pd.relevant = false; + // In theory, we *could* support mismatched width + // ports here. However, it's not worth it — wide + // ports are recognized *after* memory_dff in + // a normal flow. + if (wport.wide_log2 != port.wide_log2) + pd.relevant = false; + pd.uncollidable_mask.resize(GetSize(port.data)); + pd.transparency_mask.resize(GetSize(port.data)); + pd.collision_x_mask.resize(GetSize(port.data)); + if (pd.relevant) { + // If we got this far, this port is potentially + // transparent and/or has undefined collision + // behavior. Now, for every bit, check if it can + // ever collide. + for (int j = 0; j < ff.width; j++) { + if (!cache.can_collide_rdwr(i, wport.en[j])) { + pd.uncollidable_mask[j] = true; + pd.collision_x_mask[j] = true; + } + } + } + portdata.push_back(pd); + } + + // Now inspect the mux chain. + for (auto &md : muxdata) { + // We only mark transparent bits after processing a complete + // mux, so that the transparency priority validation check + // below sees transparency information as of previous mux. + std::vector> trans_queue; + for (int sel_idx = 0; sel_idx < GetSize(md.sig_s); sel_idx++) { + SigBit sbit = md.sig_s[sel_idx]; + SigSpec &odata = md.sig_other[sel_idx]; + for (int bitidx = md.base_idx; bitidx < md.base_idx+md.size; bitidx++) { + SigBit odbit = odata[bitidx-md.base_idx]; + bool recognized = false; + for (int pi = 0; pi < GetSize(mem.wr_ports); pi++) { + auto &pd = portdata[pi]; + auto &wport = mem.wr_ports[pi]; + if (!pd.relevant) + continue; + if (pd.uncollidable_mask[bitidx]) + continue; + bool match = cache.is_w2rbyp(pi, wport.en[bitidx], sbit, md.is_b); + if (!match) + continue; + // If we got here, we recognized this mux sel + // as valid bypass sel for a given port bit. + if (odbit == State::Sx) { + // 'x, mark collision don't care. + pd.collision_x_mask[bitidx] = true; + pd.transparency_mask[bitidx] = false; + } else if (cache.data_eq(sbit, md.is_b, wport.data[bitidx], odbit)) { + // Correct data value, mark transparency, + // but only after verifying that priority + // is fine. + for (int k = 0; k < GetSize(mem.wr_ports); k++) { + if (portdata[k].transparency_mask[bitidx]) { + if (wport.priority_mask[k]) + continue; + if (!cache.can_collide_together(pi, k, bitidx)) + continue; + log("FF found, but transparency logic priority doesn't match write priority.\n"); + return; + } + } + recognized = true; + trans_queue.push_back({pd, bitidx}); + break; + } else { + log("FF found, but with a mux data input that doesn't seem to correspond to transparency logic.\n"); + return; + } + } + if (!recognized) { + // If we haven't positively identified this as + // a bypass: it's still skippable if the + // data is 'x, or if the sel cannot actually be + // active. + if (odbit == State::Sx) + continue; + if (cache.impossible_with_ren(sbit, md.is_b)) + continue; + log("FF found, but with a mux select that doesn't seem to correspond to transparency logic.\n"); + return; + } + } + } + // Done with this mux, now actually apply the transparencies. + for (auto it : trans_queue) { + it.first.transparency_mask[it.second] = true; + it.first.collision_x_mask[it.second] = false; + } + } + + // Final merging and validation of per-bit masks. + for (int pi = 0; pi < GetSize(mem.wr_ports); pi++) { + auto &pd = portdata[pi]; + if (!pd.relevant) + continue; + bool trans = false; + bool non_trans = false; + for (int i = 0; i < ff.width; i++) { + if (pd.collision_x_mask[i]) + continue; + if (pd.transparency_mask[i]) + trans = true; + else + non_trans = true; + } + if (trans && non_trans) { + log("FF found, but soft transparency logic is inconsistent for port %d.\n", pi); + return; + } + pd.final_transparency = trans; + pd.final_collision_x = !trans && !non_trans; + } + + // OK, it worked. + log("merging output FF to cell.\n"); + merger.remove_output_ff(bits); if (ff.has_en && !ff.pol_en) ff.sig_en = module->LogicNot(NEW_ID, ff.sig_en); @@ -89,8 +519,21 @@ struct MemoryDffWorker } port.init_value = ff.val_init; port.data = ff.sig_q; + for (int pi = 0; pi < GetSize(mem.wr_ports); pi++) { + auto &pd = portdata[pi]; + if (!pd.relevant) + continue; + if (pd.final_collision_x) { + log(" Write port %d: don't care on collision.\n", pi); + port.collision_x_mask[pi] = true; + } else if (pd.final_transparency) { + log(" Write port %d: transparent.\n", pi); + port.transparency_mask[pi] = true; + } else { + log(" Write port %d: non-transparent.\n", pi); + } + } mem.emit(); - log("merged output FF to cell.\n"); } void handle_rd_port_addr(Mem &mem, int idx) @@ -146,9 +589,10 @@ struct MemoryDffWorker { std::vector memories = Mem::get_selected_memories(module); for (auto &mem : memories) { + QuickConeSat qcsat(modwalker); for (int i = 0; i < GetSize(mem.rd_ports); i++) { if (!mem.rd_ports[i].clk_enable) - handle_rd_port(mem, i); + handle_rd_port(mem, qcsat, i); } } for (auto &mem : memories) { diff --git a/tests/memories/trans_sdp.v b/tests/memories/trans_sdp.v new file mode 100644 index 000000000..b89f2ccf0 --- /dev/null +++ b/tests/memories/trans_sdp.v @@ -0,0 +1,21 @@ +// expect-wr-ports 1 +// expect-rd-ports 1 +// expect-rd-clk \clk +// expect-rd-en \re + +module top(input clk, we, re, input [7:0] ra, wa, wd, output reg [7:0] rd); + +reg [7:0] mem[0:255]; + +always @(posedge clk) begin + if (we) + mem[wa] <= wd; + + if (re) begin + rd <= mem[ra]; + if (we && ra == wa) + rd <= wd; + end +end + +endmodule diff --git a/tests/memories/trans_sp.v b/tests/memories/trans_sp.v new file mode 100644 index 000000000..ddd41a13e --- /dev/null +++ b/tests/memories/trans_sp.v @@ -0,0 +1,21 @@ +// expect-wr-ports 1 +// expect-rd-ports 1 +// expect-rd-clk \clk +// expect-rd-en \re + +module top(input clk, we, re, input [7:0] addr, wd, output reg [7:0] rd); + +reg [7:0] mem[0:255]; + +always @(posedge clk) begin + if (we) + mem[addr] <= wd; + + if (re) begin + rd <= mem[addr]; + if (we) + rd <= wd; + end +end + +endmodule diff --git a/tests/opt/memory_dff_trans.ys b/tests/opt/memory_dff_trans.ys new file mode 100644 index 000000000..7599949f3 --- /dev/null +++ b/tests/opt/memory_dff_trans.ys @@ -0,0 +1,862 @@ +# Good case 1: single port. + +read_verilog << EOT + +module top( + input [3:0] addr, + input [3:0] wd, + input we, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we) begin + mem[addr] <= wd; + rd <= wd; + end else begin + rd <= mem[addr]; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=1'b1 r:RD_COLLISION_X_MASK=1'b0 %i %i + +design -reset + +# Good case 2: single port, exclusive. + +read_verilog << EOT + +module top( + input [3:0] addr, + input [3:0] wd, + input we, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we) begin + mem[addr] <= wd; + end else begin + rd <= mem[addr]; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=1'b0 r:RD_COLLISION_X_MASK=1'b1 %i %i + +design -reset + +# Good case 3: proper bypass muxes. + +read_verilog << EOT + +module top( + input [3:0] ra, + input [3:0] wa1, + input [3:0] wa2, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + if (we1 && wa1 == ra) + rd <= wd1; + if (we2 && wa2 == ra) + rd <= wd2; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=2'b11 r:RD_COLLISION_X_MASK=2'b00 %i %i + +design -reset + +# Good case 4: proper bypass mux, but only one. + +read_verilog << EOT + +module top( + input [3:0] ra, + input [3:0] wa1, + input [3:0] wa2, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + if (we1 && wa1 == ra) + rd <= wd1; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=2'b01 r:RD_COLLISION_X_MASK=2'b00 %i %i + +design -reset + +# Good case 5: proper bypass mux, but the other one. + +read_verilog << EOT + +module top( + input [3:0] ra, + input [3:0] wa1, + input [3:0] wa2, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + if (we2 && wa2 == ra) + rd <= wd2; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=2'b10 r:RD_COLLISION_X_MASK=2'b00 %i %i + +design -reset + +# Good case 6: 'x mux. + +read_verilog << EOT + +module top( + input [3:0] ra, + input [3:0] wa1, + input [3:0] wa2, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + if (we1 && wa1 == ra) + rd <= 4'hx; + if (we2 && wa2 == ra) + rd <= wd2; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=2'b10 r:RD_COLLISION_X_MASK=2'b01 %i %i + +design -reset + +# Good case 7: uncollidable addresses. + +read_verilog << EOT + +module top( + input [3:0] addr, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +wire [3:0] wa1 = addr; +wire [3:0] wa2 = addr + 1; +wire [3:0] ra = addr + 2; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=2'b00 r:RD_COLLISION_X_MASK=2'b11 %i %i + +design -reset + +# Good case 8: uncollidable addresses, but still have soft transparency logic. + +read_verilog << EOT + +module top( + input [3:0] addr, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +wire [3:0] wa1 = addr; +wire [3:0] wa2 = addr + 1; +wire [3:0] ra = addr + 2; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + if (we1 && wa1 == ra) + rd <= wd1; + if (we2 && wa2 == ra) + rd <= wd2; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=2'b00 r:RD_COLLISION_X_MASK=2'b11 %i %i + +design -reset + +# Bad case 1: broken bypass signal. + +read_verilog << EOT + +module top( + input [3:0] ra, + input [3:0] wa1, + input [3:0] wa2, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + if (we1 && wa1 == ra) + rd <= wd1; + if (we2 && wa2 == ra && we1) + rd <= wd2; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +logger -expect log "FF found, but with a mux select that doesn't seem to correspond to transparency logic" 1 +memory_dff +logger -check-expected +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_CLK_ENABLE=1'b0 %i + +design -reset + +# Bad case 2: bad data signal. + +read_verilog << EOT + +module top( + input [3:0] ra, + input [3:0] wa1, + input [3:0] wa2, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + if (we1 && wa1 == ra) + rd <= wd1; + if (we2 && wa2 == ra) + rd <= wd1; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +logger -expect log "FF found, but with a mux data input that doesn't seem to correspond to transparency logic" 1 +memory_dff +logger -check-expected +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_CLK_ENABLE=1'b0 %i + +design -reset + +# Bad case 3: priority mismatch. + +read_verilog << EOT + +module top( + input [3:0] ra, + input [3:0] wa1, + input [3:0] wa2, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + if (we2 && wa2 == ra) + rd <= wd2; + if (we1 && wa1 == ra) + rd <= wd1; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +logger -expect log "FF found, but transparency logic priority doesn't match write priority." 1 +memory_dff +logger -check-expected +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_CLK_ENABLE=1'b0 %i + +design -reset + +# Good case 10: priority mismatch, but since the second value is 'x, it's still OK. + +read_verilog << EOT + +module top( + input [3:0] ra, + input [3:0] wa1, + input [3:0] wa2, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + if (we2 && wa2 == ra) + rd <= wd2; + if (we1 && wa1 == ra) + rd <= 4'hx; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=2'b10 r:RD_COLLISION_X_MASK=2'b01 %i %i + +design -reset + +# Good case 11: priority mismatch, but since three-way collision cannot happen, it's still OK. + +read_verilog << EOT + +module top( + input [3:0] addr, + input [1:0] mode, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] wa1, wa2, ra; + +always @* begin + case (mode) + 0: begin + wa1 = addr+1; + wa2 = addr; + ra = addr; + end + 1: begin + wa1 = addr; + wa2 = addr+1; + ra = addr; + end + 2: begin + wa1 = addr; + wa2 = addr; + ra = addr+1; + end + 3: begin + wa1 = addr; + wa2 = addr+1; + ra = addr+2; + end + endcase +end + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + if (we2 && wa2 == ra) + rd <= wd2; + if (we1 && wa1 == ra) + rd <= wd1; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=2'b11 r:RD_COLLISION_X_MASK=2'b00 %i %i + +design -reset + +# Bad case 4: half of the port is transparent. + +read_verilog << EOT + +module top( + input [3:0] ra, + input [3:0] wa1, + input [3:0] wa2, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2] <= wd2; + if (re) begin + rd <= mem[ra]; + if (we1 && wa1 == ra) + rd <= wd1; + if (we2 && wa2 == ra) + rd[3:2] <= wd2[3:2]; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +logger -expect log "FF found, but soft transparency logic is inconsistent for port 1." 1 +memory_dff +logger -check-expected +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_CLK_ENABLE=1'b0 %i + +design -reset + +# Good case 12: like above, but the other bits aren't changed by the port anyway. + +read_verilog << EOT + +module top( + input [3:0] ra, + input [3:0] wa1, + input [3:0] wa2, + input [3:0] wd1, + input [3:0] wd2, + input we1, we2, + input re, + input clk, + output reg [3:0] rd, +); + +reg [3:0] mem[0:15]; + +always @(posedge clk) begin + if (we1) + mem[wa1] <= wd1; + if (we2) + mem[wa2][3:2] <= wd2[3:2]; + if (re) begin + rd <= mem[ra]; + if (we1 && wa1 == ra) + rd <= wd1; + if (we2 && wa2 == ra) + rd[3:2] <= wd2[3:2]; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=2'b11 r:RD_COLLISION_X_MASK=2'b00 %i %i + +design -reset + +# Good case 13: wide read, narrow write. + +read_verilog << EOT + +module top( + input [7:0] addr, + input [7:0] wd, + input we, + input re, + input clk, + output reg [31:0] rd, +); + +reg [7:0] mem[0:255]; + +always @(posedge clk) begin + if (we) + mem[addr] <= wd; + if (re) begin + rd[7:0] <= mem[{addr[7:2], 2'b00}]; + rd[15:8] <= mem[{addr[7:2], 2'b01}]; + rd[23:16] <= mem[{addr[7:2], 2'b10}]; + rd[31:24] <= mem[{addr[7:2], 2'b11}]; + case ({we, addr[1:0]}) + 3'b100: rd[7:0] <= wd; + 3'b101: rd[15:8] <= wd; + 3'b110: rd[23:16] <= wd; + 3'b111: rd[31:24] <= wd; + endcase + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +dump +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=4'b1111 r:RD_COLLISION_X_MASK=4'b0000 %i %i + +design -reset + +# Good case 14: narrow read, wide write. + +read_verilog << EOT + +module top( + input [7:0] addr, + input [31:0] wd, + input we, + input re, + input clk, + output reg [7:0] rd, +); + +reg [7:0] mem[0:255]; + +always @(posedge clk) begin + if (we) begin + mem[{addr[7:2], 2'b00}] <= wd[7:0]; + mem[{addr[7:2], 2'b01}] <= wd[15:8]; + mem[{addr[7:2], 2'b10}] <= wd[23:16]; + mem[{addr[7:2], 2'b11}] <= wd[31:24]; + end + if (re) begin + rd <= mem[addr]; + case ({we, addr[1:0]}) + 3'b100: rd <= wd[7:0]; + 3'b101: rd <= wd[15:8]; + 3'b110: rd <= wd[23:16]; + 3'b111: rd <= wd[31:24]; + endcase + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +dump +memory_dff +memory_collect +select -assert-count 1 t:$mem_v2 +select -assert-count 1 t:$mem_v2 r:RD_TRANSPARENCY_MASK=4'b1111 r:RD_COLLISION_X_MASK=4'b0000 %i %i + +design -reset + +# Good case 15: wide read, wide write. + +read_verilog << EOT + +module top( + input [7:0] addr, + input [31:0] wd, + input we, + input re, + input clk, + output reg [31:0] rd, +); + +reg [7:0] mem[0:255]; + +always @(posedge clk) begin + if (we) begin + mem[{addr[7:2], 2'b00}] <= wd[7:0]; + mem[{addr[7:2], 2'b01}] <= wd[15:8]; + mem[{addr[7:2], 2'b10}] <= wd[23:16]; + mem[{addr[7:2], 2'b11}] <= wd[31:24]; + end + if (re) begin + rd[7:0] <= mem[{addr[7:2], 2'b00}]; + rd[15:8] <= mem[{addr[7:2], 2'b01}]; + rd[23:16] <= mem[{addr[7:2], 2'b10}]; + rd[31:24] <= mem[{addr[7:2], 2'b11}]; + if (we) + rd <= wd; + end +end + +endmodule + +EOT + +hierarchy -auto-top +proc +opt_dff +opt_clean +dump +memory_dff +select -assert-count 4 t:$memrd_v2 +select -assert-count 1 t:$memrd_v2 r:TRANSPARENCY_MASK=4'b0001 r:COLLISION_X_MASK=4'b1110 %i %i +select -assert-count 1 t:$memrd_v2 r:TRANSPARENCY_MASK=4'b0010 r:COLLISION_X_MASK=4'b1101 %i %i +select -assert-count 1 t:$memrd_v2 r:TRANSPARENCY_MASK=4'b0100 r:COLLISION_X_MASK=4'b1011 %i %i +select -assert-count 1 t:$memrd_v2 r:TRANSPARENCY_MASK=4'b1000 r:COLLISION_X_MASK=4'b0111 %i %i + +design -reset -- 2.30.2