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 <