Merge branch 'master' into btor-ng

1 files changed, 122 insertions, 69 deletions

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 54210f98a..92c7c9e2d 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -60,6 +60,29 @@ PRIVATE_NAMESPACE_BEGIN
 
 #ifdef YOSYS_ENABLE_VERIFIC
 
+pool<int> verific_sva_prims = {
+	// Copy&paste from Verific 3.16_484_32_170630 Netlist.h
+	PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
+	PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
+	PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
+	PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
+	PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
+	PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
+	PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
+	PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
+	PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
+	PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
+	PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
+	PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
+	PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
+	PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
+	PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
+	PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
+	PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
+	PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
+	PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
+};
+
 string verific_error_msg;
 
 void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
@@ -99,9 +122,9 @@ struct VerificImporter;
 void import_sva_assert(VerificImporter *importer, Instance *inst);
 void import_sva_assume(VerificImporter *importer, Instance *inst);
 void import_sva_cover(VerificImporter *importer, Instance *inst);
-void svapp_assert(VerificImporter *importer, Instance *inst);
-void svapp_assume(VerificImporter *importer, Instance *inst);
-void svapp_cover(VerificImporter *importer, Instance *inst);
+void svapp_assert(Instance *inst);
+void svapp_assume(Instance *inst);
+void svapp_cover(Instance *inst);
 
 struct VerificClockEdge {
 	Net *clock_net = nullptr;
@@ -120,37 +143,10 @@ struct VerificImporter
 
 	bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
 
-	pool<int> verific_sva_prims;
-
 	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) :
 			mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
 			mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose)
 	{
-		// Copy&paste from Verific 3.16_484_32_170630 Netlist.h
-		vector<int> sva_prims {
-			PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
-			PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
-			PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
-			PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
-			PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
-			PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
-			PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
-			PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
-			PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
-			PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
-			PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
-			PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
-			PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
-			PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
-			PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
-			PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
-			PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
-			PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
-			PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
-		};
-
-		for (int p : sva_prims)
-			verific_sva_prims.insert(p);
 	}
 
 	RTLIL::SigBit net_map_at(Net *net)
@@ -717,6 +713,32 @@ struct VerificImporter
 		Instance *inst;
 		PortRef *pr;
 
+		if (!mode_nosvapp)
+		{
+			vector<Instance*> asserts, assumes, covers;
+
+			FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
+			{
+				if (inst->Type() == PRIM_SVA_ASSERT)
+					asserts.push_back(inst);
+
+				if (inst->Type() == PRIM_SVA_ASSUME)
+					assumes.push_back(inst);
+
+				if (inst->Type() == PRIM_SVA_COVER)
+					covers.push_back(inst);
+			}
+
+			for (auto inst : asserts)
+				svapp_assert(inst);
+
+			for (auto inst : assumes)
+				svapp_assume(inst);
+
+			for (auto inst : covers)
+				svapp_cover(inst);
+		}
+
 		FOREACH_PORT_OF_NETLIST(nl, mi, port)
 		{
 			if (port->Bus())
@@ -1118,6 +1140,34 @@ struct VerificImporter
 			if (inst->Type() == PRIM_SVA_COVER)
 				sva_covers.insert(inst);
 
+			if (inst->Type() == OPER_SVA_STABLE && !mode_nosva)
+			{
+				VerificClockEdge clock_edge(this, inst->GetInput2Bit(0)->Driver());
+
+				log_assert(inst->Input1Size() == inst->OutputSize());
+
+				SigSpec sig_d, sig_q, sig_o;
+				sig_q = module->addWire(NEW_ID, inst->Input1Size());
+
+				for (int i = int(inst->Input1Size())-1; i >= 0; i--){
+					sig_d.append(net_map_at(inst->GetInput1Bit(i)));
+					sig_o.append(net_map_at(inst->GetOutputBit(i)));
+				}
+
+				if (verbose) {
+					log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
+							log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
+					log("    XNOR with A=%s, B=%s, Y=%s.\n",
+							log_signal(sig_d), log_signal(sig_q), log_signal(sig_o));
+				}
+
+				module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
+				module->addXnor(NEW_ID, sig_d, sig_q, sig_o);
+
+				if (!mode_keep)
+					continue;
+			}
+
 			if (inst->Type() == PRIM_SVA_PAST && !mode_nosva)
 			{
 				VerificClockEdge clock_edge(this, inst->GetInput2()->Driver());
@@ -1196,18 +1246,6 @@ struct VerificImporter
 			}
 		}
 
-		if (!mode_nosvapp)
-		{
-			for (auto inst : sva_asserts)
-				svapp_assert(this, inst);
-
-			for (auto inst : sva_assumes)
-				svapp_assume(this, inst);
-
-			for (auto inst : sva_covers)
-				svapp_cover(this, inst);
-		}
-
 		if (!mode_nosva)
 		{
 			for (auto inst : sva_asserts)
@@ -1250,15 +1288,13 @@ VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
 
 struct VerificSvaPP
 {
-	VerificImporter *importer;
-	Module *module;
-
 	Netlist *netlist;
 	Instance *root;
 
 	bool mode_assert = false;
 	bool mode_assume = false;
 	bool mode_cover = false;
+	bool did_something = false;
 
 	Instance *net_to_ast_driver(Net *n)
 	{
@@ -1273,10 +1309,11 @@ struct VerificSvaPP
 		if (inst == nullptr)
 			return nullptr;
 
-		if (!importer->verific_sva_prims.count(inst->Type()))
+		if (!verific_sva_prims.count(inst->Type()))
 			return nullptr;
 
-		if (inst->Type() == PRIM_SVA_PAST)
+		if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL ||
+				inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE || inst->Type() == PRIM_SVA_PAST)
 			return nullptr;
 
 		return inst;
@@ -1288,74 +1325,89 @@ 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 *impl_to_seq(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 = impl_to_seq(get_ast_input(inst));
+			Net *new_net = rewrite(get_ast_input(inst));
 			if (new_net) {
 				inst->Disconnect(inst->View()->GetInput());
 				inst->Connect(inst->View()->GetInput(), new_net);
 			}
-			return nullptr;
+			return default_net;
 		}
 
 		if (inst->Type() == PRIM_SVA_AT) {
-			Net *new_net = impl_to_seq(get_ast_input2(inst));
+			Net *new_net = rewrite(get_ast_input2(inst));
 			if (new_net) {
 				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) {
-				Net *new_in1 = impl_to_seq(get_ast_input1(inst));
-				Net *new_in2 = impl_to_seq(get_ast_input2(inst));
-				if (!new_in1) new_in1 = inst->GetInput1();
-				if (!new_in2) new_in2 = inst->GetInput2();
+				did_something = true;
+				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 default_net;
 		}
 
-		return nullptr;
+		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 default_net;
 	}
 
 	void run()
 	{
-		module = importer->module;
 		netlist = root->Owner();
-
-		// impl_to_seq(root);
+		do {
+			did_something = false;
+			rewrite(root);
+		} while (did_something);
 	}
 };
 
-void svapp_assert(VerificImporter *importer, Instance *inst)
+void svapp_assert(Instance *inst)
 {
 	VerificSvaPP worker;
-	worker.importer = importer;
 	worker.root = inst;
 	worker.mode_assert = true;
 	worker.run();
 }
 
-void svapp_assume(VerificImporter *importer, Instance *inst)
+void svapp_assume(Instance *inst)
 {
 	VerificSvaPP worker;
-	worker.importer = importer;
 	worker.root = inst;
 	worker.mode_assume = true;
 	worker.run();
 }
 
-void svapp_cover(VerificImporter *importer, Instance *inst)
+void svapp_cover(Instance *inst)
 {
 	VerificSvaPP worker;
-	worker.importer = importer;
 	worker.root = inst;
 	worker.mode_cover = true;
 	worker.run();
@@ -1394,10 +1446,11 @@ struct VerificSvaImporter
 		if (inst == nullptr)
 			return nullptr;
 
-		if (!importer->verific_sva_prims.count(inst->Type()))
+		if (!verific_sva_prims.count(inst->Type()))
 			return nullptr;
 
-		if (inst->Type() == PRIM_SVA_PAST)
+		if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL ||
+				inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE || inst->Type() == PRIM_SVA_PAST)
 			return nullptr;
 
 		return inst;