From 4bb4b6c66288b463bd551068a89eded3fc2ae264 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 26 Sep 2025 18:42:00 +0200 Subject: [PATCH] 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