mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-07-19 10:52:03 +00:00
Code Activity

verificsva: Support the followed-by operator in cover mode

Browse source 
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
This commit is contained in:
Jannis Harder 2025-06-13 21:27:31 +02:00
parent 67f8de54dc
commit f019e44e74
1 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

7
frontends/verific/verificsva.cc
View file

@ -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;