From b604c97b33de1785a10b2df2b3eaa48f2bee0719 Mon Sep 17 00:00:00 2001 From: Archie Date: Tue, 14 Jun 2022 14:17:00 +0100 Subject: [PATCH 01/26] Add check for BLIF with no model name --- frontends/blif/blifparse.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index 19844bda6..73d1f0ea7 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -166,7 +166,10 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool goto error; module = new RTLIL::Module; lastcell = nullptr; - module->name = RTLIL::escape_id(strtok(NULL, " \t\r\n")); + char *name = strtok(NULL, " \t\r\n"); + if (name == nullptr) + goto error; + module->name = RTLIL::escape_id(name); obj_attributes = &module->attributes; obj_parameters = nullptr; if (design->module(module->name)) From 4542d517913999754827472f1f0b6a5520fcc9e6 Mon Sep 17 00:00:00 2001 From: Archie Date: Fri, 17 Jun 2022 20:07:02 +0100 Subject: [PATCH 02/26] Adding testcase for issue 3374 --- tests/blif/bug3374.ys | 3 +++ 1 file changed, 3 insertions(+) create mode 100644 tests/blif/bug3374.ys diff --git a/tests/blif/bug3374.ys b/tests/blif/bug3374.ys new file mode 100644 index 000000000..d7d8c765b --- /dev/null +++ b/tests/blif/bug3374.ys @@ -0,0 +1,3 @@ +read_blif < Date: Mon, 20 Jun 2022 21:50:26 +0100 Subject: [PATCH 03/26] Adding expected error message. --- tests/blif/bug3374.ys | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/blif/bug3374.ys b/tests/blif/bug3374.ys index d7d8c765b..792d4de20 100644 --- a/tests/blif/bug3374.ys +++ b/tests/blif/bug3374.ys @@ -1,3 +1,4 @@ +logger -expect error "Syntax error in line 1!" 1 read_blif < Date: Sun, 21 Aug 2022 23:18:20 -0500 Subject: [PATCH 04/26] Adding check for BLIF names command input plane size. --- frontends/blif/blifparse.cc | 9 ++++++++- tests/blif/bug3385.ys | 9 +++++++++ 2 files changed, 17 insertions(+), 1 deletion(-) create mode 100644 tests/blif/bug3385.ys diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index 73d1f0ea7..52742660e 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -21,6 +21,8 @@ YOSYS_NAMESPACE_BEGIN +const int lut_input_plane_limit = 12; + static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count, std::istream &f) { string strbuf; @@ -513,6 +515,11 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool sopmode = -1; lastcell = sopcell; } + else if (input_sig.size() > lut_input_plane_limit) + { + err_reason = stringf("names' input plane must have fewer than 13 signals."); + goto error_with_reason; + } else { RTLIL::Cell *cell = module->addCell(NEW_ID, ID($lut)); @@ -576,7 +583,7 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool if (lutptr) { - if (input_len > 12) + if (input_len > lut_input_plane_limit) goto error; for (int i = 0; i < (1 << input_len); i++) { diff --git a/tests/blif/bug3385.ys b/tests/blif/bug3385.ys new file mode 100644 index 000000000..e1e45983d --- /dev/null +++ b/tests/blif/bug3385.ys @@ -0,0 +1,9 @@ +logger -expect error "Syntax error in line 4: names' input plane must have fewer than 13 signals." 1 +read_blif < Date: Sun, 2 Oct 2022 21:59:46 +0200 Subject: [PATCH 05/26] Changing error reason string to be based on lut input plane limit constant. --- frontends/blif/blifparse.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index 52742660e..fe4c9078a 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -517,7 +517,7 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool } else if (input_sig.size() > lut_input_plane_limit) { - err_reason = stringf("names' input plane must have fewer than 13 signals."); + err_reason = stringf("names' input plane must have fewer than %d signals.", lut_input_plane_limit + 1); goto error_with_reason; } else From 925f92918af783af71d5c9f1f358f79de5c20f04 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 6 Oct 2022 15:36:35 +0200 Subject: [PATCH 06/26] 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 07/26] 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 08/26] 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 09/26] 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 10/26] 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 11/26] 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 12/26] 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 From 090228a6a12e1a671a5465850d3f2e410d302ae0 Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Mon, 10 Oct 2022 00:47:42 +0200 Subject: [PATCH 13/26] Fix handling of verific -L options, add implicit "-L work" Signed-off-by: Claire Xenia Wolf --- frontends/verific/verific.cc | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 820ac042c..1b9db8772 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -2791,6 +2791,20 @@ struct VerificPass : public Pass { } veri_file::RemoveAllLOptions(); + veri_file::AddLOption("work"); + for (int i = argidx; i < GetSize(args); i++) + { + if (args[i] == "-work" && i+1 < GetSize(args)) { + ++i; + continue; + } + if (args[i] == "-L" && i+1 < GetSize(args)) { + if (args[++i] == "work") + veri_file::RemoveAllLOptions(); + continue; + } + break; + } for (; argidx < GetSize(args); argidx++) { if (args[argidx] == "-work" && argidx+1 < GetSize(args)) { From 03df1ac72be66c41521023ea18f99cebf2c189d4 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 10 Oct 2022 16:31:29 +0200 Subject: [PATCH 14/26] fix whitespace --- frontends/blif/blifparse.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index fe4c9078a..ebbe082a2 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -517,7 +517,7 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool } else if (input_sig.size() > lut_input_plane_limit) { - err_reason = stringf("names' input plane must have fewer than %d signals.", lut_input_plane_limit + 1); + err_reason = stringf("names' input plane must have fewer than %d signals.", lut_input_plane_limit + 1); goto error_with_reason; } else From 7a73133c9f79d6cbc99635f20e5b7ad76d43a0de Mon Sep 17 00:00:00 2001 From: Aki Van Ness Date: Mon, 10 Oct 2022 10:41:11 -0400 Subject: [PATCH 15/26] backends: protobuf: removed protobuf backend --- Makefile | 4 - backends/protobuf/.gitignore | 2 - backends/protobuf/Makefile.inc | 10 - backends/protobuf/protobuf.cc | 371 --------------------------------- misc/yosys.proto | 175 ---------------- 5 files changed, 562 deletions(-) delete mode 100644 backends/protobuf/.gitignore delete mode 100644 backends/protobuf/Makefile.inc delete mode 100644 backends/protobuf/protobuf.cc delete mode 100644 misc/yosys.proto diff --git a/Makefile b/Makefile index 9e1dc8207..b78cb7cd1 100644 --- a/Makefile +++ b/Makefile @@ -23,7 +23,6 @@ DISABLE_VERIFIC_EXTENSIONS := 0 DISABLE_VERIFIC_VHDL := 0 ENABLE_COVER := 1 ENABLE_LIBYOSYS := 0 -ENABLE_PROTOBUF := 0 ENABLE_ZLIB := 1 # python wrappers @@ -544,9 +543,6 @@ LDLIBS += $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -lz endif endif -ifeq ($(ENABLE_PROTOBUF),1) -LDLIBS += $(shell pkg-config --cflags --libs protobuf) -endif ifeq ($(ENABLE_COVER),1) CXXFLAGS += -DYOSYS_ENABLE_COVER diff --git a/backends/protobuf/.gitignore b/backends/protobuf/.gitignore deleted file mode 100644 index 849b38d45..000000000 --- a/backends/protobuf/.gitignore +++ /dev/null @@ -1,2 +0,0 @@ -yosys.pb.cc -yosys.pb.h diff --git a/backends/protobuf/Makefile.inc b/backends/protobuf/Makefile.inc deleted file mode 100644 index 9cac9dcaa..000000000 --- a/backends/protobuf/Makefile.inc +++ /dev/null @@ -1,10 +0,0 @@ -ifeq ($(ENABLE_PROTOBUF),1) - -backends/protobuf/yosys.pb.cc backends/protobuf/yosys.pb.h: misc/yosys.proto - $(Q) cd misc && protoc --cpp_out "../backends/protobuf" yosys.proto - -backends/protobuf/protobuf.cc: backends/protobuf/yosys.pb.h - -OBJS += backends/protobuf/protobuf.o backends/protobuf/yosys.pb.o - -endif diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc deleted file mode 100644 index 384ce2e8e..000000000 --- a/backends/protobuf/protobuf.cc +++ /dev/null @@ -1,371 +0,0 @@ -/* - * yosys -- Yosys Open SYnthesis Suite - * - * Copyright (C) 2012 Claire Xenia Wolf - * Copyright (C) 2018 Serge Bazanski - * - * Permission to use, copy, modify, and/or distribute this software for any - * purpose with or without fee is hereby granted, provided that the above - * copyright notice and this permission notice appear in all copies. - * - * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES - * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF - * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR - * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES - * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN - * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF - * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. - * - */ - -#include - -#include "kernel/rtlil.h" -#include "kernel/register.h" -#include "kernel/sigtools.h" -#include "kernel/celltypes.h" -#include "kernel/cellaigs.h" -#include "kernel/log.h" -#include "yosys.pb.h" - -USING_YOSYS_NAMESPACE -PRIVATE_NAMESPACE_BEGIN - -struct ProtobufDesignSerializer -{ - bool aig_mode_; - bool use_selection_; - yosys::pb::Design *pb_; - - Design *design_; - Module *module_; - - SigMap sigmap_; - int sigidcounter_; - dict sigids_; - pool aig_models_; - - - ProtobufDesignSerializer(bool use_selection, bool aig_mode) : - aig_mode_(aig_mode), use_selection_(use_selection) { } - - string get_name(IdString name) - { - return RTLIL::unescape_id(name); - } - - - void serialize_parameters(google::protobuf::Map *out, - const dict ¶meters) - { - for (auto ¶m : parameters) { - std::string key = get_name(param.first); - - - yosys::pb::Parameter pb_param; - - if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0) { - pb_param.set_str(param.second.decode_string()); - } else if (GetSize(param.second.bits) > 64) { - pb_param.set_str(param.second.as_string()); - } else { - pb_param.set_int_(param.second.as_int()); - } - - (*out)[key] = pb_param; - } - } - - void get_bits(yosys::pb::BitVector *out, SigSpec sig) - { - for (auto bit : sigmap_(sig)) { - auto sig = out->add_signal(); - - // Constant driver. - if (bit.wire == nullptr) { - if (bit == State::S0) sig->set_constant(sig->CONSTANT_DRIVER_LOW); - else if (bit == State::S1) sig->set_constant(sig->CONSTANT_DRIVER_HIGH); - else if (bit == State::Sz) sig->set_constant(sig->CONSTANT_DRIVER_Z); - else sig->set_constant(sig->CONSTANT_DRIVER_X); - continue; - } - - // Signal - give it a unique identifier. - if (sigids_.count(bit) == 0) { - sigids_[bit] = sigidcounter_++; - } - sig->set_id(sigids_[bit]); - } - } - - void serialize_module(yosys::pb::Module* out, Module *module) - { - module_ = module; - log_assert(module_->design == design_); - sigmap_.set(module_); - sigids_.clear(); - sigidcounter_ = 0; - - serialize_parameters(out->mutable_attribute(), module_->attributes); - - for (auto n : module_->ports) { - Wire *w = module->wire(n); - if (use_selection_ && !module_->selected(w)) - continue; - - yosys::pb::Module::Port pb_port; - pb_port.set_direction(w->port_input ? w->port_output ? - yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT : yosys::pb::DIRECTION_OUTPUT); - get_bits(pb_port.mutable_bits(), w); - (*out->mutable_port())[get_name(n)] = pb_port; - } - - for (auto c : module_->cells()) { - if (use_selection_ && !module_->selected(c)) - continue; - - yosys::pb::Module::Cell pb_cell; - pb_cell.set_hide_name(c->name[0] == '$'); - pb_cell.set_type(get_name(c->type)); - - if (aig_mode_) { - Aig aig(c); - if (aig.name.empty()) - continue; - pb_cell.set_model(aig.name); - aig_models_.insert(aig); - } - serialize_parameters(pb_cell.mutable_parameter(), c->parameters); - serialize_parameters(pb_cell.mutable_attribute(), c->attributes); - - if (c->known()) { - for (auto &conn : c->connections()) { - yosys::pb::Direction direction = yosys::pb::DIRECTION_OUTPUT; - if (c->input(conn.first)) - direction = c->output(conn.first) ? yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT; - (*pb_cell.mutable_port_direction())[get_name(conn.first)] = direction; - } - } - for (auto &conn : c->connections()) { - yosys::pb::BitVector vec; - get_bits(&vec, conn.second); - (*pb_cell.mutable_connection())[get_name(conn.first)] = vec; - } - - (*out->mutable_cell())[get_name(c->name)] = pb_cell; - } - - for (auto w : module_->wires()) { - if (use_selection_ && !module_->selected(w)) - continue; - - auto netname = out->add_netname(); - netname->set_hide_name(w->name[0] == '$'); - get_bits(netname->mutable_bits(), w); - serialize_parameters(netname->mutable_attributes(), w->attributes); - } - } - - - void serialize_models(google::protobuf::Map *models) - { - for (auto &aig : aig_models_) { - yosys::pb::Model pb_model; - for (auto &node : aig.nodes) { - auto pb_node = pb_model.add_node(); - if (node.portbit >= 0) { - if (node.inverter) { - pb_node->set_type(pb_node->TYPE_NPORT); - } else { - pb_node->set_type(pb_node->TYPE_PORT); - } - auto port = pb_node->mutable_port(); - port->set_portname(log_id(node.portname)); - port->set_bitindex(node.portbit); - } else if (node.left_parent < 0 && node.right_parent < 0) { - if (node.inverter) { - pb_node->set_type(pb_node->TYPE_TRUE); - } else { - pb_node->set_type(pb_node->TYPE_FALSE); - } - } else { - if (node.inverter) { - pb_node->set_type(pb_node->TYPE_NAND); - } else { - pb_node->set_type(pb_node->TYPE_AND); - } - auto gate = pb_node->mutable_gate(); - gate->set_left(node.left_parent); - gate->set_right(node.right_parent); - } - for (auto &op : node.outports) { - auto pb_op = pb_node->add_out_port(); - pb_op->set_name(log_id(op.first)); - pb_op->set_bit_index(op.second); - } - } - (*models)[aig.name] = pb_model; - } - } - - void serialize_design(yosys::pb::Design *pb, Design *design) - { - GOOGLE_PROTOBUF_VERIFY_VERSION; - pb_ = pb; - pb_->Clear(); - pb_->set_creator(yosys_version_str); - - design_ = design; - design_->sort(); - - auto modules = use_selection_ ? design_->selected_modules() : design_->modules(); - for (auto mod : modules) { - yosys::pb::Module pb_mod; - serialize_module(&pb_mod, mod); - (*pb->mutable_modules())[mod->name.str()] = pb_mod; - } - - serialize_models(pb_->mutable_models()); - } -}; - -struct ProtobufBackend : public Backend { - ProtobufBackend(): Backend("protobuf", "write design to a Protocol Buffer file") { } - void help() override - { - // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| - log("\n"); - log(" write_protobuf [options] [filename]\n"); - log("\n"); - log("Write a JSON netlist of the current design.\n"); - log("\n"); - log(" -aig\n"); - log(" include AIG models for the different gate types\n"); - log("\n"); - log(" -text\n"); - log(" output protobuf in Text/ASCII representation\n"); - log("\n"); - log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n"); - log("Yosys source code distribution.\n"); - log("\n"); - } - void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) override - { - bool aig_mode = false; - bool text_mode = false; - - size_t argidx; - for (argidx = 1; argidx < args.size(); argidx++) { - if (args[argidx] == "-aig") { - aig_mode = true; - continue; - } - if (args[argidx] == "-text") { - text_mode = true; - continue; - } - break; - } - extra_args(f, filename, args, argidx, !text_mode); - - log_header(design, "Executing Protobuf backend.\n"); - - yosys::pb::Design pb; - ProtobufDesignSerializer serializer(false, aig_mode); - serializer.serialize_design(&pb, design); - - if (text_mode) { - string out; - google::protobuf::TextFormat::PrintToString(pb, &out); - *f << out; - } else { - pb.SerializeToOstream(f); - } - } -} ProtobufBackend; - -struct ProtobufPass : public Pass { - ProtobufPass() : Pass("protobuf", "write design in Protobuf format") { } - void help() override - { - // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| - log("\n"); - log(" protobuf [options] [selection]\n"); - log("\n"); - log("Write a JSON netlist of all selected objects.\n"); - log("\n"); - log(" -o \n"); - log(" write to the specified file.\n"); - log("\n"); - log(" -aig\n"); - log(" include AIG models for the different gate types\n"); - log("\n"); - log(" -text\n"); - log(" output protobuf in Text/ASCII representation\n"); - log("\n"); - log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n"); - log("Yosys source code distribution.\n"); - log("\n"); - } - void execute(std::vector args, RTLIL::Design *design) override - { - std::string filename; - bool aig_mode = false; - bool text_mode = false; - - size_t argidx; - for (argidx = 1; argidx < args.size(); argidx++) - { - if (args[argidx] == "-o" && argidx+1 < args.size()) { - filename = args[++argidx]; - continue; - } - if (args[argidx] == "-aig") { - aig_mode = true; - continue; - } - if (args[argidx] == "-text") { - text_mode = true; - continue; - } - break; - } - extra_args(args, argidx, design); - - std::ostream *f; - std::stringstream buf; - - if (!filename.empty()) { - rewrite_filename(filename); - std::ofstream *ff = new std::ofstream; - ff->open(filename.c_str(), text_mode ? std::ofstream::trunc : (std::ofstream::trunc | std::ofstream::binary)); - if (ff->fail()) { - delete ff; - log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno)); - } - f = ff; - } else { - f = &buf; - } - - yosys::pb::Design pb; - ProtobufDesignSerializer serializer(true, aig_mode); - serializer.serialize_design(&pb, design); - - if (text_mode) { - string out; - google::protobuf::TextFormat::PrintToString(pb, &out); - *f << out; - } else { - pb.SerializeToOstream(f); - } - - if (!filename.empty()) { - delete f; - } else { - log("%s", buf.str().c_str()); - } - } -} ProtobufPass; - -PRIVATE_NAMESPACE_END; diff --git a/misc/yosys.proto b/misc/yosys.proto deleted file mode 100644 index a583e6265..000000000 --- a/misc/yosys.proto +++ /dev/null @@ -1,175 +0,0 @@ -// -// yosys -- Yosys Open SYnthesis Suite -// -// Copyright (C) 2018 Serge Bazanski -// -// Permission to use, copy, modify, and/or distribute this software for any -// purpose with or without fee is hereby granted, provided that the above -// copyright notice and this permission notice appear in all copies. -// -// THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES -// WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF -// MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR -// ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES -// WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN -// ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF -// OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. -// - -/// Protobuf definition of Yosys RTLIL dump/restore format for RTL designs. - -syntax = "proto3"; - -package yosys.pb; - -// Port direction. -enum Direction { - DIRECTION_INVALID = 0; - DIRECTION_INPUT = 1; - DIRECTION_OUTPUT = 2; - DIRECTION_INOUT = 3; -} - -// A freeform parameter/attribute value. -message Parameter { - oneof value { - int64 int = 1; - string str = 2; - } -} - -// A signal in the design - either a unique identifier for one, or a constant -// driver (low or high). -message Signal { - // A constant signal driver in the design. - enum ConstantDriver { - CONSTANT_DRIVER_INVALID = 0; - CONSTANT_DRIVER_LOW = 1; - CONSTANT_DRIVER_HIGH = 2; - CONSTANT_DRIVER_Z = 3; - CONSTANT_DRIVER_X = 4; - } - oneof type { - // Signal uniquely identified by ID number. - int64 id = 1; - // Constant driver. - ConstantDriver constant = 2; - } -} - -// A vector of signals. -message BitVector { - repeated Signal signal = 1; -} - -// A netlist module. -message Module { - // Freeform attributes. - map attribute = 1; - - // Named ports in this module. - message Port { - Direction direction = 1; - BitVector bits = 2; - } - map port = 2; - - // Named cells in this module. - message Cell { - // Set to true when the name of this cell is automatically created and - // likely not of interest for a regular user. - bool hide_name = 1; - string type = 2; - // Set if this module has an AIG model available. - string model = 3; - // Freeform parameters. - map parameter = 4; - // Freeform attributes. - map attribute = 5; - - /// Ports of the cell. - // Direction of the port, if interface is known. - map port_direction = 6; - // Connection of named port to signal(s). - map connection = 7; - } - map cell = 3; - - // Nets in this module. - message Netname { - // Set to true when the name of this net is automatically created and - // likely not of interest for a regular user. - bool hide_name = 1; - // Signal(s) that make up this net. - BitVector bits = 2; - // Freeform attributes. - map attributes = 3; - } - repeated Netname netname = 4; -} - -// And-Inverter-Graph model. -message Model { - message Node { - // Type of AIG node - or, what its' value is. - enum Type { - TYPE_INVALID = 0; - // The node's value is the value of the specified input port bit. - TYPE_PORT = 1; - // The node's value is the inverted value of the specified input - // port bit. - TYPE_NPORT = 2; - // The node's value is the ANDed value of specified nodes. - TYPE_AND = 3; - // The node's value is the NANDed value of specified nodes. - TYPE_NAND = 4; - // The node's value is a constant 1. - TYPE_TRUE = 5; - // The node's value is a constant 0. - TYPE_FALSE = 6; - }; - Type type = 1; - - message Port { - // Name of port. - string portname = 1; - // Bit index in port. - int64 bitindex = 2; - } - message Gate { - // Node index of left side of operation. - int64 left = 1; - // Node index of right side of operation. - int64 right = 2; - } - oneof node { - // Set for PORT, NPORT - Port port = 2; - // Set for AND, NAND. - Gate gate = 3; - } - - // Set when the node drives given output port(s). - message OutPort { - // Name of port. - string name = 1; - // Bit index in port. - int64 bit_index = 2; - } - repeated OutPort out_port = 4; - } - - // List of AIG nodes - each is explicitely numbered by its' index in this - // array. - repeated Node node = 1; -} - -// A Yosys design netlist dumped from RTLIL. -message Design { - // Human-readable freeform 'remark' string. - string creator = 1; - // List of named modules in design. - map modules = 2; - // List of named AIG models in design (if AIG export enabled). - map models = 3; -} From 5c7a1eda92269aaad372a662b0e32758b2a4e014 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 11 Oct 2022 00:24:29 +0000 Subject: [PATCH 16/26] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index b78cb7cd1..3b682b752 100644 --- a/Makefile +++ b/Makefile @@ -131,7 +131,7 @@ LDLIBS += -lrt endif endif -YOSYS_VER := 0.22+4 +YOSYS_VER := 0.22+17 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From f35c062354668b817a0f911fe9158b6b1e150617 Mon Sep 17 00:00:00 2001 From: Aki Van Ness Date: Tue, 11 Oct 2022 06:13:41 -0400 Subject: [PATCH 17/26] github: issues: added an OS dropdown to the issue template --- .github/ISSUE_TEMPLATE/bug_report.yml | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/.github/ISSUE_TEMPLATE/bug_report.yml b/.github/ISSUE_TEMPLATE/bug_report.yml index ca9cb4811..27cfd09b7 100644 --- a/.github/ISSUE_TEMPLATE/bug_report.yml +++ b/.github/ISSUE_TEMPLATE/bug_report.yml @@ -25,6 +25,19 @@ body: validations: required: true + - type: dropdown + id: os + attributes: + label: On which OS did this happen? + options: + - Linux + - macOS + - Windows + - BSD + multiple: true + validations: + required: true + - type: markdown attributes: value: > @@ -60,4 +73,3 @@ body: description: "Please describe how the behavior you see differs from the expected behavior." validations: required: true - From 4d334fd3e352f86e46e5810ae021b9ba0bf03752 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 12 Oct 2022 19:01:24 +0200 Subject: [PATCH 18/26] smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs The witness metadata was missing fine grained FFs completely and for coarse grained FFs where the output connection has multiple chunks it lacked the offset of the chunk within the SMT expression. This fixes both, the later by adding an "smtoffset" field to the metadata. --- backends/smt2/smt2.cc | 13 ++++++++++--- backends/smt2/smtbmc.py | 5 +++-- backends/smt2/smtio.py | 9 +++++++++ tests/various/smtlib2_module-expected.smt2 | 14 +++++++------- 4 files changed, 29 insertions(+), 12 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 54783cf1b..7434b13da 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -559,6 +559,9 @@ struct Smt2Worker if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) { registers.insert(cell); + SigBit q_bit = cell->getPort(ID::Q); + if (q_bit.is_wire()) + decls.push_back(witness_signal("reg", 1, 0, "", idcounter, q_bit.wire)); makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q))); register_bool(cell->getPort(ID::Q), idcounter++); recursive_cells.erase(cell); @@ -589,9 +592,12 @@ struct Smt2Worker if (cell->type.in(ID($ff), ID($dff))) { registers.insert(cell); - for (auto chunk : cell->getPort(ID::Q).chunks()) + int smtoffset = 0; + for (auto chunk : cell->getPort(ID::Q).chunks()) { if (chunk.is_wire()) - decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire)); + decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset)); + smtoffset += chunk.width; + } makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q))); register_bv(cell->getPort(ID::Q), idcounter++); recursive_cells.erase(cell); @@ -1490,7 +1496,7 @@ struct Smt2Worker return path; } - std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire) + std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire, int smtoffset = 0) { std::vector hiername; const char *wire_name = wire->name.c_str(); @@ -1508,6 +1514,7 @@ struct Smt2Worker { "offset", offset }, { "width", width }, { "smtname", smtname.empty() ? json11::Json(smtid) : json11::Json(smtname) }, + { "smtoffset", smtoffset }, { "path", witness_path(wire) }, }}).dump(line); line += "\n"; diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 5f05287de..ac329053f 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -669,7 +669,7 @@ if inywfile is not None: if common_end <= common_offset: continue - smt_expr = smt.net_expr(topmod, f"s{t}", wire["smtpath"]) + smt_expr = smt.witness_net_expr(topmod, f"s{t}", wire) if not smt_bool: slice_high = common_end - offset - 1 @@ -1267,7 +1267,8 @@ def write_yw_trace(steps_start, steps_stop, index, allregs=False): sigs = seqs for sig in sigs: - step_values[sig["sig"]] = smt.bv2bin(smt.get(smt.net_expr(topmod, f"s{k}", sig["smtpath"]))) + value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig))) + step_values[sig["sig"]] = value yw.step(step_values) yw.end_trace() diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 9af454cca..f5cfe436d 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -958,6 +958,15 @@ class SmtIo: nextbase = "(|%s_h %s| %s)" % (mod, path[0], base) return self.net_expr(nextmod, nextbase, path[1:]) + def witness_net_expr(self, mod, base, witness): + net = self.net_expr(mod, base, witness["smtpath"]) + is_bool = self.net_width(mod, witness["smtpath"]) == 1 + if is_bool: + assert witness["width"] == 1 + assert witness["smtoffset"] == 0 + return net + return "((_ extract %d %d) %s)" % (witness["smtoffset"] + witness["width"] - 1, witness["smtoffset"], net) + def net_width(self, mod, net_path): for i in range(len(net_path)-1): assert mod in self.modinfo diff --git a/tests/various/smtlib2_module-expected.smt2 b/tests/various/smtlib2_module-expected.smt2 index 74e2f3fca..494e7cda0 100644 --- a/tests/various/smtlib2_module-expected.smt2 +++ b/tests/various/smtlib2_module-expected.smt2 @@ -4,14 +4,14 @@ (declare-fun |smtlib2_is| (|smtlib2_s|) Bool) (declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a ; yosys-smt2-input a 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "type": "input", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "smtoffset": 0, "type": "input", "width": 8} (define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state)) (declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b ; yosys-smt2-input b 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "type": "input", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "smtoffset": 0, "type": "input", "width": 8} (define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state)) ; yosys-smt2-output add 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "type": "blackbox", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "smtoffset": 0, "type": "blackbox", "width": 8} (define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -19,7 +19,7 @@ (bvadd a b) )) ; yosys-smt2-output eq 1 -; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "type": "blackbox", "width": 1} +; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "smtoffset": 0, "type": "blackbox", "width": 1} (define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -27,7 +27,7 @@ (= a b) )) ; yosys-smt2-output sub 8 -; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "type": "blackbox", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "smtoffset": 0, "type": "blackbox", "width": 8} (define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let ( (|a| (|smtlib2_n a| state)) (|b| (|smtlib2_n b| state)) @@ -49,10 +49,10 @@ (declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub (declare-fun |uut_h s| (|uut_s|) |smtlib2_s|) ; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26 -; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "type": "init", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "smtoffset": 0, "type": "init", "width": 8} (declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a ; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41 -; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "type": "init", "width": 8} +; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "smtoffset": 0, "type": "init", "width": 8} (declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b (define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2 (define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9 From 2e837956dc055bc517d5bd5cd75b72bf0eb62272 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Thu, 13 Oct 2022 00:25:23 +0000 Subject: [PATCH 19/26] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 3b682b752..28e263909 100644 --- a/Makefile +++ b/Makefile @@ -131,7 +131,7 @@ LDLIBS += -lrt endif endif -YOSYS_VER := 0.22+17 +YOSYS_VER := 0.22+29 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From 922f8b614a8922d5c482f8e02a0bf0df8826b2d2 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 14 Oct 2022 16:54:57 +0200 Subject: [PATCH 20/26] Add option to import all cells from all libraries --- frontends/verific/verific.cc | 31 ++++++++++++++++++++++++++++++- 1 file changed, 30 insertions(+), 1 deletion(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 1b9db8772..3ca124a87 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -2533,6 +2533,10 @@ struct VerificPass : public Pass { log(" -fullinit\n"); log(" Keep all register initializations, even those for non-FF registers.\n"); log("\n"); + log(" -cells\n"); + log(" Import all cell definitions from Verific loaded libraries even if they are\n"); + log(" unused in design. Useful with \"-edif\" option.\n"); + log("\n"); log(" -chparam name value \n"); log(" Elaborate the specified top modules (all modules when -all given) using\n"); log(" this parameter value. Modules on which this parameter does not exist will\n"); @@ -3052,7 +3056,7 @@ struct VerificPass : public Pass { bool mode_all = false, mode_gates = false, mode_keep = false; bool mode_nosva = false, mode_names = false, mode_verific = false; bool mode_autocover = false, mode_fullinit = false; - bool flatten = false, extnets = false; + bool flatten = false, extnets = false, mode_cells = false; string dumpfile; string ppfile; Map parameters(STRING_HASH); @@ -3098,6 +3102,10 @@ struct VerificPass : public Pass { mode_fullinit = true; continue; } + if (args[argidx] == "-cells") { + mode_cells = true; + continue; + } if (args[argidx] == "-chparam" && argidx+2 < GetSize(args)) { const std::string &key = args[++argidx]; const std::string &value = args[++argidx]; @@ -3218,6 +3226,27 @@ struct VerificPass : public Pass { } delete netlists; } + if (mode_cells) { + log("Importing all cells.\n"); + Libset *gls = Libset::Global() ; + MapIter it ; + Library *l ; + FOREACH_LIBRARY_OF_LIBSET(gls,it,l) { + MapIter mi ; + Verific::Cell *c ; + FOREACH_CELL_OF_LIBRARY(l,mi,c) { + MapIter ni ; + if (c->NumOfNetlists() == 1) { + c->GetFirstNetlist()->SetName(""); + } + Netlist *nl; + FOREACH_NETLIST_OF_CELL(c, ni, nl) { + if (nl) + nl_todo.emplace(nl->CellBaseName(), nl); + } + } + } + } if (!verific_error_msg.empty()) goto check_error; From 48628fbf5a387deeb5dff18931628d19efd685a0 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 14 Oct 2022 17:41:24 +0200 Subject: [PATCH 21/26] Skip verific primitives and operators import by default --- frontends/verific/verific.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 3ca124a87..71b87755d 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -3235,6 +3235,7 @@ struct VerificPass : public Pass { MapIter mi ; Verific::Cell *c ; FOREACH_CELL_OF_LIBRARY(l,mi,c) { + if (!mode_verific && (l == Library::Primitives() || l == Library::Operators())) continue; MapIter ni ; if (c->NumOfNetlists() == 1) { c->GetFirstNetlist()->SetName(""); From d02ae8f2fc78f43e870e2d67d472b3e7039e2bbe Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Sat, 15 Oct 2022 00:24:26 +0000 Subject: [PATCH 22/26] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 28e263909..e41e5ff94 100644 --- a/Makefile +++ b/Makefile @@ -131,7 +131,7 @@ LDLIBS += -lrt endif endif -YOSYS_VER := 0.22+29 +YOSYS_VER := 0.22+33 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From 8838b1eaa474ea116be8f9bfacc03ffb37bef248 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 18 Oct 2022 19:51:36 +0200 Subject: [PATCH 23/26] smtbmc: Fix witness handling for k-induction failures The "uninitialized" value is a _list_ of chunks that are part of the initial state for the witness trace. --- backends/smt2/smtio.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index f5cfe436d..a73745896 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -701,7 +701,7 @@ class SmtIo: if witness["type"] == "mem": if allregs and not witness["rom"]: width, size = witness["width"], witness["size"] - witness = {**witness, "uninitialized": {"width": width * size, "offset": 0}} + witness = {**witness, "uninitialized": [{"width": width * size, "offset": 0}]} if not witness["uninitialized"]: continue From 8859d801c83b6d67279bb907837bb7b08d2f338e Mon Sep 17 00:00:00 2001 From: Emil J Date: Wed, 19 Oct 2022 12:20:12 +0200 Subject: [PATCH 24/26] Temporal induction counterexample loop detection (#3504) I have added an optional flag to smtbmc that causes failed temporal induction counterexample traces to be checked for duplicate states and reported to the user, since loops in the counterexample mean that increasing the induction depth won't help prove a design's safety properties. --- backends/smt2/smtbmc.py | 37 ++++++++++++++++++++++++++++++++++++- 1 file changed, 36 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index ac329053f..4c1f07229 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -55,6 +55,7 @@ noinit = False binarymode = False keep_going = False check_witness = False +detect_loops = False so = SmtOpts() @@ -175,6 +176,10 @@ def usage(): check that the used witness file contains sufficient constraints to force an assertion failure. + --detect-loops + check if states are unique in temporal induction counter examples + (this feature is experimental and incomplete) + """ + so.helpmsg()) sys.exit(1) @@ -183,7 +188,7 @@ try: opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts + ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat", "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=", - "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness"]) + "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops"]) except: usage() @@ -264,6 +269,8 @@ for o, a in opts: keep_going = True elif o == "--check-witness": check_witness = True + elif o == "--detect-loops": + detect_loops = True elif so.handle(o, a): pass else: @@ -969,6 +976,30 @@ def write_vcd_trace(steps_start, steps_stop, index): vcd.set_time(steps_stop) +def detect_state_loop(steps_start, steps_stop): + print_msg(f"Checking for loops in found induction counter example") + print_msg(f"This feature is experimental and incomplete") + + path_list = sorted(smt.hiernets(topmod, regs_only=True)) + + mem_trace_data = collect_mem_trace_data(steps_start, steps_stop) + + # Map state to index of step when it occurred + states = dict() + + for i in range(steps_start, steps_stop): + value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i) + mem_state = sorted( + [(tuple(path), addr, data) + for path, addr, data in mem_trace_data.get(i, [])]) + state = tuple(value_list), tuple(mem_state) + if state in states: + return (i, states[state]) + else: + states[state] = i + + return None + def char_ok_in_verilog(c,i): if ('A' <= c <= 'Z'): return True if ('a' <= c <= 'z'): return True @@ -1597,6 +1628,10 @@ if tempind: print_anyconsts(num_steps) print_failed_asserts(num_steps) write_trace(step, num_steps+1, '%', allregs=True) + if detect_loops: + loop = detect_state_loop(step, num_steps+1) + if loop: + print_msg(f"Loop detected, increasing induction depth will not help. Step {loop[0]} = step {loop[1]}") elif dumpall: print_anyconsts(num_steps) From 6781746872087d8c1eb3f5560fe338a693a40d7c Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Thu, 20 Oct 2022 00:25:10 +0000 Subject: [PATCH 25/26] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index e41e5ff94..0acf55a72 100644 --- a/Makefile +++ b/Makefile @@ -131,7 +131,7 @@ LDLIBS += -lrt endif endif -YOSYS_VER := 0.22+33 +YOSYS_VER := 0.22+37 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From be1a12595af49c9cba5cb3689b21767eb23fa3b1 Mon Sep 17 00:00:00 2001 From: Claire Xenia Wolf Date: Thu, 20 Oct 2022 13:50:25 +0200 Subject: [PATCH 26/26] Add missing log_dump handler for std::vector<> Signed-off-by: Claire Xenia Wolf --- kernel/log.h | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/kernel/log.h b/kernel/log.h index 3bc9fd978..8ef6e6d0e 100644 --- a/kernel/log.h +++ b/kernel/log.h @@ -419,6 +419,18 @@ static inline void log_dump_val_worker(pool &v) { log(" }"); } +template +static inline void log_dump_val_worker(std::vector &v) { + log("{"); + bool first = true; + for (auto &it : v) { + log(first ? " " : ", "); + log_dump_val_worker(it); + first = false; + } + log(" }"); +} + template static inline void log_dump_val_worker(T *ptr) { log("%p", ptr); }