From f019e44e74e33ea48c8039c86cf69d841a13a3c3 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Fri, 13 Jun 2025 21:27:31 +0200 Subject: [PATCH] verificsva: Support the followed-by operator in cover mode The implementation for the implication operator in cover mode actually implements the followed-by operator, so we can re-use it unchanged. It is not always the correct behavior for the implication operator in cover mode, but a) it will only cause false positives not miss anything so if the behavior is unexpected it will be visible in the produced traces, b) it is unlikely to make a difference for most properties one would practically use in cover mode, c) at least one other widely used SVA implementations behaves the same way and d) it's not clear whether we can fix this without rewriting most of verificsva.cc --- frontends/verific/verificsva.cc | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 860d3c166..7652f8130 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -1613,7 +1613,10 @@ struct VerificSvaImporter } else if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || - inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) + inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION || + (mode_cover && ( + inst->Type() == PRIM_SVA_OVERLAPPED_FOLLOWED_BY || + inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION))) { Net *antecedent_net = inst->GetInput1(); Net *consequent_net = inst->GetInput2(); @@ -1621,7 +1624,7 @@ struct VerificSvaImporter SvaFsm antecedent_fsm(clocking, trig); node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); - if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) { + if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION || inst->Type() == PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY) { int next_node = antecedent_fsm.createNode(); antecedent_fsm.createEdge(node, next_node); node = next_node;