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();
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 986a98643..222c7d2e9 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -1598,12 +1598,17 @@ struct VerificSvaImporter
 
 		if (inst == nullptr)
 		{
-			log_assert(trig == State::S1);
-
-			if (accept_p != nullptr)
-				*accept_p = importer->net_map_at(net);
-			if (reject_p != nullptr)
-				*reject_p = module->Not(NEW_ID, importer->net_map_at(net));
+			if (trig != State::S1) {
+				if (accept_p != nullptr)
+					*accept_p = module->And(NEW_ID, trig, importer->net_map_at(net));
+				if (reject_p != nullptr)
+					*reject_p = module->And(NEW_ID, trig, module->Not(NEW_ID, importer->net_map_at(net)));
+			} else {
+				if (accept_p != nullptr)
+					*accept_p = importer->net_map_at(net);
+				if (reject_p != nullptr)
+					*reject_p = module->Not(NEW_ID, importer->net_map_at(net));
+			}
 		}
 		else
 		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||