aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--frontends/verific/verific.cc11
-rw-r--r--frontends/verific/verific.h2
-rw-r--r--frontends/verific/verificsva.cc5
3 files changed, 16 insertions, 2 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 1dd6d7e24..c5fa58313 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -64,6 +64,7 @@ YOSYS_NAMESPACE_BEGIN
int verific_verbose;
bool verific_import_pending;
string verific_error_msg;
+int verific_sva_fsm_limit;
vector<string> verific_incdirs, verific_libdirs;
@@ -1618,6 +1619,8 @@ struct VerificExtNets
void verific_import(Design *design, std::string top)
{
+ verific_sva_fsm_limit = 16;
+
std::set<Netlist*> nl_todo, nl_done;
{
@@ -1789,6 +1792,9 @@ struct VerificPass : public Pass {
log(" -nosva\n");
log(" Ignore SVA properties, do not infer checker logic.\n");
log("\n");
+ log(" -L <int>\n");
+ log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n");
+ log("\n");
log(" -n\n");
log(" Keep all Verific names on instances and nets. By default only\n");
log(" user-declared names are preserved.\n");
@@ -1830,6 +1836,7 @@ struct VerificPass : public Pass {
}
verific_verbose = 0;
+ verific_sva_fsm_limit = 16;
const char *release_str = Message::ReleaseString();
time_t release_time = Message::ReleaseDate();
@@ -2036,6 +2043,10 @@ struct VerificPass : public Pass {
mode_nosva = true;
continue;
}
+ if (args[argidx] == "-L" && argidx+1 < GetSize(args)) {
+ verific_sva_fsm_limit = atoi(args[++argidx].c_str());
+ continue;
+ }
if (args[argidx] == "-n") {
mode_names = true;
continue;
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index cbd9314db..334a436af 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -101,6 +101,8 @@ void verific_import_sva_cover(VerificImporter *importer, Verific::Instance *inst
void verific_import_sva_trigger(VerificImporter *importer, Verific::Instance *inst);
bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net);
+extern int verific_sva_fsm_limit;
+
YOSYS_NAMESPACE_END
#endif
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 85b842186..cdc9ece8c 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -466,13 +466,14 @@ struct SvaFsm
dnode.ctrl.sort_and_unify();
- if (GetSize(dnode.ctrl) > 16) {
+ if (GetSize(dnode.ctrl) > verific_sva_fsm_limit) {
if (verific_verbose >= 2) {
log(" detected state explosion in DFSM generation:\n");
dump();
log(" ctrl signal: %s\n", log_signal(dnode.ctrl));
}
- log_error("SVA DFSM state ctrl signal has %d (>16) bits. Stopping to prevent exponential design size explosion.\n", GetSize(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);
}
for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++)