From 0404cf61d5f230de70bc6e6e6bf907bf7b112e0d Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 29 Jun 2018 19:21:04 +0200
Subject: [PATCH] Add verific support for eventually properties

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verificsva.cc | 110 ++++++++++++++++++++++++++++++--
 1 file changed, 105 insertions(+), 5 deletions(-)

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 4e440b4ca..9312fd6e6 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -980,7 +980,6 @@ struct VerificSvaImporter
 	bool mode_assume = false;
 	bool mode_cover = false;
 	bool mode_trigger = false;
-	bool eventually = false;
 
 	Instance *net_to_ast_driver(Net *n)
 	{
@@ -1487,6 +1486,69 @@ struct VerificSvaImporter
 			fsm.getFirstAcceptReject(accept_p, reject_p);
 	}
 
+	bool eventually_property(Net *&net, SigBit &trig)
+	{
+		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)
+				parser_error(inst);
+
+			net = inst->GetInput();
+			clocking.cond_net = nullptr;
+
+			return true;
+		}
+
+		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
+				inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+		{
+			Net *antecedent_net = inst->GetInput1();
+			Net *consequent_net = inst->GetInput2();
+
+			Instance *consequent_inst = net_to_ast_driver(consequent_net);
+
+			if (consequent_inst->Type() != PRIM_SVA_S_EVENTUALLY && consequent_inst->Type() != PRIM_SVA_EVENTUALLY) {
+				return false;
+			}
+
+			if (mode_cover || mode_trigger)
+				parser_error(consequent_inst);
+
+			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) {
+				int next_node = antecedent_fsm.createNode();
+				antecedent_fsm.createEdge(node, next_node);
+				node = next_node;
+			}
+			antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
+
+			trig = antecedent_fsm.getAccept();
+			net = consequent_inst->GetInput();
+			clocking.cond_net = nullptr;
+
+			if (verific_verbose) {
+				log("    Eventually Antecedent FSM:\n");
+				antecedent_fsm.dump();
+				log_dump(trig);
+			}
+
+			return true;
+		}
+
+		return false;
+	}
+
 	void parse_property(Net *net, SigBit *accept_p, SigBit *reject_p)
 	{
 		Instance *inst = net_to_ast_driver(net);
@@ -1620,10 +1682,48 @@ struct VerificSvaImporter
 			}
 			else
 			{
-				if (mode_assert || mode_assume) {
-					parse_property(clocking.body_net, nullptr, &reject_bit);
-				} else {
-					parse_property(clocking.body_net, &accept_bit, nullptr);
+				Net *net = clocking.body_net;
+				SigBit trig;
+
+				if (eventually_property(net, trig))
+				{
+					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;
+
+					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 fair/live cell
+
+					RTLIL::Cell *c = nullptr;
+
+					if (mode_assert) c = module->addLive(root_name, sig_a_q, sig_en_q);
+					if (mode_assume) c = module->addFair(root_name, sig_a_q, sig_en_q);
+
+					importer->import_attributes(c->attributes, root);
+
+					return;
+				}
+				else
+				{
+					if (mode_assert || mode_assume) {
+						parse_property(net, nullptr, &reject_bit);
+					} else {
+						parse_property(net, &accept_bit, nullptr);
+					}
 				}
 			}
 
-- 
2.30.2