Fixes and improvements in Verific SVA importer

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

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 415035ff19a9d6cebcde15a0794d0b798294554a..b7c99e4a3d1ecdf9ab1960e1e9877ed1e25869b6 100644 (file)
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -60,7 +60,7 @@ using namespace Verific;
 #ifdef YOSYS_ENABLE_VERIFIC
 YOSYS_NAMESPACE_BEGIN
 
-bool verific_verbose;
+int verific_verbose;
 string verific_error_msg;
 
 void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
@@ -1422,8 +1422,8 @@ struct VerificPass : public Pass {
                log("  -extnets\n");
                log("    Resolve references to external nets by adding module ports as needed.\n");
                log("\n");
-               log("  -v\n");
-               log("    Verbose log messages.\n");
+               log("  -v, -vv\n");
+               log("    Verbose log messages. (-vv is even more verbose than -v.)\n");
                log("\n");
                log("The following additional import options are useful for debugging the Verific\n");
                log("bindings (for Yosys and/or Verific developers):\n");
@@ -1459,7 +1459,7 @@ struct VerificPass : public Pass {
                veri_file::DefineCmdLineMacro("VERIFIC");
                veri_file::DefineCmdLineMacro("SYNTHESIS");
 
-               verific_verbose = false;
+               verific_verbose = 0;
 
                const char *release_str = Message::ReleaseString();
                time_t release_time = Message::ReleaseDate();
@@ -1607,7 +1607,11 @@ struct VerificPass : public Pass {
                                        continue;
                                }
                                if (args[argidx] == "-v") {
-                                       verific_verbose = true;
+                                       verific_verbose = 1;
+                                       continue;
+                               }
+                               if (args[argidx] == "-vv") {
+                                       verific_verbose = 2;
                                        continue;
                                }
                                if (args[argidx] == "-d" && argidx+1 < GetSize(args)) {

diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 28a0c174b64b6bf0a9f8c80976503e488df3db1e..2ca01072fbc4847bd9ce8af58a621054a9f3490c 100644 (file)
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -23,7 +23,7 @@
 
 YOSYS_NAMESPACE_BEGIN
 
-extern bool verific_verbose;
+extern int verific_verbose;
 
 extern pool<int> verific_sva_prims;
 

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 2185e4596063a7be9805a5ef4b37e3c60f0738cb..e6430e9c5188116255b5cb17a441d1a85bf1084b 100644 (file)
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -113,7 +113,6 @@ struct SvaFsm
        bool clockpol;
 
        SigBit trigger_sig = State::S1, disable_sig;
-       SigBit accept_sig = State::Sz, reject_sig = State::Sz;
        SigBit throughout_sig = State::S1;
        bool materialized = false;
 
@@ -123,6 +122,9 @@ struct SvaFsm
        int startNode, acceptNode;
        vector<SvaNFsmNode> nodes;
 
+       SigBit final_accept_sig = State::Sx;
+       SigBit final_reject_sig = State::Sx;
+
        SvaFsm(Module *mod, SigBit clk, bool clkpol, SigBit dis = State::S0, SigBit trig = State::S1)
        {
                module = mod;
@@ -323,13 +325,14 @@ struct SvaFsm
                        }
                }
 
-               return state_sig[acceptNode];
+               final_accept_sig = state_sig[acceptNode];
+               return final_accept_sig;
        }
 
        // ----------------------------------------------------
        // Generating quantifier-based NFSM circuit to acquire reject signal
 
-       SigBit getAnyAllRejectWorker(bool allMode)
+       SigBit getAnyAllRejectWorker(bool /* allMode */)
        {
                // FIXME
                log_abort();
@@ -531,104 +534,144 @@ struct SvaFsm
 
                if (accept_sigptr)
                {
-                       if (GetSize(reject_sig) == 0)
-                               *accept_sigptr = State::S0;
-                       else if (GetSize(reject_sig) == 1)
-                               *accept_sigptr = reject_sig;
+                       if (GetSize(accept_sig) == 0)
+                               final_accept_sig = State::S0;
+                       else if (GetSize(accept_sig) == 1)
+                               final_accept_sig = accept_sig;
                        else
-                               *accept_sigptr = module->ReduceOr(NEW_ID, reject_sig);
+                               final_accept_sig = module->ReduceOr(NEW_ID, accept_sig);
+                       *accept_sigptr = final_accept_sig;
                }
 
                if (GetSize(reject_sig) == 0)
-                       return State::S0;
-
-               if (GetSize(reject_sig) == 1)
-                       return reject_sig;
+                       final_reject_sig = State::S0;
+               else if (GetSize(reject_sig) == 1)
+                       final_reject_sig = reject_sig;
+               else
+                       final_reject_sig = module->ReduceOr(NEW_ID, reject_sig);
 
-               return module->ReduceOr(NEW_ID, reject_sig);
+               return final_reject_sig;
        }
 
        // ----------------------------------------------------
        // State dump for verbose log messages
 
-       void dump()
+       void dump_nodes()
        {
-               if (!nodes.empty())
+               if (nodes.empty())
+                       return;
+
+               log("      non-deterministic encoding:\n");
+               for (int i = 0; i < GetSize(nodes); i++)
                {
-                       log("      non-deterministic encoding:\n");
-                       for (int i = 0; i < GetSize(nodes); i++)
-                       {
-                               log("        node %d:%s\n", i, i == startNode ? " [start]" : i == acceptNode ? " [accept]" : "");
+                       log("        node %d:%s\n", i, i == startNode ? " [start]" : i == acceptNode ? " [accept]" : "");
 
-                               for (auto &it : nodes[i].edges) {
-                                       if (it.second != State::S1)
-                                               log("          egde %s -> %d\n", log_signal(it.second), it.first);
-                                       else
-                                               log("          egde -> %d\n", it.first);
-                               }
+                       for (auto &it : nodes[i].edges) {
+                               if (it.second != State::S1)
+                                       log("          egde %s -> %d\n", log_signal(it.second), it.first);
+                               else
+                                       log("          egde -> %d\n", it.first);
+                       }
 
-                               for (auto &it : nodes[i].links) {
-                                       if (it.second != State::S1)
-                                               log("          link %s -> %d\n", log_signal(it.second), it.first);
-                                       else
-                                               log("          link -> %d\n", it.first);
-                               }
+                       for (auto &it : nodes[i].links) {
+                               if (it.second != State::S1)
+                                       log("          link %s -> %d\n", log_signal(it.second), it.first);
+                               else
+                                       log("          link -> %d\n", it.first);
                        }
                }
+       }
+
+       void dump_unodes()
+       {
+               if (unodes.empty())
+                       return;
 
-               if (!unodes.empty())
+               log("      unlinked non-deterministic encoding:\n");
+               for (int i = 0; i < GetSize(unodes); i++)
                {
-                       log("      unlinked non-deterministic encoding:\n");
-                       for (int i = 0; i < GetSize(unodes); i++)
-                       {
-                               if (!unodes[i].reachable)
-                                       continue;
+                       if (!unodes[i].reachable)
+                               continue;
 
-                               log("        unode %d:%s\n", i, i == startNode ? " [start]" : "");
+                       log("        unode %d:%s\n", i, i == startNode ? " [start]" : "");
 
-                               for (auto &it : unodes[i].edges) {
-                                       if (!it.second.empty())
-                                               log("          egde %s -> %d\n", log_signal(it.second), it.first);
-                                       else
-                                               log("          egde -> %d\n", it.first);
-                               }
+                       for (auto &it : unodes[i].edges) {
+                               if (!it.second.empty())
+                                       log("          egde %s -> %d\n", log_signal(it.second), it.first);
+                               else
+                                       log("          egde -> %d\n", it.first);
+                       }
 
-                               for (auto &ctrl : unodes[i].accept) {
-                                       if (!ctrl.empty())
-                                               log("          accept %s\n", log_signal(ctrl));
-                                       else
-                                               log("          accept\n");
-                               }
+                       for (auto &ctrl : unodes[i].accept) {
+                               if (!ctrl.empty())
+                                       log("          accept %s\n", log_signal(ctrl));
+                               else
+                                       log("          accept\n");
                        }
                }
+       }
 
-               if (!dnodes.empty())
+       void dump_dnodes()
+       {
+               if (dnodes.empty())
+                       return;
+
+               log("      deterministic encoding:\n");
+               for (auto &it : dnodes)
                {
-                       log("      deterministic encoding:\n");
-                       for (auto &it : dnodes)
-                       {
-                               log("        dnode {");
-                               for (int i = 0; i < GetSize(it.first); i++)
-                                       log("%s%d", i ? "," : "", it.first[i]);
-                               log("}:%s\n", GetSize(it.first) == 1 && it.first[0] == startNode ? " [start]" : "");
-
-                               log("          ctrl %s\n", log_signal(it.second.ctrl));
-
-                               for (auto &edge : it.second.edges) {
-                                       log("          edge %s -> {", log_signal(edge.second));
-                                       for (int i = 0; i < GetSize(edge.first); i++)
-                                               log("%s%d", i ? "," : "", edge.first[i]);
-                                       log("}\n");
-                               }
+                       log("        dnode {");
+                       for (int i = 0; i < GetSize(it.first); i++)
+                               log("%s%d", i ? "," : "", it.first[i]);
+                       log("}:%s\n", GetSize(it.first) == 1 && it.first[0] == startNode ? " [start]" : "");
+
+                       log("          ctrl %s\n", log_signal(it.second.ctrl));
+
+                       for (auto &edge : it.second.edges) {
+                               log("          edge %s -> {", log_signal(edge.second));
+                               for (int i = 0; i < GetSize(edge.first); i++)
+                                       log("%s%d", i ? "," : "", edge.first[i]);
+                               log("}\n");
+                       }
 
-                               for (auto &value : it.second.accept)
-                                       log("          accept %s\n", log_signal(value));
+                       for (auto &value : it.second.accept)
+                               log("          accept %s\n", log_signal(value));
 
-                               for (auto &value : it.second.reject)
-                                       log("          reject %s\n", log_signal(value));
-                       }
+                       for (auto &value : it.second.reject)
+                               log("          reject %s\n", log_signal(value));
                }
        }
+
+       void dump()
+       {
+               if (!nodes.empty())
+                       log("      number of NFSM states: %d\n", GetSize(nodes));
+
+               if (!unodes.empty()) {
+                       int count = 0;
+                       for (auto &unode : unodes)
+                               if (unode.reachable)
+                                       count++;
+                       log("      number of reachable UFSM states: %d\n", count);
+               }
+
+               if (!dnodes.empty())
+                       log("      number of DFSM states: %d\n", GetSize(dnodes));
+
+               if (verific_verbose >= 2) {
+                       dump_nodes();
+                       dump_unodes();
+                       dump_dnodes();
+               }
+
+               if (trigger_sig != State::S1)
+                       log("      trigger signal: %s\n", log_signal(trigger_sig));
+
+               if (final_accept_sig != State::Sx)
+                       log("      accept signal: %s\n", log_signal(final_accept_sig));
+
+               if (final_reject_sig != State::Sx)
+                       log("      reject signal: %s\n", log_signal(final_reject_sig));
+       }
 };
 
 PRIVATE_NAMESPACE_END
@@ -941,12 +984,18 @@ struct VerificSvaImporter
                                SigBit until_match = until_fsm.getAccept();
                                SigBit not_until_match = module->Not(NEW_ID, until_match);
 
-                               Wire *extend_antecedent_match_q = module->addWire(NEW_ID);
-                               extend_antecedent_match_q->attributes["\\init"] = Const(0, 1);
-                               antecedent_match = module->Or(NEW_ID, antecedent_match, extend_antecedent_match_q);
+                               if (verific_verbose) {
+                                       log("    Until FSM:\n");
+                                       until_fsm.dump();
+                               }
+
+                               Wire *antecedent_match_q = module->addWire(NEW_ID);
+                               antecedent_match_q->attributes["\\init"] = Const(0, 1);
+
+                               antecedent_match = module->Or(NEW_ID, antecedent_match, antecedent_match_q);
+                               antecedent_match = module->And(NEW_ID, antecedent_match, not_until_match);
 
-                               SigBit extend_antecedent_match = module->And(NEW_ID, not_until_match, antecedent_match);
-                               module->addDff(NEW_ID, clock, extend_antecedent_match, extend_antecedent_match_q, clockpol);
+                               module->addDff(NEW_ID, clock, antecedent_match, antecedent_match_q, clockpol);
                        }
 
                        SvaFsm consequent_fsm(module, clock, clockpol, disable_iff, antecedent_match);