From 588ce0e34a771552ebb3e0c2d10320a990fdad3b Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 6 Mar 2018 01:51:42 +0100 Subject: [PATCH] Simplified SVA "until" handling Signed-off-by: Clifford Wolf --- frontends/verific/verificsva.cc | 41 +++++++++++++-------------------- 1 file changed, 16 insertions(+), 25 deletions(-) diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index ecff42679..6b3d3b932 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -205,6 +205,8 @@ struct SvaFsm log_assert(!materialized); log_assert(0 <= from_node && from_node < GetSize(nodes)); log_assert(0 <= to_node && to_node < GetSize(nodes)); + log_assert(from_node != acceptNode); + log_assert(to_node != acceptNode); if (throughout_sig != State::S1) { if (ctrl != State::S1) @@ -221,6 +223,7 @@ struct SvaFsm log_assert(!materialized); log_assert(0 <= from_node && from_node < GetSize(nodes)); log_assert(0 <= to_node && to_node < GetSize(nodes)); + log_assert(from_node != acceptNode); if (throughout_sig != State::S1) { if (ctrl != State::S1) @@ -994,14 +997,6 @@ struct VerificSvaImporter antecedent_fsm.createEdge(node, next_node); node = next_node; } - antecedent_fsm.createLink(node, antecedent_fsm.acceptNode); - - SigBit antecedent_match = antecedent_fsm.getAccept(); - - if (verific_verbose) { - log(" Antecedent FSM:\n"); - antecedent_fsm.dump(); - } Instance *consequent_inst = net_to_ast_driver(consequent_net); @@ -1019,26 +1014,22 @@ struct VerificSvaImporter if (until_inst != nullptr) parser_error("Currently only expressions are allowed in SVA_UNTIL condition", until_inst); - SvaFsm until_fsm(clocking); - node = parse_sequence(until_fsm, until_fsm.startNode, until_net); - until_fsm.createLink(node, until_fsm.acceptNode); - - SigBit until_match = until_fsm.getAccept(); - SigBit not_until_match = module->Not(NEW_ID, until_match); - - if (verific_verbose) { - log(" Until FSM:\n"); - until_fsm.dump(); - } + SigBit until_sig = importer->net_map_at(until_net); + SigBit not_until_sig = module->Not(NEW_ID, until_sig); + antecedent_fsm.createEdge(node, node, not_until_sig); - SigBit antecedent_match_q = module->addWire(NEW_ID); - antecedent_match = module->Or(NEW_ID, antecedent_match, antecedent_match_q); - SigBit antecedent_match_filtered = module->And(NEW_ID, antecedent_match, not_until_match); + antecedent_fsm.createLink(node, antecedent_fsm.acceptNode, until_with ? State::S1 : not_until_sig); + } + else + { + antecedent_fsm.createLink(node, antecedent_fsm.acceptNode); + } - clocking.addDff(NEW_ID, antecedent_match_filtered, antecedent_match_q, State::S0); + SigBit antecedent_match = antecedent_fsm.getAccept(); - if (!until_with) - antecedent_match = antecedent_match_filtered; + if (verific_verbose) { + log(" Antecedent FSM:\n"); + antecedent_fsm.dump(); } bool consequent_not = false; -- 2.30.2