From 315d5e32bfb63a2b4be2dc5e729125c420b164a4 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 26 Mar 2018 13:04:10 +0200
Subject: [PATCH] Fix handling of unclocked immediate assertions in Verific
 front-end

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc    |  7 ++++-
 frontends/verific/verific.h     |  2 +-
 frontends/verific/verificsva.cc | 50 +++++++++++++++++++++++----------
 3 files changed, 42 insertions(+), 17 deletions(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 9f61d69a4..793e296f4 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1297,7 +1297,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 // ==================================================================
 
-VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
+VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_at_only)
 {
 	module = importer->module;
 
@@ -1320,6 +1320,11 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net)
 			body_net = body_inst->GetInput2();
 		}
 	}
+	else
+	{
+		if (sva_at_only)
+			return;
+	}
 
 	if (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
 	{
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 877d79057..9e3e39695 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -42,7 +42,7 @@ struct VerificClocking {
 	bool posedge = true;
 
 	VerificClocking() { }
-	VerificClocking(VerificImporter *importer, Verific::Net *net);
+	VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);
 	RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const());
 	RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value);
 	RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q);
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index c9c341516..1a1000b19 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -1543,20 +1543,33 @@ struct VerificSvaImporter
 
 			RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
 
-			clocking = VerificClocking(importer, root->GetInput());
-
-			if (clocking.body_net == nullptr)
-				parser_error(stringf("Failed to parse SVA clocking"), root);
-
 			// parse SVA sequence into trigger signal
 
-			Net *net = clocking.body_net;
-			SigBit accept_bit = State::S0, reject_bit =  State::S0;
+			clocking = VerificClocking(importer, root->GetInput(), true);
+			SigBit accept_bit = State::S0, reject_bit = State::S0;
 
-			if (mode_assert || mode_assume) {
-				parse_property(net, nullptr, &reject_bit);
-			} else {
-				parse_property(net, &accept_bit, nullptr);
+			if (clocking.body_net == nullptr)
+			{
+				if (clocking.clock_net != nullptr || clocking.enable_net != nullptr || clocking.disable_net != nullptr ||  clocking.cond_net != nullptr)
+					parser_error(stringf("Failed to parse SVA clocking"), root);
+
+				if (mode_assert || mode_assume) {
+					log_ping();
+					reject_bit = module->Not(NEW_ID, parse_expression(root->GetInput()));
+				} else {
+					log_ping();
+					accept_bit = parse_expression(root->GetInput());
+				}
+			}
+			else
+			{
+				if (mode_assert || mode_assume) {
+					log_ping();
+					parse_property(clocking.body_net, nullptr, &reject_bit);
+				} else {
+					log_ping();
+					parse_property(clocking.body_net, &accept_bit, nullptr);
+				}
 			}
 
 			if (mode_trigger)
@@ -1570,10 +1583,17 @@ struct VerificSvaImporter
 
 				// add final FF stage
 
-				SigBit sig_a_q = module->addWire(NEW_ID);
-				SigBit sig_en_q = module->addWire(NEW_ID);
-				clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
-				clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
+				SigBit sig_a_q, sig_en_q;
+
+				if (clocking.body_net == nullptr) {
+					sig_a_q = sig_a;
+					sig_en_q = sig_en;
+				} else {
+					sig_a_q = module->addWire(NEW_ID);
+					sig_en_q = module->addWire(NEW_ID);
+					clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
+					clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
+				}
 
 				// generate assert/assume/cover cell
 
-- 
2.30.2