From 925f92918af783af71d5c9f1f358f79de5c20f04 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 6 Oct 2022 15:36:35 +0200 Subject: clk2fflogic: Always correctly handle simultaneously changing signals This is a complete rewrite of the FF replacing code. The previous implementation tried to implement the negative hold time by wrapping async control signals individually with pulse stretching. This did not correctly model the interaction between different simultaneously changing inputs (e.g. a falling ALOAD together with a changing AD would load the changed AD instead of the value AD had when ALOAD was high; a falling CLR could mask a raising SET for one cycle; etc.). The new approach first has the logic for all updates using only sampled values followed by the logic for all updates using only current values. That way, e.g., a falling ALOAD will load the sampled AD value but a still active ALOAD will load the current AD value. The new code also has deterministic behavior for the initial state: no operation is active when that operation would depend on a specific previous signal value. This also means clk2fflogic will no longer generate any additional uninitialized FFs. I also documented the negative hold time behavior in the help message, copying the relevant part from async2sync's help messages. --- passes/sat/clk2fflogic.cc | 190 +++++++++++++++++++++------------------------- 1 file changed, 87 insertions(+), 103 deletions(-) (limited to 'passes') diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index 2384ffced..bba2cbbec 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -26,6 +26,11 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN +struct SampledSig { + SigSpec sampled, current; + SigSpec &operator[](bool get_current) { return get_current ? current : sampled; } +}; + struct Clk2fflogicPass : public Pass { Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { } void help() override @@ -38,37 +43,65 @@ struct Clk2fflogicPass : public Pass { log("implicit global clock. This is useful for formal verification of designs with\n"); log("multiple clocks.\n"); log("\n"); + log("This pass assumes negative hold time for the async FF inputs. For example when\n"); + log("a reset deasserts with the clock edge, then the FF output will still drive the\n"); + log("reset value in the next cycle regardless of the data-in value at the time of\n"); + log("the clock edge.\n"); + log("\n"); } - SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, bool is_fine, IdString past_sig_id) { - if (!is_fine) - return wrap_async_control(module, sig, polarity, past_sig_id); - return wrap_async_control_gate(module, sig, polarity, past_sig_id); + // Active-high sampled and current value of a level-triggered control signal. Initial sampled values is low/non-asserted. + SampledSig sample_control(Module *module, SigSpec sig, bool polarity, bool is_fine) { + if (!polarity) { + if (is_fine) + sig = module->NotGate(NEW_ID, sig); + else + sig = module->Not(NEW_ID, sig); + } + std::string sig_str = log_signal(sig); + sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end()); + Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig)); + sampled_sig->attributes[ID::init] = RTLIL::Const(State::S0, GetSize(sig)); + if (is_fine) + module->addFfGate(NEW_ID, sig, sampled_sig); + else + module->addFf(NEW_ID, sig, sampled_sig); + return {sampled_sig, sig}; } - SigSpec wrap_async_control(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) { - Wire *past_sig = module->addWire(past_sig_id, GetSize(sig)); - past_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S0 : State::S1, GetSize(sig)); - module->addFf(NEW_ID, sig, past_sig); - if (polarity) - sig = module->Or(NEW_ID, sig, past_sig); + // Active-high trigger signal for an edge-triggered control signal. Initial values is low/non-edge. + SigSpec sample_control_edge(Module *module, SigSpec sig, bool polarity, bool is_fine) { + std::string sig_str = log_signal(sig); + sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end()); + Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig)); + sampled_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S1 : State::S0, GetSize(sig)); + if (is_fine) + module->addFfGate(NEW_ID, sig, sampled_sig); else - sig = module->And(NEW_ID, sig, past_sig); - if (polarity) - return sig; + module->addFf(NEW_ID, sig, sampled_sig); + return module->Eqx(NEW_ID, {sampled_sig, sig}, polarity ? SigSpec {State::S0, State::S1} : SigSpec {State::S1, State::S0}); + } + // Sampled and current value of a data signal. + SampledSig sample_data(Module *module, SigSpec sig, RTLIL::Const init, bool is_fine) { + std::string sig_str = log_signal(sig); + sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end()); + Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig)); + sampled_sig->attributes[ID::init] = init; + if (is_fine) + module->addFfGate(NEW_ID, sig, sampled_sig); else - return module->Not(NEW_ID, sig); + module->addFf(NEW_ID, sig, sampled_sig); + return {sampled_sig, sig}; } - SigSpec wrap_async_control_gate(Module *module, SigSpec sig, bool polarity, IdString past_sig_id) { - Wire *past_sig = module->addWire(past_sig_id); - past_sig->attributes[ID::init] = polarity ? State::S0 : State::S1; - module->addFfGate(NEW_ID, sig, past_sig); - if (polarity) - sig = module->OrGate(NEW_ID, sig, past_sig); + SigSpec mux(Module *module, SigSpec a, SigSpec b, SigSpec s, bool is_fine) { + if (is_fine) + return module->MuxGate(NEW_ID, a, b, s); else - sig = module->AndGate(NEW_ID, sig, past_sig); - if (polarity) - return sig; + return module->Mux(NEW_ID, a, b, s); + } + SigSpec bitwise_sr(Module *module, SigSpec a, SigSpec s, SigSpec r, bool is_fine) { + if (is_fine) + return module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r)); else - return module->NotGate(NEW_ID, sig); + return module->And(NEW_ID, module->Or(NEW_ID, a, s), module->Not(NEW_ID, r)); } void execute(std::vector args, RTLIL::Design *design) override { @@ -177,96 +210,47 @@ struct Clk2fflogicPass : public Pass { ff.remove(); - // Strip spaces from signal name, since Yosys IDs can't contain spaces - // Spaces only occur when we have a signal that's a slice of a larger bus, - // e.g. "\myreg [5:0]", so removing spaces shouldn't result in loss of uniqueness - std::string sig_q_str = log_signal(ff.sig_q); - sig_q_str.erase(std::remove(sig_q_str.begin(), sig_q_str.end(), ' '), sig_q_str.end()); - - Wire *past_q = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_q_wire", sig_q_str.c_str())), ff.width); - - if (!ff.is_fine) { - module->addFf(NEW_ID, ff.sig_q, past_q); - } else { - module->addFfGate(NEW_ID, ff.sig_q, past_q); - } - if (!ff.val_init.is_fully_undef()) - initvals.set_init(past_q, ff.val_init); - - if (ff.has_clk) { + if (ff.has_clk) ff.unmap_ce_srst(); - Wire *past_clk = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_clk#%s", sig_q_str.c_str(), log_signal(ff.sig_clk)))); - initvals.set_init(past_clk, ff.pol_clk ? State::S1 : State::S0); - - if (!ff.is_fine) - module->addFf(NEW_ID, ff.sig_clk, past_clk); - else - module->addFfGate(NEW_ID, ff.sig_clk, past_clk); + auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine).sampled; - SigSpec clock_edge_pattern; - - if (ff.pol_clk) { - clock_edge_pattern.append(State::S0); - clock_edge_pattern.append(State::S1); - } else { - clock_edge_pattern.append(State::S1); - clock_edge_pattern.append(State::S0); - } - - SigSpec clock_edge = module->Eqx(NEW_ID, {ff.sig_clk, SigSpec(past_clk)}, clock_edge_pattern); - - Wire *past_d = module->addWire(NEW_ID_SUFFIX(stringf("%s#past_d_wire", sig_q_str.c_str())), ff.width); - if (!ff.is_fine) - module->addFf(NEW_ID, ff.sig_d, past_d); - else - module->addFfGate(NEW_ID, ff.sig_d, past_d); - - if (!ff.val_init.is_fully_undef()) - initvals.set_init(past_d, ff.val_init); - - if (!ff.is_fine) - qval = module->Mux(NEW_ID, past_q, past_d, clock_edge); - else - qval = module->MuxGate(NEW_ID, past_q, past_d, clock_edge); - } else { - qval = past_q; + if (ff.has_clk) { + // The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs + auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine); + auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine); + next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine); } + SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst; // The check for a constant sig_aload is also done by opt_dff, but when using verific and running // clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids // generating a lot of extra logic. - if (ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1)) { - SigSpec sig_aload = wrap_async_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine, NEW_ID); - - if (!ff.is_fine) - qval = module->Mux(NEW_ID, qval, ff.sig_ad, sig_aload); - else - qval = module->MuxGate(NEW_ID, qval, ff.sig_ad, sig_aload); + bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1); + if (has_nonconst_aload) { + sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine); + // The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs + sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine); } - if (ff.has_sr) { - SigSpec setval = wrap_async_control(module, ff.sig_set, ff.pol_set, ff.is_fine, NEW_ID); - SigSpec clrval = wrap_async_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine, NEW_ID); - if (!ff.is_fine) { - clrval = module->Not(NEW_ID, clrval); - qval = module->Or(NEW_ID, qval, setval); - module->addAnd(NEW_ID, qval, clrval, ff.sig_q); - } else { - clrval = module->NotGate(NEW_ID, clrval); - qval = module->OrGate(NEW_ID, qval, setval); - module->addAndGate(NEW_ID, qval, clrval, ff.sig_q); - } - } else if (ff.has_arst) { - IdString id = NEW_ID_SUFFIX(stringf("%s#past_arst#%s", sig_q_str.c_str(), log_signal(ff.sig_arst))); - SigSpec arst = wrap_async_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine, id); - if (!ff.is_fine) - module->addMux(NEW_ID, qval, ff.val_arst, arst, ff.sig_q); - else - module->addMuxGate(NEW_ID, qval, ff.val_arst[0], arst, ff.sig_q); - } else { - module->connect(ff.sig_q, qval); + sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine); + sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine); + } + if (ff.has_arst) + sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine); + + // First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous + // implementation, this approach correctly handles all the cases of multiple signals changing simultaneously. + for (int current = 0; current < 2; current++) { + if (has_nonconst_aload) + next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine); + if (ff.has_sr) + next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine); + if (ff.has_arst) + next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine); } + + module->connect(ff.sig_q, next_q); } } } -- cgit v1.2.3 From 381ce66f5870291fe950c276c492b303f714738f Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Wed, 28 Apr 2021 16:52:04 +0200 Subject: Revert "Merge pull request #641 from tklam/master" This reverts commit 08be796cb8b1890923e459cda92211fda763f0c1, reversing changes made to 38dbb44fa0815b1fe80e68e17798aaa341d998cd. This fixes #2728. PR #641 did not actually "fix" #639. The actual issue in #639 is not equiv_make, but assumptions in equiv_simple that are not true for the test case provided in #639. --- passes/equiv/equiv_make.cc | 86 +++------------------------------------------- 1 file changed, 5 insertions(+), 81 deletions(-) (limited to 'passes') diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc index 7ef2827bf..4d9e3b71a 100644 --- a/passes/equiv/equiv_make.cc +++ b/passes/equiv/equiv_make.cc @@ -40,16 +40,6 @@ struct EquivMakeWorker pool undriven_bits; SigMap assign_map; - dict> bit2driven; // map: bit <--> and its driven cells - - CellTypes comb_ct; - - EquivMakeWorker() - { - comb_ct.setup_internals(); - comb_ct.setup_stdcells(); - } - void read_blacklists() { for (auto fn : blacklists) @@ -288,31 +278,16 @@ struct EquivMakeWorker } } - init_bit2driven(); - - pool visited_cells; for (auto c : cells_list) for (auto &conn : c->connections()) if (!ct.cell_output(c->type, conn.first)) { SigSpec old_sig = assign_map(conn.second); SigSpec new_sig = rd_signal_map(old_sig); - - if(old_sig != new_sig) { - SigSpec tmp_sig = old_sig; - for (int i = 0; i < GetSize(old_sig); i++) { - SigBit old_bit = old_sig[i], new_bit = new_sig[i]; - - visited_cells.clear(); - if (check_signal_in_fanout(visited_cells, old_bit, new_bit)) - continue; - - log("Changing input %s of cell %s (%s): %s -> %s\n", - log_id(conn.first), log_id(c), log_id(c->type), - log_signal(old_bit), log_signal(new_bit)); - - tmp_sig[i] = new_bit; - } - c->setPort(conn.first, tmp_sig); + if (old_sig != new_sig) { + log("Changing input %s of cell %s (%s): %s -> %s\n", + log_id(conn.first), log_id(c), log_id(c->type), + log_signal(old_sig), log_signal(new_sig)); + c->setPort(conn.first, new_sig); } } @@ -403,57 +378,6 @@ struct EquivMakeWorker } } - void init_bit2driven() - { - for (auto cell : equiv_mod->cells()) { - if (!ct.cell_known(cell->type) && !cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_), ID($ff), ID($_FF_))) - continue; - for (auto &conn : cell->connections()) - { - if (yosys_celltypes.cell_input(cell->type, conn.first)) - for (auto bit : assign_map(conn.second)) - { - bit2driven[bit].insert(cell); - } - } - } - } - - bool check_signal_in_fanout(pool & visited_cells, SigBit source_bit, SigBit target_bit) - { - if (source_bit == target_bit) - return true; - - if (bit2driven.count(source_bit) == 0) - return false; - - auto driven_cells = bit2driven.at(source_bit); - for (auto driven_cell: driven_cells) - { - bool is_comb = comb_ct.cell_known(driven_cell->type); - if (!is_comb) - continue; - - if (visited_cells.count(driven_cell) > 0) - continue; - visited_cells.insert(driven_cell); - - for (auto &conn: driven_cell->connections()) - { - if (yosys_celltypes.cell_input(driven_cell->type, conn.first)) - continue; - - for (auto bit: conn.second) { - bool is_in_fanout = check_signal_in_fanout(visited_cells, bit, target_bit); - if (is_in_fanout == true) - return true; - } - } - } - - return false; - } - void run() { copy_to_equiv(); -- cgit v1.2.3 From afa5e6bb53f15abf26ec9a0c633539cc95f57f60 Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Tue, 4 May 2021 18:54:10 +0200 Subject: Exclude primary inputs from quiv_make rewiring Signed-off-by: Claire Xenia Wolf --- passes/equiv/equiv_make.cc | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'passes') diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc index 4d9e3b71a..27cec7549 100644 --- a/passes/equiv/equiv_make.cc +++ b/passes/equiv/equiv_make.cc @@ -137,6 +137,7 @@ struct EquivMakeWorker { SigMap assign_map(equiv_mod); SigMap rd_signal_map; + SigPool primary_inputs; // list of cells without added $equiv cells auto cells_list = equiv_mod->cells().to_vector(); @@ -252,6 +253,9 @@ struct EquivMakeWorker gate_wire->port_input = false; equiv_mod->connect(gold_wire, wire); equiv_mod->connect(gate_wire, wire); + primary_inputs.add(assign_map(gold_wire)); + primary_inputs.add(assign_map(gate_wire)); + primary_inputs.add(wire); } else { @@ -283,6 +287,9 @@ struct EquivMakeWorker if (!ct.cell_output(c->type, conn.first)) { SigSpec old_sig = assign_map(conn.second); SigSpec new_sig = rd_signal_map(old_sig); + for (int i = 0; i < GetSize(old_sig); i++) + if (primary_inputs.check(old_sig[i])) + new_sig[i] = old_sig[i]; if (old_sig != new_sig) { log("Changing input %s of cell %s (%s): %s -> %s\n", log_id(conn.first), log_id(c), log_id(c->type), -- cgit v1.2.3 From 051630763741914c3ba3bdf25ea091395dbc00b4 Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Tue, 4 May 2021 19:02:37 +0200 Subject: Add "check -assert" to equiv_opt Signed-off-by: Claire Xenia Wolf --- passes/equiv/equiv_opt.cc | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) (limited to 'passes') diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc index 4d0400448..f5eb75730 100644 --- a/passes/equiv/equiv_opt.cc +++ b/passes/equiv/equiv_opt.cc @@ -60,13 +60,16 @@ struct EquivOptPass:public ScriptPass log(" -undef\n"); log(" enable modelling of undef states during equiv_induct.\n"); log("\n"); + log(" -nocheck\n"); + log(" disable running check before and after the command under test.\n"); + log("\n"); log("The following commands are executed by this verification command:\n"); help_script(); log("\n"); } std::string command, techmap_opts, make_opts; - bool assert, undef, multiclock, async2sync; + bool assert, undef, multiclock, async2sync, nocheck; void clear_flags() override { @@ -77,6 +80,7 @@ struct EquivOptPass:public ScriptPass undef = false; multiclock = false; async2sync = false; + nocheck = false; } void execute(std::vector < std::string > args, RTLIL::Design * design) override @@ -110,6 +114,10 @@ struct EquivOptPass:public ScriptPass undef = true; continue; } + if (args[argidx] == "-nocheck") { + nocheck = true; + continue; + } if (args[argidx] == "-multiclock") { multiclock = true; continue; @@ -153,10 +161,14 @@ struct EquivOptPass:public ScriptPass if (check_label("run_pass")) { run("hierarchy -auto-top"); run("design -save preopt"); + if (!nocheck) + run("check -assert", "(unless -nocheck)"); if (help_mode) run("[command]"); else run(command); + if (!nocheck) + run("check -assert", "(unless -nocheck)"); run("design -stash postopt"); } -- cgit v1.2.3