diff options
| -rw-r--r-- | frontends/verific/verific.cc | 91 | ||||
| -rw-r--r-- | frontends/verific/verific.h | 10 | ||||
| -rw-r--r-- | frontends/verific/verificsva.cc | 742 |
3 files changed, 172 insertions, 671 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index e85e6cf71..fc0f72be8 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -60,6 +60,7 @@ using namespace Verific; #ifdef YOSYS_ENABLE_VERIFIC YOSYS_NAMESPACE_BEGIN +bool 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) @@ -97,9 +98,9 @@ string get_full_netlist_name(Netlist *nl) // ================================================================== -VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) : +VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names) : mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva), - mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose) + mode_names(mode_names) { } @@ -642,13 +643,13 @@ void VerificImporter::merge_past_ffs_clock(pool<RTLIL::Cell*> &candidates, SigBi SigSpec sig_q = module->addWire(NEW_ID, GetSize(sig_d)); RTLIL::Cell *new_ff = module->addDff(NEW_ID, clock, sig_d, sig_q, clock_pol); - if (verbose) + if (verific_verbose) log(" merging single-bit past_ffs into new %d-bit ff %s.\n", GetSize(sig_d), log_id(new_ff)); for (int i = 0; i < GetSize(sig_d); i++) for (auto old_ff : dbits_db[sig_d[i]]) { - if (verbose) + if (verific_verbose) log(" replacing old ff %s on bit %d.\n", log_id(old_ff), i); SigBit old_q = old_ff->getPort("\\Q"); @@ -711,38 +712,12 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se Instance *inst; PortRef *pr; - if (!mode_nosvapp) - { - vector<Instance*> asserts, assumes, covers; - - FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) - { - if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT) - asserts.push_back(inst); - - if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) - assumes.push_back(inst); - - if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER) - covers.push_back(inst); - } - - for (auto inst : asserts) - svapp_assert(inst); - - for (auto inst : assumes) - svapp_assume(inst); - - for (auto inst : covers) - svapp_cover(inst); - } - FOREACH_PORT_OF_NETLIST(nl, mi, port) { if (port->Bus()) continue; - if (verbose) + if (verific_verbose) log(" importing port %s.\n", port->Name()); RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name())); @@ -768,7 +743,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus) { - if (verbose) + if (verific_verbose) log(" importing portbus %s.\n", portbus->Name()); RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size()); @@ -882,7 +857,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se anyseq_nets.insert(net); if (net_map.count(net)) { - if (verbose) + if (verific_verbose) log(" skipping net %s.\n", net->Name()); continue; } @@ -892,7 +867,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se RTLIL::IdString wire_name = module->uniquify(mode_names || net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID); - if (verbose) + if (verific_verbose) log(" importing net %s as %s.\n", net->Name(), log_id(wire_name)); RTLIL::Wire *wire = module->addWire(wire_name); @@ -916,7 +891,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se { RTLIL::IdString wire_name = module->uniquify(mode_names || netbus->IsUserDeclared() ? RTLIL::escape_id(netbus->Name()) : NEW_ID); - if (verbose) + if (verific_verbose) log(" importing netbus %s as %s.\n", netbus->Name(), log_id(wire_name)); RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size()); @@ -958,7 +933,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se } else { - if (verbose) + if (verific_verbose) log(" skipping netbus %s.\n", netbus->Name()); } @@ -1022,7 +997,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se { RTLIL::IdString inst_name = module->uniquify(mode_names || inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID); - if (verbose) + if (verific_verbose) log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name)); if (inst->Type() == PRIM_PWR) { @@ -1134,7 +1109,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se sig_o.append(net_map_at(inst->GetOutputBit(i))); } - if (verbose) { + if (verific_verbose) { log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); log(" XNOR with A=%s, B=%s, Y=%s.\n", @@ -1156,7 +1131,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se SigSpec sig_o = net_map_at(inst->GetOutput()); SigSpec sig_q = module->addWire(NEW_ID); - if (verbose) { + if (verific_verbose) { log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); log(" XNOR with A=%s, B=%s, Y=%s.\n", @@ -1177,7 +1152,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se SigBit sig_d = net_map_at(inst->GetInput1()); SigBit sig_q = net_map_at(inst->GetOutput()); - if (verbose) + if (verific_verbose) log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); @@ -1188,7 +1163,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se } if (!mode_keep && verific_sva_prims.count(inst->Type())) { - if (verbose) + if (verific_verbose) log(" skipping SVA cell in non k-mode\n"); continue; } @@ -1215,11 +1190,11 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se dict<IdString, vector<SigBit>> cell_port_conns; - if (verbose) + if (verific_verbose) log(" ports in verific db:\n"); FOREACH_PORTREF_OF_INST(inst, mi2, pr) { - if (verbose) + if (verific_verbose) log(" .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name()); const char *port_name = pr->GetPort()->Name(); int port_offset = 0; @@ -1238,11 +1213,11 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se sigvec[port_offset] = net_map_at(pr->GetNet()); } - if (verbose) + if (verific_verbose) log(" ports in yosys db:\n"); for (auto &it : cell_port_conns) { - if (verbose) + if (verific_verbose) log(" .%s(%s)\n", log_id(it.first), log_signal(it.second)); cell->setPort(it.first, it.second); } @@ -1292,7 +1267,6 @@ VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst) struct VerificExtNets { int portname_cnt = 0; - bool verbose = false; // a map from Net to the same Net one level up in the design hierarchy std::map<Net*, Net*> net_level_up; @@ -1347,7 +1321,7 @@ struct VerificExtNets if (!net->IsExternalTo(nl)) continue; - if (verbose) + if (verific_verbose) log("Fixing external net reference on port %s.%s.%s:\n", get_full_netlist_name(nl).c_str(), inst->Name(), port->Name()); while (net->IsExternalTo(nl)) @@ -1355,12 +1329,12 @@ struct VerificExtNets Net *newnet = get_net_level_up(net); if (newnet == net) break; - if (verbose) + if (verific_verbose) log(" external net: %s.%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name()); net = newnet; } - if (verbose) + if (verific_verbose) log(" final net: %s.%s%s\n", get_full_netlist_name(net->Owner()).c_str(), net->Name(), net->IsExternalTo(nl) ? " (external)" : ""); todo_connect.push_back(tuple<Instance*, Port*, Net*>(inst, port, net)); } @@ -1444,9 +1418,6 @@ struct VerificPass : public Pass { log(" -nosva\n"); log(" Ignore SVA properties, do not infer checker logic.\n"); log("\n"); - log(" -nosvapp\n"); - log(" Disable SVA properties pre-processing pass. This implies -nosva.\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"); @@ -1469,6 +1440,8 @@ struct VerificPass : public Pass { veri_file::DefineCmdLineMacro("VERIFIC"); veri_file::DefineCmdLineMacro("SYNTHESIS"); + verific_verbose = false; + const char *release_str = Message::ReleaseString(); time_t release_time = Message::ReleaseDate(); char *release_tmstr = ctime(&release_time); @@ -1581,8 +1554,8 @@ struct VerificPass : public Pass { { std::set<Netlist*> nl_todo, nl_done; bool mode_all = false, mode_gates = false, mode_keep = false; - bool mode_nosva = false, mode_nosvapp = false, mode_names = false; - bool verbose = false, flatten = false, extnets = false; + bool mode_nosva = false, mode_names = false; + bool flatten = false, extnets = false; string dumpfile; for (argidx++; argidx < GetSize(args); argidx++) { @@ -1610,17 +1583,12 @@ struct VerificPass : public Pass { mode_nosva = true; continue; } - if (args[argidx] == "-nosvapp") { - mode_nosva = true; - mode_nosvapp = true; - continue; - } if (args[argidx] == "-n") { mode_names = true; continue; } if (args[argidx] == "-v") { - verbose = true; + verific_verbose = true; continue; } if (args[argidx] == "-d" && argidx+1 < GetSize(args)) { @@ -1697,7 +1665,6 @@ struct VerificPass : public Pass { if (extnets) { VerificExtNets worker; - worker.verbose = verbose; for (auto nl : nl_todo) worker.run(nl); } @@ -1710,7 +1677,7 @@ struct VerificPass : public Pass { while (!nl_todo.empty()) { Netlist *nl = *nl_todo.begin(); if (nl_done.count(nl) == 0) { - VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose); + VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_names); importer.import_netlist(design, nl, nl_todo); } nl_todo.erase(nl); diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index 4f1cb5d0f..28a0c174b 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -23,6 +23,8 @@ YOSYS_NAMESPACE_BEGIN +extern bool verific_verbose; + extern pool<int> verific_sva_prims; struct VerificImporter; @@ -42,9 +44,9 @@ struct VerificImporter std::map<Verific::Net*, RTLIL::SigBit> net_map; std::map<Verific::Net*, Verific::Net*> sva_posedge_map; - bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose; + bool mode_gates, mode_keep, mode_nosva, mode_names; - VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose); + VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names); RTLIL::SigBit net_map_at(Verific::Net *net); @@ -70,10 +72,6 @@ void import_sva_assert(VerificImporter *importer, Verific::Instance *inst); void import_sva_assume(VerificImporter *importer, Verific::Instance *inst); void import_sva_cover(VerificImporter *importer, Verific::Instance *inst); -void svapp_assert(Verific::Instance *inst); -void svapp_assume(Verific::Instance *inst); -void svapp_cover(Verific::Instance *inst); - YOSYS_NAMESPACE_END #endif diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index ceaca287d..5857c4496 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -72,11 +72,23 @@ using namespace Verific; PRIVATE_NAMESPACE_BEGIN -struct SvaFsmNode +// Non-deterministic FSM +struct SvaNFsmNode { + // Edge: Activate the target node if ctrl signal is true, consumes clock cycle + // Link: Activate the target node if ctrl signal is true, doesn't consume clock cycle vector<pair<int, SigBit>> edges, links; }; +// Non-deterministic FSM after resolving links +struct SvaUFsmNode +{ + // Edge: Activate the target node if all bits in ctrl signal are true, consumes clock cycle + // Accept: This node functions as an accept node if all bits in ctrl signal are true + vector<pair<int, SigSpec>> edges; + vector<SigSpec> accept; +}; + struct SvaFsm { Module *module; @@ -91,8 +103,11 @@ struct SvaFsm vector<SigBit> disable_stack; vector<SigBit> throughout_stack; - int startNode, acceptNode, rejectNode; - vector<SvaFsmNode> nodes; + int startNode, acceptNode; + vector<SvaNFsmNode> nodes; + + // ---------------------------------------------------- + // API for creating FSM SvaFsm(Module *mod, SigBit clk, bool clkpol, SigBit dis = State::S0, SigBit trig = State::S1) { @@ -104,7 +119,6 @@ struct SvaFsm startNode = createNode(); acceptNode = createNode(); - rejectNode = createNode(); } void pushDisable(SigBit sig) @@ -149,32 +163,12 @@ struct SvaFsm throughout_stack.pop_back(); } - SigBit getAccept() - { - if (accept_sig != State::Sz) - return accept_sig; - - log_assert(!materialized); - accept_sig = module->addWire(NEW_ID); - return accept_sig; - } - - SigBit getReject() - { - if (reject_sig != State::Sz) - return reject_sig; - - log_assert(!materialized); - reject_sig = module->addWire(NEW_ID); - return reject_sig; - } - int createNode() { log_assert(!materialized); int idx = GetSize(nodes); - nodes.push_back(SvaFsmNode()); + nodes.push_back(SvaNFsmNode()); return idx; } @@ -217,15 +211,19 @@ struct SvaFsm make_link_order(order, it.first, order[node]+1); } - void materialize_ndfsm() + // ---------------------------------------------------- + // API for generating NFSM circuit to acquire accept signal + + SigBit getAccept() { log_assert(!materialized); materialized = true; - vector<SigBit> next_state_sig(GetSize(nodes)); + vector<Wire*> state_wire(GetSize(nodes)); vector<SigBit> state_sig(GetSize(nodes)); + vector<SigBit> next_state_sig(GetSize(nodes)); - // Create state FFs + // Create state signals { SigBit not_disable = State::S1; @@ -235,14 +233,10 @@ struct SvaFsm for (int i = 0; i < GetSize(nodes); i++) { - next_state_sig[i] = module->addWire(NEW_ID); - Wire *w = module->addWire(NEW_ID); - w->attributes["\\init"] = Const(0, 1); + state_wire[i] = w; state_sig[i] = w; - module->addDff(NEW_ID, clock, next_state_sig[i], state_sig[i], clockpol); - if (i == startNode) state_sig[i] = module->Or(NEW_ID, state_sig[i], trigger_sig); @@ -295,86 +289,92 @@ struct SvaFsm for (int i = 0; i < GetSize(nodes); i++) { if (GetSize(activate_sig[i]) == 0) - activate_bit[i] = State::S0; + next_state_sig[i] = State::S0; else if (GetSize(activate_sig[i]) == 1) - activate_bit[i] = activate_sig[i]; + next_state_sig[i] = activate_sig[i]; else - activate_bit[i] = module->ReduceOr(NEW_ID, activate_sig[i]); - } - - if (activate_bit[rejectNode] != State::S0) - { - SigBit not_rej = module->Not(NEW_ID, next_state_sig[rejectNode]); - for (int i = 0; i < GetSize(nodes); i++) - if (i != rejectNode && activate_bit[i] != State::S0) - activate_bit[i] = module->And(NEW_ID, activate_bit[i], not_rej); - activate_bit[rejectNode] = State::S0; - } - - for (int i = 0; i < GetSize(nodes); i++) { - module->connect(next_state_sig[i], activate_bit[i]); + next_state_sig[i] = module->ReduceOr(NEW_ID, activate_sig[i]); } } - // Construct output signals - - if (accept_sig != State::Sz) { - module->connect(accept_sig, state_sig[acceptNode]); - } + // Create state FFs - if (reject_sig != State::Sz) + for (int i = 0; i < GetSize(nodes); i++) { - SigBit fsm_active = module->ReduceOr(NEW_ID, state_sig); - SigBit fsm_next_active = module->ReduceOr(NEW_ID, next_state_sig); - module->addEq(NEW_ID, {state_sig[acceptNode], fsm_next_active, fsm_active}, SigSpec(1, 3), reject_sig); + if (next_state_sig[i] != State::S0) { + state_wire[i]->attributes["\\init"] = Const(0, 1); + module->addDff(NEW_ID, clock, next_state_sig[i], state_wire[i], clockpol); + } else { + module->connect(state_wire[i], State::S0); + } } + + return state_sig[acceptNode]; } - void materialize_dfsm() + // ---------------------------------------------------- + // API for generating quantifier-based NFSM circuit to acquire reject signal + + SigBit getAnyAllRejectWorker(bool allMode) { // FIXME log_abort(); } - bool is_linear() + SigBit getAnyReject() { - for (int i = 0; i < GetSize(nodes); i++) - if (GetSize(nodes[i].edges) + GetSize(nodes[i].links) > 1) - return false; - return true; + return getAnyAllRejectWorker(false); + } + + SigBit getAllReject() + { + return getAnyAllRejectWorker(true); + } + + // ---------------------------------------------------- + // API for generating DFSM circuit to acquire reject signal + + SigBit getReject() + { + // FIXME + log("-----------------\n"); + dump(); + log_abort(); } + // ---------------------------------------------------- + // State dump for verbose log messages + void dump() { - log("-----------\n"); - for (int i = 0; i < GetSize(nodes); i++) + if (!nodes.empty()) { - log("node %d:\n", i); - - if (i == startNode) - log(" startNode\n"); + log(" non-deterministic encoding:\n"); + for (int i = 0; i < GetSize(nodes); i++) + { + log(" node %d:\n", i); - if (i == rejectNode) - log(" rejectNode\n"); + if (i == startNode) + log(" startNode\n"); - if (i == acceptNode) - log(" acceptNode\n"); + if (i == acceptNode) + log(" acceptNode\n"); - 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); + } } } - log("-----------\n"); } }; @@ -414,7 +414,7 @@ struct VerificSvaImporter Instance *root = nullptr; SigBit clock = State::Sx; - bool clock_posedge = false; + bool clockpol = false; SigBit disable_iff = State::S0; @@ -454,124 +454,6 @@ struct VerificSvaImporter Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); } // ---------------------------------------------------------- - // SVA AST Types - - struct svatype_t - { - bool flag_linear = true; - }; - - std::map<Instance*, svatype_t> svatype_cache; - - void svatype_visit_child(svatype_t &entry, Instance *inst) - { - if (inst == nullptr) - return; - - const svatype_t &child_entry = svatype(inst); - entry.flag_linear &= child_entry.flag_linear; - } - - const svatype_t &svatype(Instance *inst) - { - if (svatype_cache.count(inst) != 0) - return svatype_cache.at(inst); - - svatype_t &entry = svatype_cache[inst]; - - if (inst == nullptr) - return entry; - - if (inst->Type() == PRIM_SVA_SEQ_CONCAT || inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT) - { - const char *sva_low_s = inst->GetAttValue("sva:low"); - const char *sva_high_s = inst->GetAttValue("sva:high"); - - int sva_low = atoi(sva_low_s); - int sva_high = atoi(sva_high_s); - bool sva_inf = !strcmp(sva_high_s, "$"); - - if (sva_inf || sva_low != sva_high) - entry.flag_linear = false; - } - - svatype_visit_child(entry, get_ast_input(inst)); - svatype_visit_child(entry, get_ast_input1(inst)); - svatype_visit_child(entry, get_ast_input2(inst)); - svatype_visit_child(entry, get_ast_input3(inst)); - svatype_visit_child(entry, get_ast_control(inst)); - - return entry; - } - - // ---------------------------------------------------------- - // SVA Preprocessor - - Net *rewrite_input(Instance *inst) { return rewrite(get_ast_input(inst), inst->GetInput()); } - Net *rewrite_input1(Instance *inst) { return rewrite(get_ast_input1(inst), inst->GetInput1()); } - Net *rewrite_input2(Instance *inst) { return rewrite(get_ast_input2(inst), inst->GetInput2()); } - Net *rewrite_input3(Instance *inst) { return rewrite(get_ast_input3(inst), inst->GetInput3()); } - Net *rewrite_control(Instance *inst) { return rewrite(get_ast_control(inst), inst->GetControl()); } - - Net *rewrite(Instance *inst, Net *default_net = nullptr) - { - if (inst == nullptr) - return default_net; - - if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME || - inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) { - Net *new_net = rewrite(get_ast_input(inst)); - if (new_net) { - inst->Disconnect(inst->View()->GetInput()); - inst->Connect(inst->View()->GetInput(), new_net); - } - return default_net; - } - - if (inst->Type() == PRIM_SVA_AT || inst->Type() == PRIM_SVA_DISABLE_IFF) { - Net *new_net = rewrite(get_ast_input2(inst)); - if (new_net) { - inst->Disconnect(inst->View()->GetInput2()); - inst->Connect(inst->View()->GetInput2(), new_net); - } - return default_net; - } - - if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) - { - if (mode_cover) { - did_something = true; - Net *new_in1 = rewrite_input1(inst); - Net *new_in2 = rewrite_input2(inst); - return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile()); - } - return default_net; - } - - if (inst->Type() == PRIM_SVA_NOT) - { - if (mode_assert || mode_assume) { - did_something = true; - Net *new_in = rewrite_input(inst); - Net *net_zero = netlist->Gnd(inst->Linefile()); - return netlist->SvaBinary(PRIM_SVA_OVERLAPPED_IMPLICATION, new_in, net_zero, inst->Linefile()); - } - return default_net; - } - - return default_net; - } - - void rewrite() - { - netlist = root->Owner(); - do { - did_something = false; - rewrite(root); - } while (did_something); - } - - // ---------------------------------------------------------- // SVA Importer int parse_sequence(SvaFsm *fsm, int start_node, Net *net) @@ -687,6 +569,10 @@ struct VerificSvaImporter 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())); + RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); // parse SVA property clock event @@ -717,25 +603,25 @@ struct VerificSvaImporter VerificClockEdge clock_edge(importer, get_ast_input1(at_node)); clock = clock_edge.clock_sig; - clock_posedge = clock_edge.posedge; + clockpol = clock_edge.posedge; // parse disable_iff expression - Net *sequence_net = at_node->GetInput2(); + Net *net = at_node->GetInput2(); while (1) { - Instance *sequence_node = net_to_ast_driver(sequence_net); + Instance *sequence_node = net_to_ast_driver(net); if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) { eventually = true; - sequence_net = sequence_node->GetInput(); + net = sequence_node->GetInput(); continue; } if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) { disable_iff = importer->net_map_at(sequence_node->GetInput1()); - sequence_net = sequence_node->GetInput2(); + net = sequence_node->GetInput2(); continue; } @@ -745,11 +631,11 @@ struct VerificSvaImporter // parse SVA sequence into trigger signal SigBit prop_okay; - Instance *inst = net_to_ast_driver(sequence_net); + Instance *inst = net_to_ast_driver(net); if (inst == nullptr) { - prop_okay = importer->net_map_at(sequence_net); + prop_okay = importer->net_map_at(net); } else if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || @@ -759,7 +645,7 @@ struct VerificSvaImporter Net *consequent_net = inst->GetInput2(); int node; - SvaFsm antecedent_fsm(module, clock, clock_posedge, disable_iff); + SvaFsm antecedent_fsm(module, clock, clockpol, disable_iff); node = parse_sequence(&antecedent_fsm, antecedent_fsm.startNode, antecedent_net); if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { int next_node = antecedent_fsm.createNode(); @@ -768,21 +654,50 @@ struct VerificSvaImporter } antecedent_fsm.createLink(node, antecedent_fsm.acceptNode); - SigBit antecedent_accept = antecedent_fsm.getAccept(); - antecedent_fsm.materialize_ndfsm(); - antecedent_fsm.dump(); + SigBit antecedent_match = antecedent_fsm.getAccept(); - SvaFsm consequent_fsm(module, clock, clock_posedge, disable_iff, antecedent_accept); + if (verific_verbose) { + log(" Antecedent FSM:\n"); + antecedent_fsm.dump(); + } + + bool consequent_not = false; + Instance *consequent_inst = net_to_ast_driver(consequent_net); + + if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) { + consequent_not = true; + consequent_net = consequent_inst->GetInput(); + } + + SvaFsm consequent_fsm(module, clock, clockpol, disable_iff, antecedent_match); node = parse_sequence(&consequent_fsm, consequent_fsm.startNode, consequent_net); consequent_fsm.createLink(node, consequent_fsm.acceptNode); - SigBit consequent_reject = consequent_fsm.getReject(); - prop_okay = module->Not(NEW_ID, consequent_reject); + if (mode_cover) { + prop_okay = consequent_not ? consequent_fsm.getReject() : consequent_fsm.getAccept(); + } else { + SigBit consequent_match = consequent_not ? consequent_fsm.getAccept() : consequent_fsm.getReject(); + prop_okay = module->Not(NEW_ID, consequent_match); + } + + if (verific_verbose) { + log(" Consequent FSM:\n"); + antecedent_fsm.dump(); + } + } + else + if (inst->Type() == PRIM_SVA_NOT || mode_cover) + { + SvaFsm fsm(module, clock, clockpol, disable_iff); + int node = parse_sequence(&fsm, fsm.startNode, mode_cover ? net : inst->GetInput()); + fsm.createLink(node, fsm.acceptNode); + SigBit accept = fsm.getAccept(); + prop_okay = module->Not(NEW_ID, accept); - if (consequent_fsm.is_linear()) - consequent_fsm.materialize_ndfsm(); - else - log_error("Currently only linear sequences are allowed as impliciation consequent.\n"); + if (verific_verbose) { + log(" Sequence FSM:\n"); + fsm.dump(); + } } else { @@ -798,7 +713,7 @@ struct VerificSvaImporter Wire *prop_okay_q = module->addWire(NEW_ID); prop_okay_q->attributes["\\init"] = Const(mode_cover ? 0 : 1, 1); - module->addDff(NEW_ID, clock, prop_okay, prop_okay_q, clock_posedge); + module->addDff(NEW_ID, clock, prop_okay, prop_okay_q, clockpol); // generate assert/assume/cover cell @@ -816,387 +731,8 @@ struct VerificSvaImporter importer->import_attributes(c->attributes, root); } - -#if 0 - // ---------------------------------------------------------- - // Old SVA Importer - - vector<SigBit> sva_until_list_inclusive; - vector<SigBit> sva_until_list_exclusive; - vector<vector<SigBit>*> sva_sequence_alive_list; - - struct sequence_t { - int length = 0; - SigBit sig_a = State::S1; - SigBit sig_en = State::S1; - }; - - void sequence_cond(sequence_t &seq, SigBit cond) - { - seq.sig_a = module->And(NEW_ID, seq.sig_a, cond); - } - - void sequence_ff(sequence_t &seq) - { - if (disable_iff != State::S0) - seq.sig_en = module->Mux(NEW_ID, seq.sig_en, State::S0, disable_iff); - - for (auto &expr : sva_until_list_exclusive) - seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr); - - Wire *sig_a_q = module->addWire(NEW_ID); - sig_a_q->attributes["\\init"] = Const(0, 1); - - Wire *sig_en_q = module->addWire(NEW_ID); - sig_en_q->attributes["\\init"] = Const(0, 1); - - for (auto list : sva_sequence_alive_list) - list->push_back(module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en)); - - module->addDff(NEW_ID, clock, seq.sig_a, sig_a_q, clock_posedge); - module->addDff(NEW_ID, clock, seq.sig_en, sig_en_q, clock_posedge); - - if (seq.length >= 0) - seq.length++; - - seq.sig_a = sig_a_q; - seq.sig_en = sig_en_q; - - for (auto &expr : sva_until_list_inclusive) - seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr); - } - - void combine_seq(sequence_t &seq, const sequence_t &other_seq) - { - if (seq.length != other_seq.length) - seq.length = -1; - - SigBit filtered_a = module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en); - SigBit other_filtered_a = module->LogicAnd(NEW_ID, other_seq.sig_a, other_seq.sig_en); - - seq.sig_a = module->LogicOr(NEW_ID, filtered_a, other_filtered_a); - seq.sig_en = module->LogicOr(NEW_ID, seq.sig_en, other_seq.sig_en); - } - - void combine_seq(sequence_t &seq, SigBit other_a, SigBit other_en) - { - SigBit filtered_a = module->LogicAnd(NEW_ID, seq.sig_a, seq.sig_en); - SigBit other_filtered_a = module->LogicAnd(NEW_ID, other_a, other_en); - - seq.length = -1; - seq.sig_a = module->LogicOr(NEW_ID, filtered_a, other_filtered_a); - seq.sig_en = module->LogicOr(NEW_ID, seq.sig_en, other_en); - } - - SigBit make_temporal_one_hot(SigBit enable = State::S1, SigBit *latched = nullptr) - { - Wire *state = module->addWire(NEW_ID); - state->attributes["\\init"] = State::S0; - - SigBit any = module->Anyseq(NEW_ID); - if (enable != State::S1) - any = module->LogicAnd(NEW_ID, any, enable); - - SigBit next_state = module->LogicOr(NEW_ID, state, any); - module->addDff(NEW_ID, clock, next_state, state, clock_posedge); - - if (latched != nullptr) - *latched = state; - - SigBit not_state = module->LogicNot(NEW_ID, state); - return module->LogicAnd(NEW_ID, next_state, not_state); - } - - SigBit make_permanent_latch(SigBit enable, bool async = false) - { - Wire *state = module->addWire(NEW_ID); - state->attributes["\\init"] = State::S0; - - SigBit next_state = module->LogicOr(NEW_ID, state, enable); - module->addDff(NEW_ID, clock, next_state, state, clock_posedge); - - return async ? next_state : state; - } - - void parse_sequence(sequence_t &seq, Net *n) - { - Instance *inst = net_to_ast_driver(n); - - // Regular expression - - if (inst == nullptr) { - sequence_cond(seq, importer->net_map_at(n)); - return; - } - - // SVA Primitives - - if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || - inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) - { - Instance *consequent = get_ast_input2(inst); - bool linear_consequent = svatype(consequent).flag_linear; - - parse_sequence(seq, inst->GetInput1()); - seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a); - - if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) - sequence_ff(seq); - - if (!linear_consequent && mode_assume) - log_error("Non-linear consequent is currently not supported in SVA assumptions.\n"); - - if (linear_consequent) - { - parse_sequence(seq, inst->GetInput2()); - } - else - { - SigBit activated; - seq.sig_en = make_temporal_one_hot(seq.sig_en, &activated); - - SigBit pass_latch_en = module->addWire(NEW_ID); - SigBit pass_latch = make_permanent_latch(pass_latch_en, true); - - vector<SigBit> alive_list; - sva_sequence_alive_list.push_back(&alive_list); - parse_sequence(seq, inst->GetInput2()); - sva_sequence_alive_list.pop_back(); - - module->addLogicAnd(NEW_ID, seq.sig_a, seq.sig_en, pass_latch_en); - alive_list.push_back(pass_latch); - - seq.length = -1; - seq.sig_a = module->ReduceOr(NEW_ID, SigSpec(alive_list)); - seq.sig_en = module->ReduceOr(NEW_ID, activated); - } - - return; - } - - if (inst->Type() == PRIM_SVA_SEQ_CONCAT) - { - const char *sva_low_s = inst->GetAttValue("sva:low"); - const char *sva_high_s = inst->GetAttValue("sva:high"); - - int sva_low = atoi(sva_low_s); - int sva_high = atoi(sva_high_s); - bool sva_inf = !strcmp(sva_high_s, "$"); - - parse_sequence(seq, inst->GetInput1()); - - for (int i = 0; i < sva_low; i++) - sequence_ff(seq); - - if (sva_inf) - { - SigBit latched_a = module->addWire(NEW_ID); - SigBit latched_en = module->addWire(NEW_ID); - combine_seq(seq, latched_a, latched_en); - - sequence_t seq_latched = seq; - sequence_ff(seq_latched); - module->connect(latched_a, seq_latched.sig_a); - module->connect(latched_en, seq_latched.sig_en); - } - else - { - for (int i = sva_low; i < sva_high; i++) - { - sequence_t last_seq = seq; - sequence_ff(seq); - combine_seq(seq, last_seq); - } - } - - parse_sequence(seq, inst->GetInput2()); - return; - } - - if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT) - { - const char *sva_low_s = inst->GetAttValue("sva:low"); - const char *sva_high_s = inst->GetAttValue("sva:high"); - - int sva_low = atoi(sva_low_s); - int sva_high = atoi(sva_high_s); - bool sva_inf = !strcmp(sva_high_s, "$"); - - parse_sequence(seq, inst->GetInput()); - - for (int i = 1; i < sva_low; i++) { - sequence_ff(seq); - parse_sequence(seq, inst->GetInput()); - } - - if (sva_inf) - { - SigBit latched_a = module->addWire(NEW_ID); - SigBit latched_en = module->addWire(NEW_ID); - combine_seq(seq, latched_a, latched_en); - - sequence_t seq_latched = seq; - sequence_ff(seq_latched); - parse_sequence(seq_latched, inst->GetInput()); - module->connect(latched_a, seq_latched.sig_a); - module->connect(latched_en, seq_latched.sig_en); - } - else - { - for (int i = sva_low; i < sva_high; i++) - { - sequence_t last_seq = seq; - sequence_ff(seq); - parse_sequence(seq, inst->GetInput()); - combine_seq(seq, last_seq); - } - } - - return; - } - - if (inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL || inst->Type() == PRIM_SVA_S_UNTIL || - inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH) - { - bool flag_with = inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH; - - if (get_ast_input1(inst) != nullptr) - log_error("Currently only simple expression properties are supported as first operand to SVA_UNTIL.\n"); - - SigBit expr = importer->net_map_at(inst->GetInput1()); - - if (flag_with) - { - seq.sig_a = module->LogicAnd(NEW_ID, seq.sig_a, expr); - sva_until_list_inclusive.push_back(expr); - parse_sequence(seq, inst->GetInput2()); - sva_until_list_inclusive.pop_back(); - } - else - { - sva_until_list_exclusive.push_back(expr); - parse_sequence(seq, inst->GetInput2()); - sva_until_list_exclusive.pop_back(); - } - - return; - } - - // Handle unsupported primitives - - if (!importer->mode_keep) - log_error("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name()); - log_warning("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name()); - } - - void import() - { - module = importer->module; - netlist = root->Owner(); - - RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); - - // parse SVA property clock event - - Instance *at_node = get_ast_input(root); - - // asynchronous immediate assertion/assumption/cover - if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT || - root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME)) - { - SigSpec sig_a = importer->net_map_at(root->GetInput()); - RTLIL::Cell *c = nullptr; - - if (eventually) { - if (mode_assert) c = module->addLive(root_name, sig_a, State::S1); - if (mode_assume) c = module->addFair(root_name, sig_a, State::S1); - } else { - if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1); - if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1); - if (mode_cover) c = module->addCover(root_name, sig_a, State::S1); - } - - importer->import_attributes(c->attributes, root); - return; - } - - log_assert(at_node && at_node->Type() == PRIM_SVA_AT); - - VerificClockEdge clock_edge(importer, get_ast_input1(at_node)); - clock = clock_edge.clock_sig; - clock_posedge = clock_edge.posedge; - - // parse disable_iff expression - - Net *sequence_net = at_node->GetInput2(); - - while (1) - { - Instance *sequence_node = net_to_ast_driver(sequence_net); - - if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) { - eventually = true; - sequence_net = sequence_node->GetInput(); - continue; - } - - if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) { - disable_iff = importer->net_map_at(sequence_node->GetInput1()); - sequence_net = sequence_node->GetInput2(); - continue; - } - - break; - } - - // parse SVA sequence into trigger signal - - sequence_t seq; - parse_sequence(seq, sequence_net); - sequence_ff(seq); - - // generate assert/assume/cover cell - - RTLIL::Cell *c = nullptr; - - if (eventually) { - if (mode_assert) c = module->addLive(root_name, seq.sig_a, seq.sig_en); - if (mode_assume) c = module->addFair(root_name, seq.sig_a, seq.sig_en); - } else { - if (mode_assert) c = module->addAssert(root_name, seq.sig_a, seq.sig_en); - if (mode_assume) c = module->addAssume(root_name, seq.sig_a, seq.sig_en); - if (mode_cover) c = module->addCover(root_name, seq.sig_a, seq.sig_en); - } - - importer->import_attributes(c->attributes, root); - } -#endif }; -void svapp_assert(Instance *inst) -{ - VerificSvaImporter worker; - worker.root = inst; - worker.mode_assert = true; - worker.rewrite(); -} - -void svapp_assume(Instance *inst) -{ - VerificSvaImporter worker; - worker.root = inst; - worker.mode_assume = true; - worker.rewrite(); -} - -void svapp_cover(Instance *inst) -{ - VerificSvaImporter worker; - worker.root = inst; - worker.mode_cover = true; - worker.rewrite(); -} - void import_sva_assert(VerificImporter *importer, Instance *inst) { VerificSvaImporter worker; |