aboutsummaryrefslogtreecommitdiffstats
path: root/frontends
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2018-03-01 10:12:15 +0100
committerClifford Wolf <clifford@clifford.at>2018-03-01 10:12:15 +0100
commit3c49e3c5b3be3cefd406ad6a541e2d5c6d116c5b (patch)
tree3db34af769eac85bd722a21e17457ea0e528c653 /frontends
parent3df0d04a7b7ac01e94d3e2fcf376b8ab4f7de90e (diff)
downloadyosys-3c49e3c5b3be3cefd406ad6a541e2d5c6d116c5b.tar.gz
yosys-3c49e3c5b3be3cefd406ad6a541e2d5c6d116c5b.tar.bz2
yosys-3c49e3c5b3be3cefd406ad6a541e2d5c6d116c5b.zip
Add $rose/$fell support to Verific bindings
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends')
-rw-r--r--frontends/verific/verific.cc25
1 files changed, 22 insertions, 3 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index fc0f72be8..415035ff1 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -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)
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());
@@ -1123,7 +1123,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
continue;
}
- if (inst->Type() == PRIM_SVA_STABLE && !mode_nosva)
+ if (inst->Type() == PRIM_SVA_STABLE)
{
VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
@@ -1145,7 +1145,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
continue;
}
- if (inst->Type() == PRIM_SVA_PAST && !mode_nosva)
+ if (inst->Type() == PRIM_SVA_PAST)
{
VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
@@ -1162,6 +1162,25 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
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 (verific_verbose)
log(" skipping SVA cell in non k-mode\n");