Hi,
quick question.
can we use |-> and ##0 interchangeably in SVA, ie consider
property p1(a,b);
@(posedge clk) a |-> b;
endproperty
Is this same as:
property p2(a,b);
@(posedge clk) a ##0 b;
endproperty
I know when it comes to coverage there is subtlety here, I don’t want to discuss that within the scope of this question.
All I want to understand here is that if p1 and p2 are the same then why is SVA built up on the default “Antecedent implies Consequent ie (A |-> B)” terminology in all learning sources.
Kind Regards
In reply to curious_learner:
It’s hard to fully comprehend the differences without knowing what “a” and “b” represent and how these properties are used in directives.
If “a” and “b” are boolean expressions, then a ##0 b is the same as a && b.
assert property (p2(A,B));
The above fails every clock cycle A&&B is false.
If “a” and “b” are boolean expressions, then a |-> b is almost the same as !a || b
assert property (p1(A,B));
The above only fails if A && !B. But the property is only considered “covered” when A && B is true.
It starts getting more complicated when “a” and “b” are sequences, but I hope this is enough to show you the key differences.