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

Add $rose/$fell support to Verific bindings 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-01 10:12:15 +01:00
parent 3df0d04a7b
commit 3c49e3c5b3
1 changed files with 22 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
frontends/verific/verific.cc
View File

@ -1095,7 +1095,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER) if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER)
sva_covers.insert(inst); sva_covers.insert(inst);
if (inst->Type() == OPER_SVA_STABLE && !mode_nosva) if (inst->Type() == OPER_SVA_STABLE)
{ {
VerificClockEdge clock_edge(this, inst->GetInput2Bit(0)->Driver()); VerificClockEdge clock_edge(this, inst->GetInput2Bit(0)->Driver());
@ -1123,7 +1123,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
continue; continue;
} }
if (inst->Type() == PRIM_SVA_STABLE && !mode_nosva) if (inst->Type() == PRIM_SVA_STABLE)
{ {
VerificClockEdge clock_edge(this, inst->GetInput2()->Driver()); VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
@ -1145,7 +1145,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
continue; continue;
} }
if (inst->Type() == PRIM_SVA_PAST && !mode_nosva) if (inst->Type() == PRIM_SVA_PAST)
{ {
VerificClockEdge clock_edge(this, inst->GetInput2()->Driver()); VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
@ -1162,6 +1162,25 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
continue; continue;
} }
if ((inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL))
{
VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
SigBit sig_d = net_map_at(inst->GetInput1());
SigBit sig_o = net_map_at(inst->GetOutput());
SigBit sig_q = module->addWire(NEW_ID);
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));
module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
module->addEq(NEW_ID, {sig_q, sig_d}, Const(inst->Type() == PRIM_SVA_ROSE ? 1 : 2, 2), sig_o);
if (!mode_keep)
continue;
}
if (!mode_keep && verific_sva_prims.count(inst->Type())) { if (!mode_keep && verific_sva_prims.count(inst->Type())) {
if (verific_verbose) if (verific_verbose)
log(" skipping SVA cell in non k-mode\n"); log(" skipping SVA cell in non k-mode\n");