From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 29 Jun 2018 17:24:58 +0000 (+0200)
Subject: Fix verific eventually handling
X-Git-Tag: yosys-0.8~59
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8b92ddb9d2635c30636b17ff3d24bc09a44b8551;p=yosys.git

Fix verific eventually handling

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

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 9312fd6e6..8e985c3a6 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -1488,13 +1488,16 @@ struct VerificSvaImporter
 
 	bool eventually_property(Net *&net, SigBit &trig)
 	{
+		Instance *inst = net_to_ast_driver(net);
+
+		if (inst == nullptr)
+			return false;
+
 		if (clocking.cond_net != nullptr)
 			trig = importer->net_map_at(clocking.cond_net);
 		else
 			trig = State::S1;
 
-		Instance *inst = net_to_ast_driver(net);
-
 		if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
 		{
 			if (mode_cover || mode_trigger)
@@ -1523,7 +1526,6 @@ struct VerificSvaImporter
 
 			int node;
 
-			log_dump(trig);
 			SvaFsm antecedent_fsm(clocking, trig);
 			node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
 			if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
@@ -1540,7 +1542,6 @@ struct VerificSvaImporter
 			if (verific_verbose) {
 				log("    Eventually Antecedent FSM:\n");
 				antecedent_fsm.dump();
-				log_dump(trig);
 			}
 
 			return true;
@@ -1690,8 +1691,6 @@ struct VerificSvaImporter
 					SigBit sig_a, sig_en = trig;
 					parse_property(net, &sig_a, nullptr);
 
-					log_dump(trig, sig_a, sig_en);
-
 					// add final FF stage
 
 					SigBit sig_a_q, sig_en_q;