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
+ // Create state FFs
- if (accept_sig != State::Sz) {
- module->connect(accept_sig, state_sig[acceptNode]);
- }
-
- 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);
+ log(" non-deterministic encoding:\n");
+ for (int i = 0; i < GetSize(nodes); i++)
+ {
+ log(" node %d:\n", i);
- if (i == startNode)
- log(" startNode\n");
+ if (i == startNode)
+ log(" startNode\n");
- if (i == rejectNode)
- log(" rejectNode\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;
@@ -453,124 +453,6 @@ struct VerificSvaImporter
Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
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
@@ -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 (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(" 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 (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;