From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 10 Dec 2017 00:10:03 +0000 (+0100)
Subject: Add support for Verific PRIM_SVA_NOT properties
X-Git-Tag: yosys-0.8~257
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ba90e08398e3068a525c3704a069182a365474e8;p=yosys.git

Add support for Verific PRIM_SVA_NOT properties
---

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 04133e5fb..92c7c9e2d 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1325,10 +1325,16 @@ struct VerificSvaPP
 	Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
 	Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
 
-	Net *rewrite(Instance *inst)
+	Net *rewrite_input(Instance *inst) { return rewrite(get_ast_input(inst), inst->GetInput()); }
+	Net *rewrite_input1(Instance *inst) { return rewrite(get_ast_input1(inst), inst->GetInput1()); }
+	Net *rewrite_input2(Instance *inst) { return rewrite(get_ast_input2(inst), inst->GetInput2()); }
+	Net *rewrite_input3(Instance *inst) { return rewrite(get_ast_input3(inst), inst->GetInput3()); }
+	Net *rewrite_control(Instance *inst) { return rewrite(get_ast_control(inst), inst->GetControl()); }
+
+	Net *rewrite(Instance *inst, Net *default_net = nullptr)
 	{
 		if (inst == nullptr)
-			return nullptr;
+			return default_net;
 
 		if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME) {
 			Net *new_net = rewrite(get_ast_input(inst));
@@ -1336,7 +1342,7 @@ struct VerificSvaPP
 				inst->Disconnect(inst->View()->GetInput());
 				inst->Connect(inst->View()->GetInput(), new_net);
 			}
-			return nullptr;
+			return default_net;
 		}
 
 		if (inst->Type() == PRIM_SVA_AT) {
@@ -1345,23 +1351,32 @@ struct VerificSvaPP
 				inst->Disconnect(inst->View()->GetInput2());
 				inst->Connect(inst->View()->GetInput2(), new_net);
 			}
-			return nullptr;
+			return default_net;
 		}
 
 		if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
 		{
 			if (mode_cover) {
 				did_something = true;
-				Net *new_in1 = rewrite(get_ast_input1(inst));
-				Net *new_in2 = rewrite(get_ast_input2(inst));
-				if (!new_in1) new_in1 = inst->GetInput1();
-				if (!new_in2) new_in1 = inst->GetInput2();
+				Net *new_in1 = rewrite_input1(inst);
+				Net *new_in2 = rewrite_input2(inst);
 				return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile());
 			}
-			return nullptr;
+			return default_net;
+		}
+
+		if (inst->Type() == PRIM_SVA_NOT)
+		{
+			if (mode_assert || mode_assume) {
+				did_something = true;
+				Net *new_in = rewrite_input(inst);
+				Net *net_zero = netlist->Gnd(inst->Linefile());
+				return netlist->SvaBinary(PRIM_SVA_OVERLAPPED_IMPLICATION, new_in, net_zero, inst->Linefile());
+			}
+			return default_net;
 		}
 
-		return nullptr;
+		return default_net;
 	}
 
 	void run()