diff options
| -rw-r--r-- | frontends/verific/verificsva.cc | 32 |
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); |