Add "verific -L <int>" option

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 1dd6d7e24783646265ef28c2828ed648777a3be2..c5fa5831332fe0c41d36f74e235eb4cd5817caff 100644 (file)
--- 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 cbd9314dbc4615040f62a510f07cd7e1edd6478b..334a436af5fe7e6c51b9cfab8ec83e1d2139e894 100644 (file)
--- 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 85b8421862efe7ec00a048d972174c84bf7ffd31..cdc9ece8c6fcfca1d7b6d7bbbc8a88edd97f976a 100644 (file)
--- 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++)