mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 03:32:29 +00:00
Code Activity

Fix verific eventually handling

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-06-29 19:24:58 +02:00
parent 0404cf61d5
commit 8b92ddb9d2
1 changed files with 5 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

11
frontends/verific/verificsva.cc
View file

@ -1488,13 +1488,16 @@ struct VerificSvaImporter
bool eventually_property(Net *&net, SigBit &trig) bool eventually_property(Net *&net, SigBit &trig)
{ {
Instance *inst = net_to_ast_driver(net);
if (inst == nullptr)
return false;
if (clocking.cond_net != nullptr) if (clocking.cond_net != nullptr)
trig = importer->net_map_at(clocking.cond_net); trig = importer->net_map_at(clocking.cond_net);
else else
trig = State::S1; trig = State::S1;
Instance *inst = net_to_ast_driver(net);
if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY) if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
{ {
if (mode_cover || mode_trigger) if (mode_cover || mode_trigger)
@ -1523,7 +1526,6 @@ struct VerificSvaImporter
int node; int node;
log_dump(trig);
SvaFsm antecedent_fsm(clocking, trig); SvaFsm antecedent_fsm(clocking, trig);
node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net); 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) {
@ -1540,7 +1542,6 @@ struct VerificSvaImporter
if (verific_verbose) { if (verific_verbose) {
log(" Eventually Antecedent FSM:\n"); log(" Eventually Antecedent FSM:\n");
antecedent_fsm.dump(); antecedent_fsm.dump();
log_dump(trig);
} }
return true; return true;
@ -1690,8 +1691,6 @@ struct VerificSvaImporter
SigBit sig_a, sig_en = trig; SigBit sig_a, sig_en = trig;
parse_property(net, &sig_a, nullptr); parse_property(net, &sig_a, nullptr);
log_dump(trig, sig_a, sig_en);
// add final FF stage // add final FF stage
SigBit sig_a_q, sig_en_q; SigBit sig_a_q, sig_en_q;