aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--frontends/verific/verificsva.cc32
1 files changed, 25 insertions, 7 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 7f09ccae4..fd464909f 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -56,7 +56,10 @@
// not seq
// seq |=> seq
// seq |=> not seq
+// seq |=> seq until expr
// seq |=> seq until seq.triggered
+// seq |=> not seq until expr
+// seq |=> not seq until seq.triggered
//
// Currently supported sequence operators:
// ##[N:M]
@@ -959,20 +962,28 @@ struct VerificSvaImporter
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();
- }
-
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();
+ Instance *until_inst = net_to_ast_driver(until_net);
+
+ consequent_net = consequent_inst->GetInput1();
+ consequent_inst = net_to_ast_driver(consequent_net);
+
+ if (until_inst != nullptr) {
+ if (until_inst->Type() != PRIM_SVA_TRIGGERED) {
+ if (!importer->mode_keep)
+ log_error("Currently only boolean expressions or sequence.triggered is alowed in SVA_UNTIL condition.\n");
+ log_warning("Currently only boolean expressions or sequence.triggered is alowed in SVA_UNTIL condition.\n");
+ return;
+ }
+ until_net = until_inst->GetInput();
+ }
SvaFsm until_fsm(module, clock, clockpol, disable_iff);
node = parse_sequence(&until_fsm, until_fsm.startNode, until_net);
@@ -998,6 +1009,13 @@ struct VerificSvaImporter
antecedent_match = antecedent_match_filtered;
}
+ bool consequent_not = false;
+ if (consequent_inst && consequent_inst->Type() == PRIM_SVA_NOT) {
+ consequent_not = true;
+ consequent_net = consequent_inst->GetInput();
+ consequent_inst = net_to_ast_driver(consequent_net);
+ }
+
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);