From 3cbca5064cfbb418ac69d703034f8bb780a9cc41 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Fri, 21 Apr 2023 17:19:42 +0200
Subject: [PATCH] verific: Handle non-seq properties with VerificClocking
conditions
---
frontends/verific/verificsva.cc | 17 +++++++++++------
1 file changed, 11 insertions(+), 6 deletions(-)
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 ||