Advanced Properties - SVA: The Power of Assertions in SystemVerilog - page 220

In s |-> q , where s must be a sequence and q some property, the evaluation of
q starts at the time when any evaluation thread of s has a match. In p implies q ,
p and q are properties, hence there is no notion of an endpoint and a match. Both p
and q start evaluating at the same time and the truth results are computed using the
logical operator implies . For example, consider
a ##1 b |-> c ##1 d
vs.
a ##1 b implies c ##1 d
In the case of |-> , the consequent c ##1 d will start evaluating when a ##1 b
matches. In the case of implies , both a ##1 b and c ##1 d start evaluation at
the same clock tick. Finally, if p is a sequence s , writing strong (s) implies q
is equivalent to s |-> q only when s is a Boolean expression. The Boolean
implication b1 -> b2 is a short-hand for ! bit '(b1)|| b2 . Therefore, unlike
property and suffix implications, such Boolean expressions have no notion of
vacuity of evaluation. That is, the evaluation of b1 -> b2 as a sequence property is
always nonvacuous (see Sect. 10.6 ).
An interesting example that uses implies is as follows.
Example 10.3. The signal sig should be high from m>=0 clock ticks before event
ev happens until n>=0 clock ticks after it. That is, if ev happens at time 10, m=2 ,
and n=3 , then sig should be high at times 8, 9, :::, 13.
Solution:
a1: assert property (
strong (##m ev) implies sig[ * (m+n+1)]);
We have used a strong sequence strong (##m ev) in the antecedent of implies
so as to require that there are enough clock ticks for ev to become true.
To express the same using |-> the assertion becomes more complex:
a2: assert property (
(!sig |-> !ev[ * (m+1)]) and (ev |-> sig[ * (n+1)]));

t

Equivalence

The property p iff q is true iff either properties p and q are both true or they are
both false (Chap. 22 ).
Like the case of implies , when p and q are Boolean expressions e1 and e2 ,
respectively, then e1 iff e2 is equivalent to e1 <-> e2 provided the clock ticks,
e.g., if the clock is the global clock.
When can iff be used? A very useful application is in verifying that two property
definitions have the same meaning: The same property may be implemented
in different ways because one implementation may be much more efficient in
simulation and the other in formal verification. Often the two properties look and