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

Fig. 11.2 Sequence e[->2]

! e e ! e ! e e

clock ticks

11.1.2 Goto Repetition

Motivation Example.

Example 11.2. After request req is serviced by done asserted, signal ready should

be asserted.

Solution: We need to check ready in the clock tick following the clock tick when
done became high for the first time after req is asserted:
a1: assert property (req ##1 !done[ * ] ##1 done |=> ready);

t

The situation when something should happen for the first time described in
Example 11.2 is very common. There is a special sequence operator, a goto
repetition , stating that the condition e must happen for the first time: e[->1] .For
an arbitrary integer constant n 0, e[->n] , where e is a Boolean, is a shortcut for
(!e[ * ]##e)[ * n] . This sequence has a match when e happens for the nth time,
as shown in Fig. 11.2 .
Unlike the consecutive repetition described in Sect. 6.5 which can be applied to
arbitrary sequences, the goto repetition may be applied only to Boolean values.

Example 11.3. Using goto repetition, the assertion from Example 11.2 may be

rewritten as

t

a2: assert property (req ##1 done[->1] |=> ready);

It is also possible to specify ranges in goto repetition: e[->m:n] , 0 m n, has
a match when e happens for the mth, m C 1st,...,andthenth time. The upper bound
of the range may also be open-ended ( $ ). The formal definitions are as follows (we
assume that m n ):

b[->m:n] (!b[ * ] ##1 b)[ * m:n] .
b[->m:$] (!b[ * ] ##1 b)[ * m:$] .
b[->m] (!b[ * ] ##1 b)[ * m] .
Example 11.4. After start is asserted, at each occurrence of request req , starting
from the second and ending with the fifth one, enable en must be asserted.
Solution:

t

a1: assert property (start ##1 req[->2:5] |-> en);

Example 11.5. After start is asserted, at each occurrence of request req , starting
from the second one, enable en must be asserted.
a1: assert property (start ##1 req[->2:$] |-> en);

t