commit 6af0d03faede4a8d87292a76ae70dd1362dfcbb3
author Clifford Wolf <clifford@clifford.at> Fri Nov 22 15:52:21 2019 +0100
committer Clifford Wolf <clifford@clifford.at> Fri Nov 22 15:52:21 2019 +0100
tree 32f8e72013cf4e6be4e1fb728f7670ebde320d1e
parent 72d2ef6fd071a8b2b9e1a77ddab3a9d632aa0f3d

Add Verific SVA support for "always" properties

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

frontends/verific/verificsva.cc

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 909e9b4..225fd3e 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -1590,15 +1590,25 @@
 			Instance *consequent_inst = net_to_ast_driver(consequent_net);
 
 			if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL ||
-					consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH))
+					consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH ||
+					consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS))
 			{
 				bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH;
 
-				Net *until_net = consequent_inst->GetInput2();
-				consequent_net = consequent_inst->GetInput1();
-				consequent_inst = net_to_ast_driver(consequent_net);
+				Net *until_net = nullptr;
+				if (consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS)
+				{
+					consequent_net = consequent_inst->GetInput();
+					consequent_inst = net_to_ast_driver(consequent_net);
+				}
+				else
+				{
+					until_net = consequent_inst->GetInput2();
+					consequent_net = consequent_inst->GetInput1();
+					consequent_inst = net_to_ast_driver(consequent_net);
+				}
 
-				SigBit until_sig = parse_expression(until_net);
+				SigBit until_sig = until_net ? parse_expression(until_net) : RTLIL::S0;
 				SigBit not_until_sig = module->Not(NEW_ID, until_sig);
 				antecedent_fsm.createEdge(node, node, not_until_sig);