Basic Properties - SVA: The Power of Assertions in SystemVerilog - page 102

Example 5.19. What is the meaning of ( always p) and ( always q) ?
Solution: According to the definition of property and this property is true iff both
p and q hold in each clock tick, that is, the original property is equivalent to
always (p and q) .
Discussion: ( always p) or ( always q) is not equivalent to always (p or q) .
Consider a case when p holds in all odd clock ticks, and q holds in all even ticks.
Then always (p or q) is true, whereas ( always p) or ( always q) is false. t

5.6 Until Property

Property p until q is true in clock tick i iff p is true in every clock tick j i
until, but not including, the first clock tick k i where q is true. If there is no such
k, p should be true in all clock ticks j i .
It follows that property p until q is true iff the property p is true in every clock
tick until (but not including) the first clock tick where q is true. See Fig. 5.5 .If q
never happens p should be true forever.
Note that p until q does not mean that p cannot be true starting from the clock
tick when q becomes true. It only means that p does not have to be true after q
becomes true for the first time. Also, the operator until is nonoverlapping : p does
not have to be true when q becomes true for the first time (though, of course, p may
be true at this moment).
There is also an overlapping version of until called until_with . The only
difference between until and until_with is that for until_with to be true p must
be true at the moment q becomes true for the first time, as stated in the following
definition:
Property p until_with q is true iff the property p is true in every clock tick
until (and including) the first clock tick where q is true. See Fig. 5.6 .If q never
happens p should be true forever. We leave the definition of the truth of property
until_with in clock tick i as an exercise to the reader.
p until_with q is equivalent to p until (p and q) . (Why? See Exer-
cise 5.8 .)

Example 5.20. Table 5.2 contains an initial trace fragment of signals a , b , c , d ,

and e .
￿ a until b is true since b is true in clock tick 0.
￿ a until c is true since a is true in clock tick 0, and c is true in clock tick 1.

p p p p p q

Fig. 5.5 until property clock ticks

p p p p p pq

Fig. 5.6 until_with
property clock ticks