Fix handling of SVA "until seq.triggered" properties

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 7f09ccae4005437aebe69df933f4df13c1b64e14..fd464909fe8a4ff6cda94102fb006f39cfe4c656 100644 (file)
--- 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);