diff options
author | Clifford Wolf <clifford@clifford.at> | 2018-03-06 01:51:42 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2018-03-06 01:51:42 +0100 |
commit | 588ce0e34a771552ebb3e0c2d10320a990fdad3b (patch) | |
tree | e242f765c1abb0e8c155098fbde8c144d2a778b2 /frontends/verific | |
parent | cedbc35f4b4a0244d6499a8a682b42086fb28dfd (diff) | |
download | yosys-588ce0e34a771552ebb3e0c2d10320a990fdad3b.tar.gz yosys-588ce0e34a771552ebb3e0c2d10320a990fdad3b.tar.bz2 yosys-588ce0e34a771552ebb3e0c2d10320a990fdad3b.zip |
Simplified SVA "until" handling
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends/verific')
-rw-r--r-- | frontends/verific/verificsva.cc | 41 |
1 files 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; |