From 9a2a8cd97b8ff155c137045ee3654dcdc046c401 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 1 Mar 2018 11:40:43 +0100 Subject: [PATCH] Fixes and improvements in Verific SVA importer Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 14 ++- frontends/verific/verific.h | 2 +- frontends/verific/verificsva.cc | 203 ++++++++++++++++++++------------ 3 files changed, 136 insertions(+), 83 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 415035ff1..b7c99e4a3 100644 --- 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 28a0c174b..2ca01072f 100644 --- 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 verific_sva_prims; diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 2185e4596..e6430e9c5 100644 --- 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 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); -- 2.30.2