From 925f92918af783af71d5c9f1f358f79de5c20f04 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 6 Oct 2022 15:36:35 +0200 Subject: [PATCH 1/7] 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 | 192 +++++++++++++++++--------------------- 1 file changed, 88 insertions(+), 104 deletions(-) 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; - else - return module->Not(NEW_ID, 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}); } - 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); + // 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 - sig = module->AndGate(NEW_ID, sig, past_sig); - if (polarity) - return sig; + module->addFf(NEW_ID, sig, sampled_sig); + return {sampled_sig, 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 - return module->NotGate(NEW_ID, 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->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); + auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine).sampled; - if (!ff.is_fine) - module->addFf(NEW_ID, ff.sig_clk, past_clk); - else - module->addFfGate(NEW_ID, ff.sig_clk, past_clk); - - 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); } } } From 381ce66f5870291fe950c276c492b303f714738f Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Wed, 28 Apr 2021 16:52:04 +0200 Subject: [PATCH 2/7] 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(-) 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(); From afa5e6bb53f15abf26ec9a0c633539cc95f57f60 Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Tue, 4 May 2021 18:54:10 +0200 Subject: [PATCH 3/7] Exclude primary inputs from quiv_make rewiring Signed-off-by: Claire Xenia Wolf --- passes/equiv/equiv_make.cc | 7 +++++++ 1 file changed, 7 insertions(+) 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), From f0478c520dd87f463a7fd8aee741273a85f3b1d4 Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Tue, 4 May 2021 20:12:29 +0200 Subject: [PATCH 4/7] Re-enable opt_dff_sr equiv_opt checks Signed-off-by: Claire Xenia Wolf --- tests/opt/opt_dff_sr.ys | 25 ++++++++++++------------- 1 file changed, 12 insertions(+), 13 deletions(-) diff --git a/tests/opt/opt_dff_sr.ys b/tests/opt/opt_dff_sr.ys index 0961cb11e..1d3fd300e 100644 --- a/tests/opt/opt_dff_sr.ys +++ b/tests/opt/opt_dff_sr.ys @@ -22,10 +22,9 @@ EOT design -save orig -# Equivalence check will fail for unmapped adlatch and dlatchsr due to negative hold hack. -#equiv_opt -undef -assert -multiclock opt_dff -#design -load postopt -opt_dff +equiv_opt -undef -assert -multiclock opt_dff +design -load postopt + select -assert-count 1 t:$dffsr select -assert-count 1 t:$dffsr r:WIDTH=2 %i select -assert-count 1 t:$dffsre @@ -36,9 +35,9 @@ select -assert-none t:$sr design -load orig -#equiv_opt -undef -assert -multiclock opt_dff -keepdc -#design -load postopt -opt_dff -keepdc +equiv_opt -undef -assert -multiclock opt_dff -keepdc +design -load postopt + select -assert-count 1 t:$dffsr select -assert-count 1 t:$dffsr r:WIDTH=4 %i select -assert-count 1 t:$dffsre @@ -51,9 +50,9 @@ select -assert-count 1 t:$sr r:WIDTH=4 %i design -load orig simplemap -#equiv_opt -undef -assert -multiclock opt_dff -#design -load postopt -opt_dff +equiv_opt -undef -assert -multiclock opt_dff +design -load postopt + select -assert-count 1 t:$_DFF_PP0_ select -assert-count 1 t:$_DFF_PP1_ select -assert-count 1 t:$_DFFE_PN0P_ @@ -65,9 +64,9 @@ select -assert-none t:$_DFF_PP0_ t:$_DFF_PP1_ t:$_DFFE_PN0P_ t:$_DFFE_PN1P_ t:$_ design -load orig simplemap -#equiv_opt -undef -assert -multiclock opt_dff -keepdc -#design -load postopt -opt_dff -keepdc +equiv_opt -undef -assert -multiclock opt_dff -keepdc +design -load postopt + select -assert-count 1 t:$_DFF_PP0_ select -assert-count 1 t:$_DFF_PP1_ select -assert-count 2 t:$_DFFSR_PPP_ From 051630763741914c3ba3bdf25ea091395dbc00b4 Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Tue, 4 May 2021 19:02:37 +0200 Subject: [PATCH 5/7] 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(-) 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"); } From 81906aa627ed4a2d232a27a84e050bf86f2f83a6 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 25 Aug 2022 14:24:31 +0200 Subject: [PATCH 6/7] Fix tests for check in equiv_opt --- tests/arch/ice40/bug1597.ys | 3 ++- tests/arch/ice40/ice40_opt.ys | 1 + tests/arch/xilinx/abc9_dff.ys | 7 +++++++ tests/arch/xilinx/opt_lut_ins.ys | 1 + tests/arch/xilinx/xilinx_dffopt.ys | 12 ++++++------ tests/opt/opt_dff_en.ys | 2 +- tests/opt/opt_dff_mux.ys | 2 +- tests/opt/opt_dff_qd.ys | 2 +- tests/techmap/dfflegalize_adlatch.ys | 2 +- tests/techmap/dfflegalize_adlatch_init.ys | 2 +- tests/techmap/dfflibmap.ys | 6 ++++-- tests/techmap/dffunmap.ys | 2 +- tests/techmap/zinit.ys | 4 ++++ 13 files changed, 31 insertions(+), 15 deletions(-) diff --git a/tests/arch/ice40/bug1597.ys b/tests/arch/ice40/bug1597.ys index b7983cfa4..73bc18eb2 100644 --- a/tests/arch/ice40/bug1597.ys +++ b/tests/arch/ice40/bug1597.ys @@ -3,7 +3,7 @@ module top ( input CLK, PIN_1, PIN_2, PIN_3, PIN_4, PIN_5, PIN_6, PIN_7, PIN_8, PIN_9, PIN_10, PIN_11, PIN_12, PIN_13, PIN_25, output USBPU, PIN_14, PIN_15, PIN_16, PIN_17, PIN_18, - PIN_19, PIN_20, PIN_21, PIN_22, PIN_23, PIN_24, + PIN_19, ); assign USBPU = 0; @@ -67,6 +67,7 @@ module SSCounter6o (input wire rst, clk, adv, jmp, input wire [5:0] in, output w SB_LUT4 #(.LUT_INIT(16'h8BB8)) l5 (lo[5], in[5], jmp, out[5], co[4]); endmodule EOT +read_verilog -lib +/ice40/cells_sim.v hierarchy -top top flatten equiv_opt -multiclock -map +/ice40/cells_sim.v synth_ice40 diff --git a/tests/arch/ice40/ice40_opt.ys b/tests/arch/ice40/ice40_opt.ys index 71b68431e..e779ab207 100644 --- a/tests/arch/ice40/ice40_opt.ys +++ b/tests/arch/ice40/ice40_opt.ys @@ -21,6 +21,7 @@ module top(input CI, I0, output [1:0] CO, output O); endmodule EOT +read_verilog -icells -lib +/ice40/abc9_model.v +/ice40/cells_sim.v equiv_opt -assert -map +/ice40/abc9_model.v -map +/ice40/cells_sim.v ice40_opt design -load postopt select -assert-count 1 t:* diff --git a/tests/arch/xilinx/abc9_dff.ys b/tests/arch/xilinx/abc9_dff.ys index 0ba3901f7..79e5a322c 100644 --- a/tests/arch/xilinx/abc9_dff.ys +++ b/tests/arch/xilinx/abc9_dff.ys @@ -12,6 +12,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b1), .D(D), .CLR(1'b1), .Q(Q[6])); FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b1), .D(D), .PRE(1'b1), .Q(Q[7])); endmodule EOT +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 6 t:FD* @@ -31,6 +32,7 @@ FDCE_1 #(.INIT(0)) fd7(.C(C), .CE(1'b0), .D(D), .CLR(1'b0), .Q(Q[6])); FDPE_1 #(.INIT(0)) fd8(.C(C), .CE(1'b0), .D(D), .PRE(1'b0), .Q(Q[7])); endmodule EOT +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 4 t:FD* @@ -54,6 +56,7 @@ logger -expect warning "Whitebox '\$paramod\\FDRE\\INIT=.*1' with \(\* abc9_flop logger -expect warning "Whitebox '\$paramod\\FDRE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 logger -expect warning "Whitebox 'FDSE' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 logger -expect warning "Whitebox '\$paramod\\FDSE_1\\INIT=.*1' with \(\* abc9_flop \*\) contains a \$dff cell with non-zero initial state -- this is not supported for ABC9 sequential synthesis. Treating as a blackbox\." 1 +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 8 t:FD* @@ -75,6 +78,7 @@ always @(posedge clk or posedge pre) endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDCE @@ -94,6 +98,7 @@ assign q = ~r; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDRE %co w:r %i @@ -111,6 +116,7 @@ assign q2 = r; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf design -load postopt select -assert-count 1 t:FDRE %co %a w:r %i @@ -128,6 +134,7 @@ assign o = r1 | r2; endmodule EOT proc +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -multiclock -map +/xilinx/cells_sim.v synth_xilinx -abc9 -dff -noiopad -noclkbuf diff --git a/tests/arch/xilinx/opt_lut_ins.ys b/tests/arch/xilinx/opt_lut_ins.ys index a01d02179..2328919a3 100644 --- a/tests/arch/xilinx/opt_lut_ins.ys +++ b/tests/arch/xilinx/opt_lut_ins.ys @@ -18,6 +18,7 @@ end EOF +read_verilog -lib +/xilinx/cells_sim.v equiv_opt -assert -map +/xilinx/cells_sim.v opt_lut_ins -tech xilinx design -load postopt diff --git a/tests/arch/xilinx/xilinx_dffopt.ys b/tests/arch/xilinx/xilinx_dffopt.ys index c09699411..9f0b27ced 100644 --- a/tests/arch/xilinx/xilinx_dffopt.ys +++ b/tests/arch/xilinx/xilinx_dffopt.ys @@ -5,7 +5,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -52,7 +52,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -100,7 +100,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -137,7 +137,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -183,7 +183,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; @@ -232,7 +232,7 @@ read_verilog << EOT module t0 (...); input wire clk; input wire [7:0] i; -output wire [7:0] o; +output wire [0:0] o; wire [7:0] tmp ; diff --git a/tests/opt/opt_dff_en.ys b/tests/opt/opt_dff_en.ys index 06ee6c63d..9538afcc2 100644 --- a/tests/opt/opt_dff_en.ys +++ b/tests/opt/opt_dff_en.ys @@ -6,7 +6,7 @@ module top(...); input CLK; input [1:0] D; -output [15:0] Q; +output [11:0] Q; input SRST; input ARST; input [1:0] CLR; diff --git a/tests/opt/opt_dff_mux.ys b/tests/opt/opt_dff_mux.ys index ed01bed59..f21f9e9b8 100644 --- a/tests/opt/opt_dff_mux.ys +++ b/tests/opt/opt_dff_mux.ys @@ -7,7 +7,7 @@ module top(...); input CLK; input NE, NS; input EN; -output [23:0] Q; +output [17:0] Q; input [23:0] D; input SRST; input ARST; diff --git a/tests/opt/opt_dff_qd.ys b/tests/opt/opt_dff_qd.ys index afc96c42f..7b0b4c224 100644 --- a/tests/opt/opt_dff_qd.ys +++ b/tests/opt/opt_dff_qd.ys @@ -7,7 +7,7 @@ module top(...); input CLK; input EN; (* init = 24'h555555 *) -output [23:0] Q; +output [19:0] Q; input SRST; input ARST; input [1:0] CLR; diff --git a/tests/techmap/dfflegalize_adlatch.ys b/tests/techmap/dfflegalize_adlatch.ys index b242cc809..559363301 100644 --- a/tests/techmap/dfflegalize_adlatch.ys +++ b/tests/techmap/dfflegalize_adlatch.ys @@ -12,7 +12,7 @@ $_DLATCH_PN1_ ff1 (.E(E), .R(R), .D(D), .Q(Q[1])); $_DLATCH_NP1_ ff2 (.E(E), .R(R), .D(D), .Q(Q[2])); endmodule -module top(input C, E, R, D, output [13:0] Q); +module top(input C, E, R, D, output [5:0] Q); adlatch0 adlatch0_(.E(E), .R(R), .D(D), .Q(Q[2:0])); adlatch1 adlatch1_(.E(E), .R(R), .D(D), .Q(Q[5:3])); endmodule diff --git a/tests/techmap/dfflegalize_adlatch_init.ys b/tests/techmap/dfflegalize_adlatch_init.ys index a55082d1d..8e371c528 100644 --- a/tests/techmap/dfflegalize_adlatch_init.ys +++ b/tests/techmap/dfflegalize_adlatch_init.ys @@ -12,7 +12,7 @@ $_DLATCH_PN1_ ff1 (.E(E), .R(R), .D(D), .Q(Q[1])); $_DLATCH_NP1_ ff2 (.E(E), .R(R), .D(D), .Q(Q[2])); endmodule -module top(input C, E, R, D, output [13:0] Q); +module top(input C, E, R, D, output [5:0] Q); adlatch0 adlatch0_(.E(E), .R(R), .D(D), .Q(Q[2:0])); adlatch1 adlatch1_(.E(E), .R(R), .D(D), .Q(Q[5:3])); endmodule diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index 04477eb14..b0a7d6b7e 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -17,9 +17,11 @@ EOT simplemap design -save orig +read_liberty -lib dfflibmap.lib + +equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib +equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib -#equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib -#equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib dfflibmap -prepare -liberty dfflibmap.lib equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib diff --git a/tests/techmap/dffunmap.ys b/tests/techmap/dffunmap.ys index b813078ee..247699f80 100644 --- a/tests/techmap/dffunmap.ys +++ b/tests/techmap/dffunmap.ys @@ -4,7 +4,7 @@ module top(...); input C, R, E, S; input [1:0] D; -output [20:0] Q; +output [17:0] Q; $dff #(.CLK_POLARITY(1'b0), .WIDTH(2)) ff0 (.CLK(C), .D(D), .Q(Q[1:0])); $dffe #(.CLK_POLARITY(1'b0), .EN_POLARITY(1'b0), .WIDTH(2)) ff1 (.CLK(C), .EN(E), .D(D), .Q(Q[3:2])); diff --git a/tests/techmap/zinit.ys b/tests/techmap/zinit.ys index bc07f40e6..af78709b2 100644 --- a/tests/techmap/zinit.ys +++ b/tests/techmap/zinit.ys @@ -13,6 +13,8 @@ $_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); $_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); $_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); +assign Q[8] = 0; + $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); $adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11])); endmodule @@ -44,6 +46,8 @@ $_DFF_PN1_ dff5 (.C(C), .D(D[0]), .R(R), .Q(Q[5])); $_DFF_PP0_ dff6 (.C(C), .D(D[0]), .R(R), .Q(Q[6])); $_DFF_PP1_ dff7 (.C(C), .D(D[0]), .R(R), .Q(Q[7])); +assign Q[8] = 0; + $adff #(.WIDTH(2), .CLK_POLARITY(1), .ARST_POLARITY(1'b0), .ARST_VALUE(2'b10)) dff8 (.CLK(C), .ARST(R), .D(D), .Q(Q[10:9])); $adff #(.WIDTH(2), .CLK_POLARITY(0), .ARST_POLARITY(1'b1), .ARST_VALUE(2'b01)) dff9 (.CLK(C), .ARST(R), .D(D), .Q(Q[12:11])); endmodule From 0113f44faaa5778afd0fa3afbdbf12f33f2cea4e Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 30 Aug 2022 13:56:05 +0200 Subject: [PATCH 7/7] Reenable existing equiv_opt tests --- tests/arch/ice40/bug1597.ys | 2 +- tests/arch/intel_alm/counter.ys | 4 ++-- tests/opt/opt_expr_xor.ys | 8 ++++---- tests/techmap/adff2dff.ys | 2 +- tests/techmap/dff2ff.ys | 2 +- tests/techmap/dfflegalize_aldff.ys | 4 ++-- tests/techmap/dfflegalize_aldff_init.ys | 8 ++++---- tests/techmap/dfflegalize_dffsr_init.ys | 24 +++++++++++----------- tests/techmap/dfflegalize_dlatchsr_init.ys | 14 ++++++------- tests/techmap/dfflegalize_sr_init.ys | 24 +++++++++++----------- tests/techmap/pmux2mux.ys | 2 +- tests/techmap/shiftx2mux.ys | 2 +- tests/techmap/zinit.ys | 10 ++++----- 13 files changed, 52 insertions(+), 54 deletions(-) diff --git a/tests/arch/ice40/bug1597.ys b/tests/arch/ice40/bug1597.ys index 73bc18eb2..c1509cabc 100644 --- a/tests/arch/ice40/bug1597.ys +++ b/tests/arch/ice40/bug1597.ys @@ -70,4 +70,4 @@ EOT read_verilog -lib +/ice40/cells_sim.v hierarchy -top top flatten -equiv_opt -multiclock -map +/ice40/cells_sim.v synth_ice40 +equiv_opt -assert -multiclock -map +/ice40/cells_sim.v synth_ice40 diff --git a/tests/arch/intel_alm/counter.ys b/tests/arch/intel_alm/counter.ys index 56c9cabb3..0a5b9356a 100644 --- a/tests/arch/intel_alm/counter.ys +++ b/tests/arch/intel_alm/counter.ys @@ -2,7 +2,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check +equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclonev -noiopad -noclkbuf # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd top # Constrain all select calls below inside the top module @@ -17,7 +17,7 @@ read_verilog ../common/counter.v hierarchy -top top proc flatten -equiv_opt -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check +equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd top # Constrain all select calls below inside the top module diff --git a/tests/opt/opt_expr_xor.ys b/tests/opt/opt_expr_xor.ys index a879f3ec9..8874f2775 100644 --- a/tests/opt/opt_expr_xor.ys +++ b/tests/opt/opt_expr_xor.ys @@ -10,7 +10,7 @@ design -save read select -assert-count 2 t:$xor select -assert-count 2 t:$xnor -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-none t:$xor select -assert-none t:$xnor @@ -19,7 +19,7 @@ select -assert-count 2 t:$not design -load read simplemap -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-none t:$_XOR_ select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ @@ -34,7 +34,7 @@ $_XNOR_ u1(.A(1'b1), .B(a), .Y(y[1])); endmodule EOT select -assert-count 2 t:$_XNOR_ -equiv_opt opt_expr +equiv_opt -assert opt_expr design -load postopt select -assert-none t:$_XNOR_ # NB: simplemap does $xnor -> $_XOR_+$_NOT_ select -assert-count 1 t:$_NOT_ @@ -49,7 +49,7 @@ assign y = a~^1'b0; assign z = a~^1'b1; endmodule EOT -equiv_opt opt_expr +equiv_opt -assert opt_expr # Single-bit $xor diff --git a/tests/techmap/adff2dff.ys b/tests/techmap/adff2dff.ys index 53f7d2f08..6d03d1963 100644 --- a/tests/techmap/adff2dff.ys +++ b/tests/techmap/adff2dff.ys @@ -16,4 +16,4 @@ EOT proc -equiv_opt -async2sync techmap -map +/adff2dff.v +#equiv_opt -assert -async2sync techmap -map +/adff2dff.v diff --git a/tests/techmap/dff2ff.ys b/tests/techmap/dff2ff.ys index 5adf14b07..6e7e6082b 100644 --- a/tests/techmap/dff2ff.ys +++ b/tests/techmap/dff2ff.ys @@ -13,4 +13,4 @@ EOT proc -equiv_opt techmap -map +/dff2ff.v +equiv_opt -assert techmap -map +/dff2ff.v diff --git a/tests/techmap/dfflegalize_aldff.ys b/tests/techmap/dfflegalize_aldff.ys index 1ee9e3af6..5be3e9742 100644 --- a/tests/techmap/dfflegalize_aldff.ys +++ b/tests/techmap/dfflegalize_aldff.ys @@ -24,8 +24,8 @@ design -save orig flatten equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ x equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ x -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ x +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ x # Convert everything to ALDFFs. diff --git a/tests/techmap/dfflegalize_aldff_init.ys b/tests/techmap/dfflegalize_aldff_init.ys index f4db8dd32..ffa7cbf16 100644 --- a/tests/techmap/dfflegalize_aldff_init.ys +++ b/tests/techmap/dfflegalize_aldff_init.ys @@ -26,10 +26,10 @@ equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFF_PP_ 1 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 0 equiv_opt -assert -multiclock dfflegalize -cell $_ALDFFE_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to ALDFFs. diff --git a/tests/techmap/dfflegalize_dffsr_init.ys b/tests/techmap/dfflegalize_dffsr_init.ys index ce5a32f76..b6160bb87 100644 --- a/tests/techmap/dfflegalize_dffsr_init.ys +++ b/tests/techmap/dfflegalize_dffsr_init.ys @@ -41,18 +41,18 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP0_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFF_PP1_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP0P_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 0 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFE_PP1P_ 1 -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to ADFFs. diff --git a/tests/techmap/dfflegalize_dlatchsr_init.ys b/tests/techmap/dfflegalize_dlatchsr_init.ys index b38a9eb3b..da4ca164e 100644 --- a/tests/techmap/dfflegalize_dlatchsr_init.ys +++ b/tests/techmap/dfflegalize_dlatchsr_init.ys @@ -14,7 +14,7 @@ $_DLATCHSR_PNP_ ff2 (.E(E), .R(R), .S(S), .D(D), .Q(Q[2])); $_DLATCHSR_NPP_ ff3 (.E(E), .R(R), .S(S), .D(D), .Q(Q[3])); endmodule -module top(input C, E, R, S, D, output [17:0] Q); +module top(input C, E, R, S, D, output [7:0] Q); dlatchsr0 dlatchsr0_(.E(E), .R(R), .S(S), .D(D), .Q(Q[3:0])); dlatchsr1 dlatchsr1_(.E(E), .R(R), .S(S), .D(D), .Q(Q[7:4])); endmodule @@ -23,12 +23,12 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 # Convert everything to ADLATCHs. diff --git a/tests/techmap/dfflegalize_sr_init.ys b/tests/techmap/dfflegalize_sr_init.ys index 9d724de29..7cb1c629d 100644 --- a/tests/techmap/dfflegalize_sr_init.ys +++ b/tests/techmap/dfflegalize_sr_init.ys @@ -21,18 +21,18 @@ EOT design -save orig flatten -#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 -#equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_SR_PP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP0_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCH_PP1_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DLATCHSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSR_PPP_ 1 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 0 +equiv_opt -assert -multiclock dfflegalize -cell $_DFFSRE_PPPP_ 1 # Convert everything to SRs. diff --git a/tests/techmap/pmux2mux.ys b/tests/techmap/pmux2mux.ys index 1714a6b87..1e08485ef 100644 --- a/tests/techmap/pmux2mux.ys +++ b/tests/techmap/pmux2mux.ys @@ -12,4 +12,4 @@ output [3:0] O; endmodule EOT -equiv_opt techmap -map +/pmux2mux.v +equiv_opt -assert techmap -map +/pmux2mux.v diff --git a/tests/techmap/shiftx2mux.ys b/tests/techmap/shiftx2mux.ys index f749e79b2..680681297 100644 --- a/tests/techmap/shiftx2mux.ys +++ b/tests/techmap/shiftx2mux.ys @@ -106,4 +106,4 @@ endmodule EOT opt wreduce -equiv_opt techmap +equiv_opt -assert techmap diff --git a/tests/techmap/zinit.ys b/tests/techmap/zinit.ys index af78709b2..562db0776 100644 --- a/tests/techmap/zinit.ys +++ b/tests/techmap/zinit.ys @@ -95,9 +95,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23])); endmodule EOT -#equiv_opt -assert -multiclock zinit -#design -load postopt -zinit +equiv_opt -assert -multiclock zinit +design -load postopt select -assert-count 48 t:$_NOT_ select -assert-count 0 w:Q a:init %i @@ -142,9 +141,8 @@ $_SDFFE_PP1P_ dff23(.C(C), .D(D[0]),.E(E), .R(R), .Q(Q[23])); endmodule EOT -#equiv_opt -assert -multiclock zinit -#design -load postopt -zinit +equiv_opt -assert -multiclock zinit +design -load postopt select -assert-count 0 t:$_NOT_ select -assert-count 1 w:Q a:init=24'b0 %i