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

Fig. 6.3 r ##2 s

r s

clock ticks

Example 6.7 illustrates a typical situation when two sequences are not adjoining,
but there is a constant number of clock ticks between them (Fig. 6.3 ). There is a
special syntax to capture this situation:

r##ns

n must be a nonnegative elaboration time integral constant. We will call this interval
between two sequences in clock cycles delay (not to be confused with the delay
operator # in SystemVerilog).

Efficiency Tip. Big delay values are inefficient both in simulation and in FV.
Example 6.8. Using this syntax, the sequence from Example 6.7 may be rewritten
as req ##2 ack .

t

6.3.2 Top-Level Sequential Properties

As stated in Sect. 6.2 , there is a sequential property associated with each sequence
not admitting an empty match. With the exception of Boolean sequential properties,
top-level sequential properties are relatively rare in assertions and assumptions, and
they are normally used to specify reset sequences. 2

Example 6.9. Reset rst must be initially high and be low in clock tick 20.

Solution:

initial a1: assert property (@( posedge clk) rst ##20 !rst);

Discussion: We do not claim anything about the reset behavior in all clock ticks
other than 0 and 20. t

You should be very careful when using sequential properties in continuously
monitored assertions and assumptions since their meaning may be different from
your intent, as illustrated by the following examples.

Example 6.10. What does the following assertion mean?

a1: assert property (@( posedge clk) a ##1 b);

2 Top-level sequential properties are very common in cover statements, see Chap. 18 .