Advanced Sequences - SVA: The Power of Assertions in SystemVerilog - page 249

Table 11.3 Past temporal operators

Operator Description

sofar p Holds in clock tick t iff p holds in all clock ticks t 1 t (Fig. 11.8 ).

once p Holds in clock tick t iff p holds in some clock tick t 1 t (Fig. 11.9 ).

p since q Holds in clock tick t iff q holds in some clock tick t 1 t ,andp holds in

all clock ticks t 2 , t 1 <t 2 t (Fig. 11.10 ).

p backto q A weak version of p since q:ifq has not happened yet, p should hold in

all clock ticks t 1 t .

previously p Holds in clock tick t iff t ¤ 0,andp holds in clock tick t 1 (Fig. 11.11 ).

before p Holds in clock tick t iff either t D 0 or p holds in clock tick t 1. Thus,

the only difference between previously p and before p is that previously p
is false in clock tick 0, whereas before p is true.

sequence ack;
!rst throughout enable ##[1:10] end_ack;
endsequence
One problem remains: the reset specified by the disable iff operator is
asynchronous (see Chap. 13 ), while the behavior of the throughout operator is
synchronous: it is checked only at clock ticks. Usually, this difference is not
important. When it is, the sequence to which the method triggered is applied as
well as the assertion should be controlled by the global clock if it exists.

t

To make the sequence to which the method triggered is applied sensitive to
the assertion disabling condition reset , include !reset throughout as the
top operator in the sequence. The sequence is disabled synchronously with
the clock ticks of the sequence, however.

p p p p p p

t clock ticks

Fig. 11.8 sofar property

p

t

Fig. 11.9 once property

clock ticks

q p p p

t

clock ticks

Fig. 11.10 since property