From ec47bf174549f4f2430c08e0d24bb9ba7bd5390d Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Fri, 21 Apr 2023 16:51:42 +0200
Subject: [PATCH] verific: Handle conditions when using sva_at_only in
 VerificClocking

This handles conditions on clocked concurrent assertions in unclocked
procedural contexts.
---
 frontends/verific/verific.cc | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 605dcdfb2..bc61c9c82 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -2011,6 +2011,28 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a
 
 	Instance *inst = net->Driver();
 
+	// Detect condition expression in sva_at_only mode
+	if (sva_at_only)
+	do {
+		Instance *inst_mux = net->Driver();
+		if (inst_mux->Type() != PRIM_MUX)
+			break;
+
+		bool pwr1 = inst_mux->GetInput1()->IsPwr();
+		bool pwr2 = inst_mux->GetInput2()->IsPwr();
+
+		if (!pwr1 && !pwr2)
+			break;
+
+		Net *sva_net = pwr1 ? inst_mux->GetInput2() : inst_mux->GetInput1();
+		if (!verific_is_sva_net(importer, sva_net))
+			break;
+
+		inst = sva_net->Driver();
+		cond_net = inst_mux->GetControl();
+		cond_pol = pwr1;
+	} while (0);
+
 	if (inst != nullptr && inst->Type() == PRIM_SVA_AT)
 	{
 		net = inst->GetInput1();