riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Add VerificClocking class and refactor Verific DFF handling 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-04 13:48:53 +01:00
parent ae4e204c76
commit 261cf706f4
3 changed files with 197 additions and 127 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

197
frontends/verific/verific.cc
View File

@ -277,16 +277,18 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
if (inst->Type() == PRIM_DFFRS) if (inst->Type() == PRIM_DFFRS)
{ {
VerificClocking clocking(this, inst->GetClock());
log_assert(clocking.disable_sig == State::S0);
log_assert(clocking.body_net == nullptr);
if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
module->addDffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else if (inst->GetSet()->IsGnd()) else if (inst->GetSet()->IsGnd())
module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()), clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S0);
net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), false);
else if (inst->GetReset()->IsGnd()) else if (inst->GetReset()->IsGnd())
module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), State::S1);
net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), true);
else else
module->addDffsrGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
return true; return true;
} }
@ -358,16 +360,18 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
if (inst->Type() == PRIM_DFFRS) if (inst->Type() == PRIM_DFFRS)
{ {
VerificClocking clocking(this, inst->GetClock());
log_assert(clocking.disable_sig == State::S0);
log_assert(clocking.body_net == nullptr);
if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
module->addDff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); clocking.addDff(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
else if (inst->GetSet()->IsGnd()) else if (inst->GetSet()->IsGnd())
module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()), clocking.addAdff(inst_name, net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0);
else if (inst->GetReset()->IsGnd()) else if (inst->GetReset()->IsGnd())
module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), clocking.addAdff(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1);
else else
module->addDffsr(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), clocking.addDffsr(inst_name, net_map_at(inst->GetSet()), net_map_at(inst->GetReset()),
net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
return true; return true;
} }
@ -594,13 +598,20 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
return true; return true;
} }
if (inst->Type() == OPER_WIDE_DFFRS) { if (inst->Type() == OPER_WIDE_DFFRS)
{
VerificClocking clocking(this, inst->GetClock());
log_assert(clocking.disable_sig == State::S0);
log_assert(clocking.body_net == nullptr);
RTLIL::SigSpec sig_set = operatorInport(inst, "set"); RTLIL::SigSpec sig_set = operatorInport(inst, "set");
RTLIL::SigSpec sig_reset = operatorInport(inst, "reset"); RTLIL::SigSpec sig_reset = operatorInport(inst, "reset");
if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool()) if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool())
module->addDff(inst_name, net_map_at(inst->GetClock()), IN, OUT); clocking.addDff(inst_name, IN, OUT);
else else
module->addDffsr(inst_name, net_map_at(inst->GetClock()), sig_set, sig_reset, IN, OUT); clocking.addDffsr(inst_name, sig_set, sig_reset, IN, OUT);
return true; return true;
} }
@ -1097,7 +1108,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (inst->Type() == OPER_SVA_STABLE) if (inst->Type() == OPER_SVA_STABLE)
{ {
VerificClockEdge clock_edge(this, inst->GetInput2Bit(0)->Driver()); VerificClocking clocking(this, inst->GetInput2Bit(0));
log_assert(inst->Input1Size() == inst->OutputSize()); log_assert(inst->Input1Size() == inst->OutputSize());
@ -1110,13 +1121,13 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
} }
if (verific_verbose) { if (verific_verbose) {
log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
log(" XNOR with A=%s, B=%s, Y=%s.\n", log(" XNOR with A=%s, B=%s, Y=%s.\n",
log_signal(sig_d), log_signal(sig_q), log_signal(sig_o)); log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
} }
module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge); clocking.addDff(NEW_ID, sig_d, sig_q);
module->addXnor(NEW_ID, sig_d, sig_q, sig_o); module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
if (!mode_keep) if (!mode_keep)
@ -1125,20 +1136,20 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (inst->Type() == PRIM_SVA_STABLE) if (inst->Type() == PRIM_SVA_STABLE)
{ {
VerificClockEdge clock_edge(this, inst->GetInput2()->Driver()); VerificClocking clocking(this, inst->GetInput2());
SigSpec sig_d = net_map_at(inst->GetInput1()); SigSpec sig_d = net_map_at(inst->GetInput1());
SigSpec sig_o = net_map_at(inst->GetOutput()); SigSpec sig_o = net_map_at(inst->GetOutput());
SigSpec sig_q = module->addWire(NEW_ID); SigSpec sig_q = module->addWire(NEW_ID);
if (verific_verbose) { if (verific_verbose) {
log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
log(" XNOR with A=%s, B=%s, Y=%s.\n", log(" XNOR with A=%s, B=%s, Y=%s.\n",
log_signal(sig_d), log_signal(sig_q), log_signal(sig_o)); log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
} }
module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge); clocking.addDff(NEW_ID, sig_d, sig_q);
module->addXnor(NEW_ID, sig_d, sig_q, sig_o); module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
if (!mode_keep) if (!mode_keep)
@ -1147,16 +1158,16 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (inst->Type() == PRIM_SVA_PAST) if (inst->Type() == PRIM_SVA_PAST)
{ {
VerificClockEdge clock_edge(this, inst->GetInput2()->Driver()); VerificClocking clocking(this, inst->GetInput2());
SigBit sig_d = net_map_at(inst->GetInput1()); SigBit sig_d = net_map_at(inst->GetInput1());
SigBit sig_q = net_map_at(inst->GetOutput()); SigBit sig_q = net_map_at(inst->GetOutput());
if (verific_verbose) if (verific_verbose)
log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
past_ffs.insert(module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge)); past_ffs.insert(clocking.addDff(NEW_ID, sig_d, sig_q));
if (!mode_keep) if (!mode_keep)
continue; continue;
@ -1164,17 +1175,17 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL)) if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL))
{ {
VerificClockEdge clock_edge(this, inst->GetInput2()->Driver()); VerificClocking clocking(this, inst->GetInput2());
SigBit sig_d = net_map_at(inst->GetInput1()); SigBit sig_d = net_map_at(inst->GetInput1());
SigBit sig_o = net_map_at(inst->GetOutput()); SigBit sig_o = net_map_at(inst->GetOutput());
SigBit sig_q = module->addWire(NEW_ID); SigBit sig_q = module->addWire(NEW_ID);
if (verific_verbose) if (verific_verbose)
log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg", log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clocking.posedge ? "pos" : "neg",
log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig)); log_signal(sig_d), log_signal(sig_q), log_signal(clocking.clock_sig));
module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge); clocking.addDff(NEW_ID, sig_d, sig_q);
module->addEq(NEW_ID, {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o); module->addEq(NEW_ID, {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
if (!mode_keep) if (!mode_keep)
@ -1259,26 +1270,130 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
// ================================================================== // ==================================================================
VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst) VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
{ {
module = importer->module;
log_assert(importer != nullptr); log_assert(importer != nullptr);
log_assert(inst != nullptr); log_assert(net != nullptr);
// SVA posedge/negedge Instance *inst = net->Driver();
if (inst->Type() == PRIM_SVA_POSEDGE)
if (inst != nullptr && inst->Type() == PRIM_SVA_AT)
{ {
clock_net = inst->GetInput(); net = inst->GetInput1();
posedge = true; body_net = inst->GetInput2();
Instance *driver = clock_net->Driver(); inst = net->Driver();
if (!clock_net->IsMultipleDriven() && driver && driver->Type() == PRIM_INV) {
clock_net = driver->GetInput(); Instance *body_inst = body_net->Driver();
if (body_inst != nullptr && body_inst->Type() == PRIM_SVA_DISABLE_IFF) {
disable_net = body_inst->GetInput1();
disable_sig = importer->net_map_at(disable_net);
body_net = body_inst->GetInput2();
}
}
if (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
{
net = inst->GetInput();
inst = net->Driver();;
}
if (inst != nullptr && inst->Type() == PRIM_INV)
{
net = inst->GetInput();
inst = net->Driver();;
posedge = false; posedge = false;
} }
// Detect clock-enable circuit
do {
if (inst == nullptr || inst->Type() != PRIM_AND)
break;
Net *net_dlatch = inst->GetInput1();
Instance *inst_dlatch = net_dlatch->Driver();
if (inst_dlatch == nullptr || inst_dlatch->Type() != PRIM_DLATCHRS)
break;
if (!inst_dlatch->GetSet()->IsGnd() || !inst_dlatch->GetReset()->IsGnd())
break;
Net *net_enable = inst_dlatch->GetInput();
Net *net_not_clock = inst_dlatch->GetControl();
if (net_enable == nullptr || net_not_clock == nullptr)
break;
Instance *inst_not_clock = net_not_clock->Driver();
if (inst_not_clock == nullptr || inst_not_clock->Type() != PRIM_INV)
break;
Net *net_clock1 = inst_not_clock->GetInput();
Net *net_clock2 = inst->GetInput2();
if (net_clock1 == nullptr || net_clock1 != net_clock2)
break;
enable_net = net_enable;
enable_sig = importer->net_map_at(enable_net);
net = net_clock1;
inst = net->Driver();;
} while (0);
clock_net = net;
clock_sig = importer->net_map_at(clock_net); clock_sig = importer->net_map_at(clock_net);
return; }
Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value)
{
log_assert(GetSize(sig_d) == GetSize(sig_q));
if (GetSize(init_value) != 0) {
log_assert(GetSize(sig_q) == GetSize(init_value));
if (sig_q.is_wire()) {
sig_q.as_wire()->attributes["\\init"] = init_value;
} else {
Wire *w = module->addWire(NEW_ID, GetSize(sig_q));
w->attributes["\\init"] = init_value;
module->connect(sig_q, w);
sig_q = w;
} }
}
if (enable_sig != State::S1)
sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
if (disable_sig != State::S0) {
log_assert(GetSize(sig_q) == GetSize(init_value));
return module->addAdff(name, clock_sig, disable_sig, sig_d, sig_q, init_value, posedge);
}
return module->addDff(name, clock_sig, sig_d, sig_q, posedge);
}
Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value)
{
log_assert(disable_sig == State::S0);
if (enable_sig != State::S1)
sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
return module->addAdff(name, clock_sig, sig_arst, sig_d, sig_q, arst_value, posedge);
}
Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q)
{
log_assert(disable_sig == State::S0);
if (enable_sig != State::S1)
sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
return module->addDffsr(name, clock_sig, sig_set, sig_clr, sig_d, sig_q, posedge);
} }
// ================================================================== // ==================================================================

17
frontends/verific/verific.h
View File

@ -29,11 +29,22 @@ extern pool<int> verific_sva_prims;
struct VerificImporter; struct VerificImporter;
struct VerificClockEdge { struct VerificClocking {
RTLIL::Module *module = nullptr;
Verific::Net *clock_net = nullptr; Verific::Net *clock_net = nullptr;
Verific::Net *enable_net = nullptr;
Verific::Net *disable_net = nullptr;
Verific::Net *body_net = nullptr;
SigBit clock_sig = State::Sx; SigBit clock_sig = State::Sx;
bool posedge = false; SigBit enable_sig = State::S1;
VerificClockEdge(VerificImporter *importer, Verific::Instance *inst); SigBit disable_sig = State::S0;
bool posedge = true;
VerificClocking() { }
VerificClocking(VerificImporter *importer, Verific::Net *net);
RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const());
RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value);
RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q);
}; };
struct VerificImporter struct VerificImporter

104
frontends/verific/verificsva.cc
View File

@ -37,7 +37,9 @@
// Notes: // Notes:
// |-> is a placeholder for |-> and |=> // |-> is a placeholder for |-> and |=>
// "until" is a placeholder for all until operators // "until" is a placeholder for all until operators
// ##[N:M], [*N:M], [=N:M], [->N:M] includes ##N, [*N], [=N], [->N] // ##[N:M] includes ##N, ##[*], ##[+]
// [*N:M] includes [*N], [*], [+]
// [=N:M], [->N:M] includes [=N], [->N]
// //
// ------------------------------------------------------- // -------------------------------------------------------
// //
@ -117,8 +119,7 @@ struct SvaDFsmNode
struct SvaFsm struct SvaFsm
{ {
Module *module; Module *module;
SigBit clock; VerificClocking clocking;
bool clockpol;
SigBit trigger_sig = State::S1, disable_sig; SigBit trigger_sig = State::S1, disable_sig;
SigBit throughout_sig = State::S1; SigBit throughout_sig = State::S1;
@ -133,12 +134,10 @@ struct SvaFsm
SigBit final_accept_sig = State::Sx; SigBit final_accept_sig = State::Sx;
SigBit final_reject_sig = State::Sx; SigBit final_reject_sig = State::Sx;
SvaFsm(Module *mod, SigBit clk, bool clkpol, SigBit dis = State::S0, SigBit trig = State::S1) SvaFsm(const VerificClocking &clking, SigBit trig = State::S1)
{ {
module = mod; module = clking.module;
clock = clk; clocking = clking;
clockpol = clkpol;
disable_sig = dis;
trigger_sig = trig; trigger_sig = trig;
startNode = createNode(); startNode = createNode();
@ -326,8 +325,7 @@ struct SvaFsm
for (int i = 0; i < GetSize(nodes); i++) for (int i = 0; i < GetSize(nodes); i++)
{ {
if (next_state_sig[i] != State::S0) { if (next_state_sig[i] != State::S0) {
state_wire[i]->attributes["\\init"] = Const(0, 1); clocking.addDff(NEW_ID, next_state_sig[i], state_wire[i], Const(0, 1));
module->addDff(NEW_ID, clock, next_state_sig[i], state_wire[i], clockpol);
} else { } else {
module->connect(state_wire[i], State::S0); module->connect(state_wire[i], State::S0);
} }
@ -501,7 +499,6 @@ struct SvaFsm
{ {
SvaDFsmNode &dnode = it.second; SvaDFsmNode &dnode = it.second;
dnode.ffoutwire = module->addWire(NEW_ID); dnode.ffoutwire = module->addWire(NEW_ID);
dnode.ffoutwire->attributes["\\init"] = Const(0, 1);
dnode.statesig = dnode.ffoutwire; dnode.statesig = dnode.ffoutwire;
if (it.first == vector<int>{startNode}) if (it.first == vector<int>{startNode})
@ -533,10 +530,10 @@ struct SvaFsm
module->connect(dnode.ffoutwire, State::S0); module->connect(dnode.ffoutwire, State::S0);
} else } else
if (GetSize(dnode.nextstate) == 1) { if (GetSize(dnode.nextstate) == 1) {
module->addDff(NEW_ID, clock, dnode.nextstate, dnode.ffoutwire, clockpol); clocking.addDff(NEW_ID, dnode.nextstate, dnode.ffoutwire, State::S0);
} else { } else {
SigSpec nextstate = module->ReduceOr(NEW_ID, dnode.nextstate); SigSpec nextstate = module->ReduceOr(NEW_ID, dnode.nextstate);
module->addDff(NEW_ID, clock, nextstate, dnode.ffoutwire, clockpol); clocking.addDff(NEW_ID, nextstate, dnode.ffoutwire, State::S0);
} }
} }
@ -717,16 +714,12 @@ struct VerificSvaImporter
Netlist *netlist = nullptr; Netlist *netlist = nullptr;
Instance *root = nullptr; Instance *root = nullptr;
SigBit clock = State::Sx; VerificClocking clocking;
bool clockpol = false;
SigBit disable_iff = State::S0;
bool mode_assert = false; bool mode_assert = false;
bool mode_assume = false; bool mode_assume = false;
bool mode_cover = false; bool mode_cover = false;
bool eventually = false; bool eventually = false;
bool did_something = false;
Instance *net_to_ast_driver(Net *n) Instance *net_to_ast_driver(Net *n)
{ {
@ -887,62 +880,16 @@ struct VerificSvaImporter
RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
// parse SVA property clock event clocking = VerificClocking(importer, root->GetInput());
Instance *at_node = get_ast_input(root); if (clocking.body_net == nullptr)
log_error("Failed to parse SVA clocking at %s (%s) at %s:%d.", root->Name(), root->View()->Owner()->Name(),
// asynchronous immediate assertion/assumption/cover LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()));
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;
clockpol = clock_edge.posedge;
// parse disable_iff expression
Net *net = at_node->GetInput2();
while (1)
{
Instance *sequence_node = net_to_ast_driver(net);
if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
eventually = true;
net = sequence_node->GetInput();
continue;
}
if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
disable_iff = importer->net_map_at(sequence_node->GetInput1());
net = sequence_node->GetInput2();
continue;
}
break;
}
// parse SVA sequence into trigger signal // parse SVA sequence into trigger signal
SigBit prop_okay; SigBit prop_okay;
Net *net = clocking.body_net;
Instance *inst = net_to_ast_driver(net); Instance *inst = net_to_ast_driver(net);
if (inst == nullptr) if (inst == nullptr)
@ -957,7 +904,7 @@ struct VerificSvaImporter
Net *consequent_net = inst->GetInput2(); Net *consequent_net = inst->GetInput2();
int node; int node;
SvaFsm antecedent_fsm(module, clock, clockpol, disable_iff); SvaFsm antecedent_fsm(clocking);
node = parse_sequence(&antecedent_fsm, antecedent_fsm.startNode, antecedent_net); node = parse_sequence(&antecedent_fsm, antecedent_fsm.startNode, antecedent_net);
if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
int next_node = antecedent_fsm.createNode(); int next_node = antecedent_fsm.createNode();
@ -996,7 +943,7 @@ struct VerificSvaImporter
until_net = until_inst->GetInput(); until_net = until_inst->GetInput();
} }
SvaFsm until_fsm(module, clock, clockpol, disable_iff); SvaFsm until_fsm(clocking);
node = parse_sequence(&until_fsm, until_fsm.startNode, until_net); node = parse_sequence(&until_fsm, until_fsm.startNode, until_net);
until_fsm.createLink(node, until_fsm.acceptNode); until_fsm.createLink(node, until_fsm.acceptNode);
@ -1008,13 +955,11 @@ struct VerificSvaImporter
until_fsm.dump(); until_fsm.dump();
} }
Wire *antecedent_match_q = module->addWire(NEW_ID); SigBit 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->Or(NEW_ID, antecedent_match, antecedent_match_q);
SigBit antecedent_match_filtered = module->And(NEW_ID, antecedent_match, not_until_match); SigBit antecedent_match_filtered = module->And(NEW_ID, antecedent_match, not_until_match);
module->addDff(NEW_ID, clock, antecedent_match_filtered, antecedent_match_q, clockpol); clocking.addDff(NEW_ID, antecedent_match_filtered, antecedent_match_q, State::S0);
if (!until_with) if (!until_with)
antecedent_match = antecedent_match_filtered; antecedent_match = antecedent_match_filtered;
@ -1027,7 +972,7 @@ struct VerificSvaImporter
consequent_inst = net_to_ast_driver(consequent_net); consequent_inst = net_to_ast_driver(consequent_net);
} }
SvaFsm consequent_fsm(module, clock, clockpol, disable_iff, antecedent_match); SvaFsm consequent_fsm(clocking, antecedent_match);
node = parse_sequence(&consequent_fsm, consequent_fsm.startNode, consequent_net); node = parse_sequence(&consequent_fsm, consequent_fsm.startNode, consequent_net);
consequent_fsm.createLink(node, consequent_fsm.acceptNode); consequent_fsm.createLink(node, consequent_fsm.acceptNode);
@ -1046,7 +991,7 @@ struct VerificSvaImporter
else else
if (inst->Type() == PRIM_SVA_NOT || mode_cover) if (inst->Type() == PRIM_SVA_NOT || mode_cover)
{ {
SvaFsm fsm(module, clock, clockpol, disable_iff); SvaFsm fsm(clocking);
int node = parse_sequence(&fsm, fsm.startNode, mode_cover ? net : inst->GetInput()); int node = parse_sequence(&fsm, fsm.startNode, mode_cover ? net : inst->GetInput());
fsm.createLink(node, fsm.acceptNode); fsm.createLink(node, fsm.acceptNode);
SigBit accept = fsm.getAccept(); SigBit accept = fsm.getAccept();
@ -1069,9 +1014,8 @@ struct VerificSvaImporter
// add final FF stage // add final FF stage
Wire *prop_okay_q = module->addWire(NEW_ID); SigBit prop_okay_q = module->addWire(NEW_ID);
prop_okay_q->attributes["\\init"] = Const(mode_cover ? 0 : 1, 1); clocking.addDff(NEW_ID, prop_okay, prop_okay_q, Const(mode_cover ? 0 : 1, 1));
module->addDff(NEW_ID, clock, prop_okay, prop_okay_q, clockpol);
// generate assert/assume/cover cell // generate assert/assume/cover cell