From ec47bf174549f4f2430c08e0d24bb9ba7bd5390d Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 21 Apr 2023 16:51:42 +0200 Subject: [PATCH 1/2] 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(); From 3cbca5064cfbb418ac69d703034f8bb780a9cc41 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 21 Apr 2023 17:19:42 +0200 Subject: [PATCH 2/2] 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 ||