aboutsummaryrefslogtreecommitdiffstats
path: root/frontends
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2018-02-28 15:32:17 +0100
committerClifford Wolf <clifford@clifford.at>2018-02-28 15:32:17 +0100
commit5ac3ee858a35bf4dd20c02a3cfcd9c0e23db9ecc (patch)
treeb745bb0a4129a512fc8dc1460bf79c8674a88482 /frontends
parent8a1d6ccf0c1b0c7e84cd160dd2572eabebcd67cc (diff)
downloadyosys-5ac3ee858a35bf4dd20c02a3cfcd9c0e23db9ecc.tar.gz
yosys-5ac3ee858a35bf4dd20c02a3cfcd9c0e23db9ecc.tar.bz2
yosys-5ac3ee858a35bf4dd20c02a3cfcd9c0e23db9ecc.zip
Add support for PRIM_SVA_UNTIL to new SVA importer
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends')
-rw-r--r--frontends/verific/verificsva.cc27
1 files changed, 27 insertions, 0 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 14b989493..2185e4596 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -922,6 +922,33 @@ struct VerificSvaImporter
consequent_net = consequent_inst->GetInput();
}
+ if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL ||
+ consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH))
+ {
+ bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH;
+ consequent_net = consequent_inst->GetInput1();
+ Net *until_net = consequent_inst->GetInput2();
+
+ SvaFsm until_fsm(module, clock, clockpol, disable_iff);
+ node = parse_sequence(&until_fsm, until_fsm.startNode, until_net);
+ if (until_with) {
+ int next_node = until_fsm.createNode();
+ until_fsm.createEdge(node, next_node);
+ node = next_node;
+ }
+ until_fsm.createLink(node, until_fsm.acceptNode);
+
+ SigBit until_match = until_fsm.getAccept();
+ SigBit not_until_match = module->Not(NEW_ID, until_match);
+
+ Wire *extend_antecedent_match_q = module->addWire(NEW_ID);
+ extend_antecedent_match_q->attributes["\\init"] = Const(0, 1);
+ antecedent_match = module->Or(NEW_ID, antecedent_match, extend_antecedent_match_q);
+
+ SigBit extend_antecedent_match = module->And(NEW_ID, not_until_match, antecedent_match);
+ module->addDff(NEW_ID, clock, extend_antecedent_match, extend_antecedent_match_q, clockpol);
+ }
+
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);