Basic Sequences - SVA: The Power of Assertions in SystemVerilog - page 127

Informally speaking ##[m:n] s means skipping from m to n clock ticks before
the initial point of s , and ##[m:$] s means skipping m or more clock ticks before
the initial point of s . As usual, there is a shortcut ##[ * ]s for ##[0:$] s (“zero or
more clock ticks”), and ##[+] s for ##[1:$] s (“one or more clock ticks”).
Efficiency Tip. Big delay factors, and ranges with big finite upper bound are
inefficient both in simulation and in FV. Infinite delay ranges may also be inefficient
in simulation. Their efficiency is explained in detail in Sect. 19.3 . Infinite delay
ranges are efficient in FV if their lower bound is small.

Example 6.40. Write a sequence describing the scenario when ready is asserted at
the end of the transaction (signal etrans asserted) or in the next clock tick after it.
Solution: trans ##[0:1] ready t

Example 6.41. Write the following sequence: grant gnt asserted from two to four
clock ticks after request req was asserted.
Solution: req ##[2:4] gnt
Discussion: If the initial point is 0, this sequence means: req is true in clock tick
0, and gnt is true either in clock tick 2, 3, or 4. It does not say anything about req
behavior after clock tick 0: req does not have to be deasserted there, though it can
be. Neither does this sequence claim that gnt is false in clock ticks 0, 1, 5, .... t
Example 6.42. Request req must be granted (grant gnt should be asserted) within

five clock ticks.

Solution:

a1: assert property (@( posedge clk) req |-> ##[1:5] gnt);

Discussion: In this example, it is also possible to have one gnt issued for several
requests, as shown in Fig. 6.8 . t

Example 6.43. The device should become ready ( ready asserted) from 10 to 12
cycles after power-on.

Solution:

initial a1: assert property (@( posedge clk) ##[10:12] ready);

Discussion: This assertion states that ready is asserted either in clock tick 10, 11
or 12. It does not state that ready must be continuously asserted in clock ticks 10,
11 and 12. Neither does it state that ready cannot be asserted before clock tick 10.
t

Example 6.44. Write a sequence describing a scenario when request req is granted
( gnt is received).
Solution: This means that gnt is asserted in one or more clock ticks after req :
req ##[+] gnt .

t