From 4e5f1f59d66b96c5e0592e4f9810cca5d55c6894 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 1 Mar 2018 19:37:36 +0100 Subject: [PATCH] Fix in Verific SVA importer handling of until_with Signed-off-by: Clifford Wolf --- frontends/verific/verificsva.cc | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index e6430e9c5..70c28e387 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -974,11 +974,6 @@ struct VerificSvaImporter SvaFsm until_fsm(module, clock, clockpol, disable_iff); node = parse_sequence(&until_fsm, until_fsm.startNode, until_net); - if (until_with) { - int next_node = until_fsm.createNode(); - until_fsm.createEdge(node, next_node); - node = next_node; - } until_fsm.createLink(node, until_fsm.acceptNode); SigBit until_match = until_fsm.getAccept(); @@ -993,9 +988,12 @@ struct VerificSvaImporter antecedent_match_q->attributes["\\init"] = Const(0, 1); antecedent_match = module->Or(NEW_ID, antecedent_match, antecedent_match_q); - antecedent_match = module->And(NEW_ID, antecedent_match, not_until_match); + SigBit antecedent_match_filtered = module->And(NEW_ID, antecedent_match, not_until_match); + + module->addDff(NEW_ID, clock, antecedent_match_filtered, antecedent_match_q, clockpol); - module->addDff(NEW_ID, clock, antecedent_match, antecedent_match_q, clockpol); + if (!until_with) + antecedent_match = antecedent_match_filtered; } SvaFsm consequent_fsm(module, clock, clockpol, disable_iff, antecedent_match); -- 2.30.2