From 6f7f71fe038cc95df77b5efbe978ce1af5e2997e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Tue, 9 Jan 2024 19:31:11 +0100 Subject: [PATCH 01/13] read_blif: Represent sequential elements with gate cells When reading the BLIF input, represent the native sequential elements with fine-grained cells like `$_FF_` instead of the coarse-grained cells like `$ff` which we were using up to now. There are two reasons for this: * The sequential elements in BLIF are always single-bit, so the gate cells are a better fit. * This makes it symmetrical to the BLIF backend which only understands the fine-grained cells, and only translates those to the native BLIF features. --- frontends/blif/blifparse.cc | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index ebbe082a2..72f942425 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -352,17 +352,17 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool goto no_latch_clock; if (!strcmp(edge, "re")) - cell = module->addDff(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q)); + cell = module->addDffGate(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q)); else if (!strcmp(edge, "fe")) - cell = module->addDff(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q), false); + cell = module->addDffGate(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q), false); else if (!strcmp(edge, "ah")) - cell = module->addDlatch(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q)); + cell = module->addDlatchGate(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q)); else if (!strcmp(edge, "al")) - cell = module->addDlatch(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q), false); + cell = module->addDlatchGate(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q), false); else { no_latch_clock: if (dff_name.empty()) { - cell = module->addFf(NEW_ID, blif_wire(d), blif_wire(q)); + cell = module->addFfGate(NEW_ID, blif_wire(d), blif_wire(q)); } else { cell = module->addCell(NEW_ID, dff_name); cell->setPort(ID::D, blif_wire(d)); From e9aacd8a0593009b469a1933873bedd49caacaef Mon Sep 17 00:00:00 2001 From: Robert O'Callahan Date: Tue, 23 Sep 2025 23:26:47 +0000 Subject: [PATCH 02/13] Move `OptMerge` cell filtering logic to happen while building the cell vector. This code is quite confusing because there are two "is the cell known" filters applied, one while building the cell vector and one after building the cell vector, and they're subtly different. I'm preserving the actual behaviour here but it looks like there is, or was, a bug here. --- passes/opt/opt_merge.cc | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/passes/opt/opt_merge.cc b/passes/opt/opt_merge.cc index 1cb499740..a59807be1 100644 --- a/passes/opt/opt_merge.cc +++ b/passes/opt/opt_merge.cc @@ -249,10 +249,15 @@ struct OptMergeWorker // mem can have an excessively large parameter holding the init data continue; } + if (cell->type == ID($scopeinfo)) + continue; if (mode_keepdc && has_dont_care_initval(cell)) continue; - if (ct.cell_known(cell->type) || (mode_share_all && cell->known())) - cells.push_back(cell); + if (!cell->known()) + continue; + if (!mode_share_all && !ct.cell_known(cell->type)) + continue; + cells.push_back(cell); } did_something = false; @@ -281,12 +286,6 @@ struct OptMergeWorker for (auto cell : cells) { - if ((!mode_share_all && !ct.cell_known(cell->type)) || !cell->known()) - continue; - - if (cell->type == ID($scopeinfo)) - continue; - auto [cell_in_map, inserted] = known_cells.insert(cell); if (!inserted) { // We've failed to insert since we already have an equivalent cell From 83dd99efb7971d212b3538bf05d92140393aed7d Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 24 Sep 2025 18:47:54 +0200 Subject: [PATCH 03/13] verific: New `-sva-continue-on-error` import option This option allows you to process a design that includes unsupported SVA. Unsupported SVA gets imported as formal cells using 'x inputs and with the `unsupported_sva` attribute set. This allows you to get a complete list of defined properties or to check only a supported subset of properties. To ensure no properties are unintentionally skipped for actual verification, even in cases where `-sva-continue-on-error` is used by default to read and inspect a design, `hierarchy -simcheck` and `hierarchy -smtcheck` (run by SBY) now ensure that no `unsupported_sva` property cells remain in the design. --- frontends/verific/verific.cc | 26 ++++++++++--- frontends/verific/verific.h | 6 ++- frontends/verific/verificsva.cc | 51 ++++++++++++++++--------- passes/hierarchy/hierarchy.cc | 19 +++++++++ tests/verific/sva_continue_on_err.ys | 38 ++++++++++++++++++ tests/verific/sva_no_continue_on_err.ys | 9 +++++ 6 files changed, 124 insertions(+), 25 deletions(-) create mode 100644 tests/verific/sva_continue_on_err.ys create mode 100644 tests/verific/sva_no_continue_on_err.ys diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 279b0dd52..b2b85641f 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -200,8 +200,8 @@ YosysStreamCallBackHandler verific_read_cb; // ================================================================== -VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) : - mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), +VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_sva_continue, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) : + mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), mode_sva_continue(mode_sva_continue), mode_names(mode_names), mode_verific(mode_verific), mode_autocover(mode_autocover), mode_fullinit(mode_fullinit) { @@ -2316,6 +2316,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma wire->attributes.erase(ID::init); } } + + if (num_sva_continue) { + log_warning("Encountered %d items containing unsupported SVA!\n", num_sva_continue); + log_warning("Unsupported SVA imported as 'x and marked using the `unsupported_sva' attribute due to -sva-continue-on-err.\n"); + } + num_sva_continue = 0; } // ================================================================== @@ -3051,7 +3057,7 @@ std::string verific_import(Design *design, const std::mapsecond; if (nl_done.count(it->first) == 0) { - VerificImporter importer(false, false, false, false, false, false, false); + VerificImporter importer(false, false, false, false, false, false, false, false); nl_done[it->first] = it->second; importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->CellBaseName())); } @@ -3288,6 +3294,11 @@ struct VerificPass : public Pass { log(" -nosva\n"); log(" Ignore SVA properties, do not infer checker logic.\n"); log("\n"); + log(" -sva-continue-on-err\n"); + log(" Turns unsupported SVA from an error into a warning. Properties are imported\n"); + log(" with their trigger condition replaced with 'x and with an `unsupported_sva'\n"); + log(" attribute to produce a later error in SBY if they remain in the design.\n"); + log("\n"); log(" -L \n"); log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n"); log("\n"); @@ -4033,7 +4044,8 @@ struct VerificPass : public Pass { { std::map nl_todo, nl_done; bool mode_all = false, mode_gates = false, mode_keep = false; - bool mode_nosva = false, mode_names = false, mode_verific = false; + bool mode_nosva = false, mode_sva_continue = false; + bool mode_names = false, mode_verific = false; bool mode_autocover = false, mode_fullinit = false; bool flatten = false, extnets = false, mode_cells = false; bool split_complex_ports = true; @@ -4071,6 +4083,10 @@ struct VerificPass : public Pass { mode_nosva = true; continue; } + if (args[argidx] == "-sva-continue-on-err") { + mode_sva_continue = true; + continue; + } if (args[argidx] == "-L" && argidx+1 < GetSize(args)) { verific_sva_fsm_limit = atoi(args[++argidx].c_str()); continue; @@ -4201,7 +4217,7 @@ struct VerificPass : public Pass { auto it = nl_todo.begin(); Netlist *nl = it->second; if (nl_done.count(it->first) == 0) { - VerificImporter importer(mode_gates, mode_keep, mode_nosva, + VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_sva_continue, mode_names, mode_verific, mode_autocover, mode_fullinit); nl_done[it->first] = it->second; importer.import_netlist(design, nl, nl_todo, top_mod_names.count(nl->CellBaseName())); diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index 4e9c7a305..f33a380f7 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -73,10 +73,12 @@ struct VerificImporter std::map sva_posedge_map; pool any_all_nets; - bool mode_gates, mode_keep, mode_nosva, mode_names, mode_verific; + bool mode_gates, mode_keep, mode_nosva, mode_sva_continue, mode_names, mode_verific; bool mode_autocover, mode_fullinit; - VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit); + int num_sva_continue = 0; + + VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_sva_continue, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit); RTLIL::SigBit net_map_at(Verific::Net *net); diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 3908947eb..9757f07f2 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -1023,7 +1023,7 @@ struct VerificSvaImporter [[noreturn]] void parser_error(std::string errmsg) { - if (!importer->mode_keep) + if (!importer->mode_keep && !importer->mode_sva_continue) log_error("%s", errmsg); log_warning("%s", errmsg); throw ParserErrorException(); @@ -1710,30 +1710,30 @@ struct VerificSvaImporter void import() { - try - { - module = importer->module; - netlist = root->Owner(); + module = importer->module; + netlist = root->Owner(); - if (verific_verbose) - log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(), - LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile())); + if (verific_verbose) + log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(), + LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile())); - bool is_user_declared = root->IsUserDeclared(); + bool is_user_declared = root->IsUserDeclared(); - // FIXME - if (!is_user_declared) { - const char *name = root->Name(); - for (int i = 0; name[i]; i++) { - if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) { - is_user_declared = true; - break; - } + // FIXME + if (!is_user_declared) { + const char *name = root->Name(); + for (int i = 0; name[i]; i++) { + if (i ? (name[i] < '0' || name[i] > '9') : (name[i] != 'i')) { + is_user_declared = true; + break; } } + } - RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID); + RTLIL::IdString root_name = module->uniquify(importer->mode_names || is_user_declared ? RTLIL::escape_id(root->Name()) : NEW_ID); + try + { // parse SVA sequence into trigger signal clocking = VerificClocking(importer, root->GetInput(), true); @@ -1836,6 +1836,21 @@ struct VerificSvaImporter } catch (ParserErrorException) { + if (importer->mode_sva_continue) { + + RTLIL::Cell *c = nullptr; + + if (mode_assert) c = module->addAssert(root_name, State::Sx, State::Sx); + if (mode_assume) c = module->addAssume(root_name, State::Sx, State::Sx); + if (mode_cover) c = module->addCover(root_name, State::Sx, State::Sx); + + if (c) { + importer->import_attributes(c->attributes, root); + c->set_bool_attribute(ID(unsupported_sva)); + } + + importer->num_sva_continue++; + } } } }; diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc index a7f86c3f0..b3edcef94 100644 --- a/passes/hierarchy/hierarchy.cc +++ b/passes/hierarchy/hierarchy.cc @@ -1149,6 +1149,25 @@ struct HierarchyPass : public Pass { } } + if (flag_simcheck || flag_smtcheck) { + for (auto mod : design->modules()) { + for (auto cell : mod->cells()) { + if (!cell->type.in(ID($check), ID($assert), ID($assume), ID($live), ID($fair), ID($cover))) + continue; + if (!cell->has_attribute(ID(unsupported_sva))) + continue; + + auto src = cell->get_src_attribute(); + + if (!src.empty()) + src += ": "; + + log_error("%sProperty `%s' in module `%s' uses unsupported SVA constructs. See frontend warnings for details, run `delete */a:unsupported_sva' to ignore.\n", + src, log_id(cell->name), log_id(mod->name)); + } + } + } + if (!keep_positionals) { std::set pos_mods; diff --git a/tests/verific/sva_continue_on_err.ys b/tests/verific/sva_continue_on_err.ys new file mode 100644 index 000000000..4cd603f74 --- /dev/null +++ b/tests/verific/sva_continue_on_err.ys @@ -0,0 +1,38 @@ +verific -sv < b); + prop_unsupported1: assert property (@(posedge clk) a ##1 b #=# b); + prop_unsupported2: assert property (@(posedge clk) a ##1 @(posedge b) ##1 a); + + sequence local_var_seq; + logic v; + (1, v = a) ##1 b ##1 (v == a); + endsequence + + prop_unsupported3: assert property (@(posedge clk) local_var_seq); + +endmodule +EOF + +logger -expect warning "Mixed clocking is currently not supported" 1 +logger -expect warning "Verific SVA primitive sva_non_overlapped_followed_by .* is currently unsupported in this context" 1 +logger -expect warning "SVA sequences with local variable assignments are currently not supported" 1 +logger -expect warning "Encountered 3 items containing unsupported SVA" 1 +verific -import -sva-continue-on-err top +logger -check-expected + +select -assert-count 4 top/t:$assert +select -assert-count 4 top/a:unsupported_sva top/prop_supported %% top/t:$assert %i + +select -assert-count 3 top/a:unsupported_sva +select -assert-count 3 top/a:unsupported_sva top/prop_unsupported* %i +select -assert-count 1 top/a:unsupported_sva top/prop_unsupported1 %i +select -assert-count 1 top/a:unsupported_sva top/prop_unsupported2 %i +select -assert-count 1 top/a:unsupported_sva top/prop_unsupported3 %i +select -assert-count 0 top/a:unsupported_sva top/prop_supported %i +select -assert-count 1 top/prop_supported + +logger -expect error "uses unsupported SVA constructs." 1 +hierarchy -smtcheck -top top +logger -check-expected diff --git a/tests/verific/sva_no_continue_on_err.ys b/tests/verific/sva_no_continue_on_err.ys new file mode 100644 index 000000000..5a0a59a81 --- /dev/null +++ b/tests/verific/sva_no_continue_on_err.ys @@ -0,0 +1,9 @@ + +verific -sv < Date: Fri, 26 Sep 2025 18:39:32 +0200 Subject: [PATCH 04/13] hierarchy: Suggest more specific command to skip unsupported SVA --- passes/hierarchy/hierarchy.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc index b3edcef94..ea68add18 100644 --- a/passes/hierarchy/hierarchy.cc +++ b/passes/hierarchy/hierarchy.cc @@ -1162,7 +1162,7 @@ struct HierarchyPass : public Pass { if (!src.empty()) src += ": "; - log_error("%sProperty `%s' in module `%s' uses unsupported SVA constructs. See frontend warnings for details, run `delete */a:unsupported_sva' to ignore.\n", + log_error("%sProperty `%s' in module `%s' uses unsupported SVA constructs. See frontend warnings for details, run `chformal -remove a:unsupported_sva' to ignore.\n", src, log_id(cell->name), log_id(mod->name)); } } From 4bb4b6c66288b463bd551068a89eded3fc2ae264 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 26 Sep 2025 18:42:00 +0200 Subject: [PATCH 05/13] verific: Extend -sva-continue-on-err to handle FSM explosion This also rolls back any added cells and wires, since we might have added a lot of helper logic by the point we detect this. --- frontends/verific/verificsva.cc | 34 +++++++++++++++++-- .../verific/sva_continue_on_err_explosion.ys | 31 +++++++++++++++++ 2 files changed, 63 insertions(+), 2 deletions(-) create mode 100644 tests/verific/sva_continue_on_err_explosion.ys diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 9757f07f2..50e0049ae 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -124,6 +124,7 @@ struct SvaFsm { Module *module; VerificClocking clocking; + std::function parser_error; SigBit trigger_sig = State::S1, disable_sig; SigBit throughout_sig = State::S1; @@ -148,6 +149,7 @@ struct SvaFsm module = clking.module; clocking = clking; trigger_sig = trig; + parser_error = [](std::string msg){ log_error("%s", msg); }; startNode = createNode(); acceptNode = createNode(); @@ -475,8 +477,8 @@ struct SvaFsm dump(); log(" ctrl signal: %s\n", log_signal(dnode.ctrl)); } - log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n", - GetSize(dnode.ctrl), verific_sva_fsm_limit); + parser_error(stringf("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n", + GetSize(dnode.ctrl), verific_sva_fsm_limit)); } for (unsigned long long i = 0; i < (1ull << GetSize(dnode.ctrl)); i++) @@ -1260,6 +1262,7 @@ struct VerificSvaImporter if (inst->Type() == PRIM_SVA_FIRST_MATCH) { SvaFsm match_fsm(clocking); + match_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; match_fsm.createLink(parse_sequence(match_fsm, match_fsm.createStartNode(), inst->GetInput()), match_fsm.acceptNode); int node = fsm.createNode(); @@ -1426,12 +1429,15 @@ struct VerificSvaImporter if (inst->Type() == PRIM_SVA_SEQ_AND || inst->Type() == PRIM_SVA_AND) { SvaFsm fsm1(clocking); + fsm1.parser_error = [&](std::string msg) { this->parser_error(msg); }; fsm1.createLink(parse_sequence(fsm1, fsm1.createStartNode(), inst->GetInput1()), fsm1.acceptNode); SvaFsm fsm2(clocking); + fsm2.parser_error = [&](std::string msg) { this->parser_error(msg); }; fsm2.createLink(parse_sequence(fsm2, fsm2.createStartNode(), inst->GetInput2()), fsm2.acceptNode); SvaFsm combined_fsm(clocking); + combined_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; fsm1.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode); fsm2.getDFsm(combined_fsm, combined_fsm.createStartNode(), -1, combined_fsm.acceptNode); @@ -1456,6 +1462,7 @@ struct VerificSvaImporter if (inst->Type() == PRIM_SVA_INTERSECT || inst->Type() == PRIM_SVA_WITHIN) { SvaFsm intersect_fsm(clocking); + intersect_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; if (inst->Type() == PRIM_SVA_INTERSECT) { @@ -1562,6 +1569,7 @@ struct VerificSvaImporter int node; SvaFsm antecedent_fsm(clocking, trig); + antecedent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { int next_node = antecedent_fsm.createNode(); @@ -1623,6 +1631,7 @@ struct VerificSvaImporter int node; SvaFsm antecedent_fsm(clocking, trig); + antecedent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION || inst->Type() == PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY) { int next_node = antecedent_fsm.createNode(); @@ -1677,6 +1686,7 @@ struct VerificSvaImporter } SvaFsm consequent_fsm(clocking, antecedent_match); + consequent_fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; node = parse_sequence(consequent_fsm, consequent_fsm.createStartNode(), consequent_net); consequent_fsm.createLink(node, consequent_fsm.acceptNode); @@ -1696,6 +1706,7 @@ struct VerificSvaImporter } SvaFsm fsm(clocking, trig); + fsm.parser_error = [&](std::string msg) { this->parser_error(msg); }; int node = parse_sequence(fsm, fsm.createStartNode(), net); fsm.createLink(node, fsm.acceptNode); @@ -1713,6 +1724,10 @@ struct VerificSvaImporter module = importer->module; netlist = root->Owner(); + int initial_cell_count = GetSize(module->cells_); + int initial_wire_count = GetSize(module->wires_); + int initial_connection_count = GetSize(module->connections_); + if (verific_verbose) log(" importing SVA property at root cell %s (%s) at %s:%d.\n", root->Name(), root->View()->Owner()->Name(), LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile())); @@ -1838,6 +1853,21 @@ struct VerificSvaImporter { if (importer->mode_sva_continue) { + std::vector remove_cells; + pool remove_wires; + + for (int i = 0, end = GetSize(module->cells_) - initial_cell_count; i != end; ++i) + remove_cells.push_back(module->cells_.element(i)->second); + + for (int i = 0, end = GetSize(module->wires_) - initial_wire_count; i != end; ++i) + remove_wires.emplace(module->wires_.element(i)->second); + + for (auto cell : remove_cells) + module->remove(cell); + module->remove(remove_wires); + + module->connections_.resize(initial_connection_count); + RTLIL::Cell *c = nullptr; if (mode_assert) c = module->addAssert(root_name, State::Sx, State::Sx); diff --git a/tests/verific/sva_continue_on_err_explosion.ys b/tests/verific/sva_continue_on_err_explosion.ys new file mode 100644 index 000000000..c96ad0140 --- /dev/null +++ b/tests/verific/sva_continue_on_err_explosion.ys @@ -0,0 +1,31 @@ +verific -sv < b); + + prop_exploding: assert property (@(posedge clk) + ((a [*7] ##1 b) [*11]) and + ((a [*11] ##1 b) [*7]) and + ((a [*13] ##1 b) [*5]) and + ((a [*5] ##1 b) [*13]) + ); + + prop_supported2: assert property (@(posedge clk) a [*5] ##1 b |=> b); + +endmodule +EOF + +logger -expect warning "Stopping to prevent exponential design size explosion." 1 +verific -import -sva-continue-on-err top +logger -check-expected + +select -assert-count 3 top/t:$assert +select -assert-count 1 top/a:unsupported_sva top/prop_exploding %% top/t:$assert %i + +select -assert-count 0 top/a:unsupported_sva top/prop_supported1 %i +select -assert-count 0 top/a:unsupported_sva top/prop_supported2 %i +select -assert-count 2 top/prop_supported* + +logger -expect error "uses unsupported SVA constructs." 1 +hierarchy -smtcheck -top top +logger -check-expected From 9396e5e5fe40f90e44498597ae4df4cc391561e1 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 23 Sep 2025 14:40:22 +0200 Subject: [PATCH 06/13] portarcs: Ignore all bufnorm helper cells The `portarcs` pass was already ignoring `$buf` cells when loading timing data, but now bufnorm will also emit `$input_port` and `$connect` helper cells, which need to be ignored as well. --- passes/cmds/portarcs.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/passes/cmds/portarcs.cc b/passes/cmds/portarcs.cc index 36870489a..8cc5d1236 100644 --- a/passes/cmds/portarcs.cc +++ b/passes/cmds/portarcs.cc @@ -124,7 +124,8 @@ struct PortarcsPass : Pass { TopoSort sort; for (auto cell : m->cells()) - if (cell->type != ID($buf)) { + // Ignore all bufnorm helper cells + if (!cell->type.in(ID($buf), ID($input_port), ID($connect))) { auto tdata = tinfo.find(cell->type); if (tdata == tinfo.end()) log_cmd_error("Missing timing data for module '%s'.\n", log_id(cell->type)); From 90669ab4eba25878ee592b80bc4ba5f79386b81c Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 23 Sep 2025 14:44:13 +0200 Subject: [PATCH 07/13] aiger2: Only fail for reachable undirected bufnorm helper cells The aiger2 backend checks for unsupported cells during indexing. This causes it to fail when `$connect` or `$tribuf` (as workaround for missing 'z-$buf support) cells are present in the module. Since bufnorm adds these cells automatically, it is very easy to end up with them due to unconnected wires or e.g. `$specify` cells, which do not pose an actual problem for the backend, since it will never encounter those during a traversal. With this, we ignore them during indexing and only produce an actual error message if we reach such a cell during the traversal. --- backends/aiger2/aiger.cc | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/backends/aiger2/aiger.cc b/backends/aiger2/aiger.cc index b63e51bde..41e1b91c1 100644 --- a/backends/aiger2/aiger.cc +++ b/backends/aiger2/aiger.cc @@ -105,6 +105,13 @@ struct Index { if (allow_blackboxes) { info.found_blackboxes.insert(cell); } else { + // Even if we don't allow blackboxes these might still be + // present outside of any traversed input cones, so we + // can't bail at this point. If they are hit by a traversal + // (which can only really happen with $tribuf not + // $connect), we can still detect this as an error later. + if (cell->type == ID($connect) || (cell->type == ID($tribuf) && cell->has_attribute(ID(aiger2_zbuf)))) + continue; if (!submodule || submodule->get_blackbox_attribute()) log_error("Unsupported cell type: %s (%s in %s)\n", log_id(cell->type), log_id(cell), log_id(m)); @@ -483,7 +490,8 @@ struct Index { { Design *design = index.design; auto &minfo = leaf_minfo(index); - log_assert(minfo.suboffsets.count(cell)); + if (!minfo.suboffsets.count(cell)) + log_error("Reached unsupport cell %s (%s in %s)\n", log_id(cell->type), log_id(cell), log_id(cell->module)); Module *def = design->module(cell->type); log_assert(def); levels.push_back(Level(index.modules.at(def), cell)); From cbc1055517b6936de34332c480da9e7a9aae658f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 23 Sep 2025 21:54:55 +0200 Subject: [PATCH 08/13] opt_clean: Fix debug output when cleaning up bufnorm cells --- passes/opt/opt_clean.cc | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index dc3f015cd..996a9b3c9 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -635,9 +635,17 @@ void rmunused_module(RTLIL::Module *module, bool purge_mode, bool verbose, bool } } for (auto cell : delcells) { - if (verbose) - log_debug(" removing buffer cell `%s': %s = %s\n", cell->name, - log_signal(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::A))); + if (verbose) { + if (cell->type == ID($connect)) + log_debug(" removing connect cell `%s': %s <-> %s\n", cell->name, + log_signal(cell->getPort(ID::A)), log_signal(cell->getPort(ID::B))); + else if (cell->type == ID($input_port)) + log_debug(" removing input port marker cell `%s': %s\n", cell->name, + log_signal(cell->getPort(ID::Y))); + else + log_debug(" removing buffer cell `%s': %s = %s\n", cell->name, + log_signal(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::A))); + } module->remove(cell); } if (!delcells.empty()) From 86fb2f16f7863634e1df9e692520656fa55a36a7 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 23 Sep 2025 14:28:10 +0200 Subject: [PATCH 09/13] bufnorm: Refactor and fix incremental bufNormalize This fixes some edge cases the previous version didn't handle properly by simplifying the logic of determining directly driven wires and representatives to use as buffer inputs. --- kernel/rtlil.cc | 7 + kernel/rtlil_bufnorm.cc | 224 ++++++++++++++--------------- tests/various/bufnorm_opt_clean.ys | 154 ++++++++++++++++++++ 3 files changed, 270 insertions(+), 115 deletions(-) create mode 100644 tests/various/bufnorm_opt_clean.ys diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index e9d051de8..8daf2c821 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -2829,6 +2829,13 @@ void RTLIL::Module::remove(const pool &wires) delete_wire_worker.wires_p = &wires; rewrite_sigspecs2(delete_wire_worker); + if (design->flagBufferedNormalized) { + for (auto wire : wires) { + buf_norm_wire_queue.erase(wire); + buf_norm_connect_index.erase(wire); + } + } + for (auto &it : wires) { log_assert(wires_.count(it->name) != 0); wires_.erase(it->name); diff --git a/kernel/rtlil_bufnorm.cc b/kernel/rtlil_bufnorm.cc index 6d619d9e6..d0561f880 100644 --- a/kernel/rtlil_bufnorm.cc +++ b/kernel/rtlil_bufnorm.cc @@ -43,6 +43,7 @@ void RTLIL::Design::bufNormalize(bool enable) wire->driverCell_ = nullptr; wire->driverPort_ = IdString(); } + module->buf_norm_connect_index.clear(); } flagBufferedNormalized = false; @@ -126,15 +127,19 @@ void RTLIL::Module::bufNormalize() idict wire_queue_entries; // Ordered queue of wires to process int wire_queue_pos = 0; // Index up to which we processed the wires - // Wires with their unique driving cell port. If we know a wire is - // driven by multiple (potential) drivers, this is indicated by a - // nullptr as cell. + // Wires with their unique driving cell port. We pick the first driver + // we encounter, with the exception that we ensure that a module input + // port can only get $input_port drivers and that $input_port drivers + // cannot drive any other modules. If we reject an $input_port driver + // because it's not driving an input port or because there already is + // another $input_port driver for the same port, we also delete that + // $input_port cell. dict> direct_driven_wires; - // Set of non-unique or driving cell ports for each processed wire. - dict>> direct_driven_wires_conflicts; - - // Set of cell ports that need a fresh intermediate wire. + // Set of cell ports that need a fresh intermediate wire. These are all + // cell ports that drive non-full-wire sigspecs, cell ports driving + // module input ports, and cell ports driving wires that are already + // driven. pool> pending_ports; // This helper will be called for every output/inout cell port that is @@ -149,27 +154,14 @@ void RTLIL::Module::bufNormalize() SigSpec const &sig = cell->getPort(port); - if (cell->type == ID($input_port)) { - // If an `$input_port` cell isn't fully connected to a full - // input port wire, we remove it since the wires are still the - // canonical source of module ports and the `$input_port` cells - // are just helpers to simplfiy the bufnorm invariant. - log_assert(port == ID::Y); - if (!sig.is_wire()) { - buf_norm_cell_queue.insert(cell); - remove(cell); - return; - } - Wire *w = sig.as_wire(); - if (!w->port_input || w->port_output) { - buf_norm_cell_queue.insert(cell); - remove(cell); - return; - } - w->driverCell_ = cell; - w->driverPort_ = ID::Y; - } else if (cell->type == ID($buf) && cell->attributes.empty() && !cell->name.isPublic()) { + // Make sure all wires of the cell port are enqueued, ensuring we + // detect other connected drivers (output and inout). + for (auto chunk : sig.chunks()) + if (chunk.is_wire()) + wire_queue_entries(chunk.wire); + + if (cell->type == ID($buf) && cell->attributes.empty() && !cell->name.isPublic()) { // For a plain `$buf` cell, we enqueue all wires on its input // side, bypass it using module level connections (skipping 'z // bits) and then remove the cell. Eventually the module level @@ -206,47 +198,40 @@ void RTLIL::Module::bufNormalize() if (!sig_y.empty()) connect(sig_y, sig_a); + remove(cell); + log_assert(GetSize(buf_norm_wire_queue) <= 1); + buf_norm_wire_queue.clear(); + return; + } else if (cell->type == ID($input_port)) { + log_assert(port == ID::Y); + if (sig.is_wire()) { + Wire *w = sig.as_wire(); + if (w->port_input && !w->port_output) { + // An $input_port cell can only drive a full wire module input port + auto [found, inserted] = direct_driven_wires.emplace(w, {cell, port}); + if (!inserted || (found->second.first == cell && found->second.second == port)) + return; + } + } + + // If an `$input_port` cell isn't driving a full + // input port wire, we remove it since the wires are still the + // canonical source of module ports + buf_norm_cell_queue.insert(cell); remove(cell); + log_assert(GetSize(buf_norm_wire_queue) <= 1); + buf_norm_wire_queue.clear(); return; } - // Make sure all wires of the cell port are enqueued, ensuring we - // detect other connected drivers (output and inout). - for (auto const &chunk : sig.chunks()) - if (chunk.wire) - wire_queue_entries(chunk.wire); - if (sig.is_wire()) { - // If the full cell port is connected to a full wire, we might be - // able to keep that connection if this is a unique output port driving that wire Wire *w = sig.as_wire(); - - // We try to store the current port as unique driver, if this - // succeeds we're done with the port. - auto [found, inserted] = direct_driven_wires.emplace(w, {cell, port}); - if (inserted || (found->second.first == cell && found->second.second == port)) - return; - - // When this failed, we store this port as a conflict. If we - // had already stored a candidate for a unique driver, we also - // move it to the conflicts, leaving a nullptr marker. - - auto &conflicts = direct_driven_wires_conflicts[w]; - if (Cell *other_cell = found->second.first) { - if (other_cell->type == ID($input_port)) { - // Multiple input port cells - log_assert(cell->type != ID($input_port)); - } else { - pending_ports.insert(found->second); - conflicts.emplace(found->second); - found->second = {nullptr, {}}; - } - } - if (cell->type == ID($input_port)) { - found->second = {cell, port}; - } else { - conflicts.emplace(cell, port); + if (!w->port_input || w->port_output) { + // If the full cell port is connected to a full non-input-port wire, pick it as driver + auto [found, inserted] = direct_driven_wires.emplace(w, {cell, port}); + if (inserted || (found->second.first == cell && found->second.second == port)) + return; } } @@ -256,16 +241,22 @@ void RTLIL::Module::bufNormalize() pending_ports.emplace(cell, port); }; + // We enqueue all enqueued wires for `$buf`/`$connect` processing (clearing the module level queue). + for (auto wire : buf_norm_wire_queue) + wire_queue_entries(wire); + buf_norm_wire_queue.clear(); + + // Only after clearing the `buf_norm_wire_queue` are we allowed to call + // enqueue_cell_port, since we're using assertions to check against + // unintended wires being enqueued into `buf_norm_wire_queue` that + // would prevent us from restoring the bufnorm invariants in a single + // pass. + // We process all explicitly enqueued cell ports (clearing the module level queue). for (auto const &[cell, port_name] : buf_norm_cell_port_queue) enqueue_cell_port(cell, port_name); buf_norm_cell_port_queue.clear(); - // And enqueue all wires for `$buf`/`$connect` processing (clearing the module level queue). - for (auto wire : buf_norm_wire_queue) - wire_queue_entries(wire); - buf_norm_wire_queue.clear(); - // We also enqueue all wires that saw newly added module level connections. for (auto &[a, b] : connections_) for (auto &sig : {a, b}) @@ -302,8 +293,11 @@ void RTLIL::Module::bufNormalize() if (chunk.wire) wire_queue_entries(chunk.wire); connect(sig_a, sig_b); + buf_norm_cell_queue.insert(connect_cell); remove(connect_cell); + log_assert(GetSize(buf_norm_wire_queue) <= 2); + buf_norm_wire_queue.clear(); } } } @@ -315,6 +309,9 @@ void RTLIL::Module::bufNormalize() // As a first step for re-normalization we add all require intermediate // wires for cell output and inout ports. for (auto &[cell, port] : pending_ports) { + log_assert(cell->type != ID($input_port)); + log_assert(!cell->type.empty()); + log_assert(!pending_deleted_cells.count(cell)); SigSpec const &sig = cell->getPort(port); Wire *w = addWire(NEW_ID, GetSize(sig)); @@ -323,16 +320,9 @@ void RTLIL::Module::bufNormalize() // correspond to what you would get if the intermediate wires had // been in place from the beginning. connect(sig, w); - auto port_dir = cell->port_dir(port); - if (port_dir == RTLIL::PD_INOUT || port_dir == RTLIL::PD_UNKNOWN) { - direct_driven_wires.emplace(w, {nullptr, {}}); - direct_driven_wires_conflicts[w].emplace(cell, port); - } else { - direct_driven_wires.emplace(w, {cell, port}); - } - - cell->setPort(port, w); - wire_queue_entries(w); + direct_driven_wires.emplace(w, {cell, port}); + cell->setPort(port, w); // Hits the fast path that doesn't enqueue w + wire_queue_entries(w); // Needed so we pick up the sig <-> w connection } // At this point we're done with creating wires and know which ones are @@ -346,7 +336,7 @@ void RTLIL::Module::bufNormalize() wire->driverPort_.clear(); } - // For the unique output cell ports fully connected to a full wire, we + // For the unique driving cell ports fully connected to a full wire, we // can update the bufnorm data right away. For all other wires we will // have to create new `$buf` cells. for (auto const &[wire, cellport] : direct_driven_wires) { @@ -373,54 +363,55 @@ void RTLIL::Module::bufNormalize() SigMap sigmap(this); new_connections({}); - pool conflicted; - pool driven; - - // We iterate over all direct driven wires and try to make that wire's - // sigbits the representative sigbit for the net. We do a second pass - // to detect conflicts to then remove the conflicts from `driven`. - for (bool check : {false, true}) { + // We pick SigMap representatives by prioritizing input ports over + // driven wires over other/unknown wires. + for (bool input_ports : {false, true}) { for (auto const &[wire, cellport] : direct_driven_wires) { - if (cellport.first == nullptr) - continue; - auto const &[cell, port] = cellport; - - SigSpec z_mask; - if (cell->type == ID($buf)) - z_mask = cell->getPort(ID::A); - - for (int i = 0; i != GetSize(wire); ++i) { - SigBit driver = SigBit(wire, i); - if (!z_mask.empty() && z_mask[i] == State::Sz) - continue; - if (check) { - SigBit repr = sigmap(driver); - if (repr != driver) - conflicted.insert(repr); - else - driven.insert(repr); - } else { + if ((wire->port_input && !wire->port_output) == input_ports) { + for (int i = 0; i != GetSize(wire); ++i) { + SigBit driver = SigBit(wire, i); sigmap.database.promote(driver); } } } } - // Ensure that module level inout ports are directly driven or - // connected using `$connect` cells and never `$buf`fered. - for (auto wire : wire_queue_entries) { - if (!wire->port_input || !wire->port_output) - continue; + // All three pool below are in terms of sigmapped bits + // Bits that are known to have a unique driver that is an unconditional driver or one or more inout drivers + pool driven; + // Bits that have multiple unconditional drivers, this forces the use of `$connect` + pool conflicted; + // Bits that are driven by an inout driver + pool weakly_driven; + + for (auto const &[wire, cellport] : direct_driven_wires) { + auto const &[cell, port] = cellport; for (int i = 0; i != GetSize(wire); ++i) { - SigBit driver = SigBit(wire, i); - SigBit repr = sigmap(driver); - if (driver != repr) - driven.erase(repr); + SigBit driver = sigmap(SigBit(wire, i)); + if (cell->type == ID($tribuf) || cell->port_dir(port) == RTLIL::PD_INOUT) { + // We add inout drivers to `driven` in a separate loop below + weakly_driven.insert(driver); + } else { + // We remove driver conflicts from `driven` in a separate loop below + bool inserted = driven.insert(driver).second; + if (!inserted) + conflicted.insert(driver); + } } } - for (auto &bit : conflicted) - driven.erase(bit); + // If a wire has one or more inout drivers and an unconditional driver, that's still a conflict + for (auto driver : weakly_driven) + if (!driven.insert(driver).second) + conflicted.insert(driver); + + // This only leaves the drivers matching `driven`'s definition above + for (auto driver : conflicted) + driven.erase(driver); + + // Having picked representatives and checked whether they are unique + // drivers, we can turn the connecitivty of our sigmap back into $buf + // and $connect cells. // Module level bitwise connections not representable by `$buf` cells pool> undirected_connections; @@ -561,6 +552,8 @@ void RTLIL::Cell::unsetPort(const RTLIL::IdString& portname) w->driverCell_ = nullptr; w->driverPort_ = IdString(); module->buf_norm_wire_queue.insert(w); + } else if (w->driverCell_) { + log_assert(w->driverCell_->getPort(w->driverPort_) == w); } } @@ -630,7 +623,8 @@ void RTLIL::Cell::setPort(const RTLIL::IdString& portname, RTLIL::SigSpec signal // bufNormalize call if ((dir == RTLIL::PD_OUTPUT || dir == RTLIL::PD_INOUT) && signal.is_wire()) { Wire *w = signal.as_wire(); - if (w->driverCell_ == nullptr) { + if (w->driverCell_ == nullptr && ( + (w->port_input && !w->port_output) == (type == ID($input_port)))) { w->driverCell_ = this; w->driverPort_ = portname; diff --git a/tests/various/bufnorm_opt_clean.ys b/tests/various/bufnorm_opt_clean.ys new file mode 100644 index 000000000..e1036f920 --- /dev/null +++ b/tests/various/bufnorm_opt_clean.ys @@ -0,0 +1,154 @@ + +read_aiger < Date: Mon, 29 Sep 2025 12:26:43 +0200 Subject: [PATCH 10/13] opt_hier: Fix two optimizations conflicting Fix a conflict between the following two: * propagation of tied-together inputs in * propagation of unused inputs out --- passes/opt/opt_hier.cc | 19 ++++++++++++++----- tests/opt/bug5398.ys | 23 +++++++++++++++++++++++ 2 files changed, 37 insertions(+), 5 deletions(-) create mode 100644 tests/opt/bug5398.ys diff --git a/passes/opt/opt_hier.cc b/passes/opt/opt_hier.cc index a8df78dc1..06103b4be 100644 --- a/passes/opt/opt_hier.cc +++ b/passes/opt/opt_hier.cc @@ -310,7 +310,7 @@ struct UsageData { refine_tie_togethers(inputs); } - bool apply_changes() { + bool apply_changes(ModuleIndex &index) { bool did_something = false; if (module->get_blackbox_attribute()) { @@ -374,8 +374,16 @@ struct UsageData { // Propagate tied-together inputs dict ties; for (auto group : tie_together_inputs) { - for (int i = 1; i < group.size(); i++) - ties[group[i]] = group[0]; + // Only consider used inputs for a tie-together group. + // ModuleIndex::apply_changes might have disconnected + // unused inputs. + SigSpec filtered_group; + for (auto bit : group) { + if (index.used.check(bit)) + filtered_group.append(bit); + } + for (int i = 1; i < filtered_group.size(); i++) + ties[filtered_group[i]] = filtered_group[0]; } SigPool applied_ties; auto ties_rewrite = [&](SigSpec &signal) { @@ -449,12 +457,13 @@ struct OptHierPass : Pass { bool did_something = false; for (auto module : d->selected_modules(RTLIL::SELECT_WHOLE_ONLY, RTLIL::SB_UNBOXED_CMDERR)) { + ModuleIndex &parent_index = indices.at(module->name); + if (usage_datas.count(module->name)) { log_debug("Applying usage data changes to %s\n", log_id(module)); - did_something |= usage_datas.at(module->name).apply_changes(); + did_something |= usage_datas.at(module->name).apply_changes(parent_index); } - ModuleIndex &parent_index = indices.at(module->name); for (auto cell : module->cells()) { if (indices.count(cell->type)) { log_debug("Applying changes to instance %s of %s in %s\n", log_id(cell), log_id(cell->type), log_id(module)); diff --git a/tests/opt/bug5398.ys b/tests/opt/bug5398.ys new file mode 100644 index 000000000..93c5a2d52 --- /dev/null +++ b/tests/opt/bug5398.ys @@ -0,0 +1,23 @@ +read_verilog < Date: Mon, 29 Sep 2025 12:26:54 +0200 Subject: [PATCH 11/13] opt_hier: Adjust messages --- passes/opt/opt_hier.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/passes/opt/opt_hier.cc b/passes/opt/opt_hier.cc index 06103b4be..5c3b09b31 100644 --- a/passes/opt/opt_hier.cc +++ b/passes/opt/opt_hier.cc @@ -144,12 +144,12 @@ struct ModuleIndex { } if (nunused > 0) { - log("Disconnected %d input bits of instance '%s' of '%s' in '%s'\n", + log("Disconnected %d input bits of instance '%s' (type '%s') in '%s'\n", nunused, log_id(instantiation), log_id(instantiation->type), log_id(parent.module)); changed = true; } if (nconstants > 0) { - log("Substituting constant for %d output bits of instance '%s' of '%s' in '%s'\n", + log("Substituting constant for %d output bits of instance '%s' (type '%s') in '%s'\n", nconstants, log_id(instantiation), log_id(instantiation->type), log_id(parent.module)); changed = true; } From acf3a6606ffef050f903c5c9e2d0cfcd2709fdac Mon Sep 17 00:00:00 2001 From: Akash Levy Date: Sun, 28 Sep 2025 07:25:25 -0700 Subject: [PATCH 12/13] Small gitignore fixes --- .gitignore | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/.gitignore b/.gitignore index cac630d7c..47f758a9b 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,9 @@ ## user config /Makefile.conf +## homebrew +/Brewfile.lock.json + ## build artifacts # compiler intermediate files *.o @@ -11,6 +14,12 @@ *.gcno *.so.dSYM/ +## test artifacts +**/run-test.mk +*.err +*.log +*.tmp + # compiler output files /kernel/version_*.cc /share From 5fd2aecd90ff36bffeb5a4cebc7cfb61d862e877 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 30 Sep 2025 00:23:05 +0000 Subject: [PATCH 13/13] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 7a2e8419b..317dbeb9b 100644 --- a/Makefile +++ b/Makefile @@ -164,7 +164,7 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.57+218 +YOSYS_VER := 0.57+244 YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1) YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1) YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2)