From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 1 Mar 2018 18:37:36 +0000 (+0100)
Subject: Fix in Verific SVA importer handling of until_with
X-Git-Tag: yosys-0.8~194
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4e5f1f59d66b96c5e0592e4f9810cca5d55c6894;p=yosys.git

Fix in Verific SVA importer handling of until_with

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

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index e6430e9c5..70c28e387 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -974,11 +974,6 @@ struct VerificSvaImporter
 
 				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();
@@ -993,9 +988,12 @@ struct VerificSvaImporter
 				antecedent_match_q->attributes["\\init"] = Const(0, 1);
 
 				antecedent_match = module->Or(NEW_ID, antecedent_match, antecedent_match_q);
-				antecedent_match = module->And(NEW_ID, antecedent_match, not_until_match);
+				SigBit antecedent_match_filtered = module->And(NEW_ID, antecedent_match, not_until_match);
+
+				module->addDff(NEW_ID, clock, antecedent_match_filtered, antecedent_match_q, clockpol);
 
-				module->addDff(NEW_ID, clock, antecedent_match, antecedent_match_q, clockpol);
+				if (!until_with)
+					antecedent_match = antecedent_match_filtered;
 			}
 
 			SvaFsm consequent_fsm(module, clock, clockpol, disable_iff, antecedent_match);