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

Example 6.45. Write a sequence describing a scenario when request req is granted
( gnt ) in two or more cycles.
Solution: req ##[2:$] gnt .
Discussion: This sequence does not specify that there be no grant in clock tick 1, it
just requires at least one grant to happen in two or more clock ticks. t

Example 6.46. What is the meaning of the following assertion?
initial a1: assert property (@( posedge clk) ##[ * ] s |-> p);

Solution: According to the definition of the overlapping implication, at each tight
satisfaction point of sequence ##[ * ]s property p should be true. This is equivalent
to the requirement that p is true starting at all tight satisfaction points of sequence
s with initial points 0, 1, .... Therefore, assertion a1 is equivalent to assertions a2
below:
a2: assert property (@( posedge clk) s |-> p);

Discussion: Assertions a1 and a2 are also equivalent to assertion a3 .
a3: assert property (@( posedge clk) ##[ * ] s |-> p);
Although assertions a1 , a2 , and a3 are logically equivalent, their simulation
performance is likely to be very different. Assertion a2 is the most efficient,
assertion a1 is much less efficient, but using assertion a3 may lead to a tremendous
performance degradation (see Sect. 19.3 ). FV performance for these three assertions
is generally the same. t

Efficiency Tip. Never use infinite initial delay in antecedents.

6.10 Unbounded Sequences

In Example 6.42 , we discussed the situation when a request had to be granted within
five clock ticks. The suggested assertion was
a1: assert property (@( posedge clk) req |-> ##[1:5] gnt);
We want now to modify the problem and require that the request req be granted
some time in the future, without specifying any upper bound. It may seem that the
only change required is to replace the range upper bound 5 with $ :
a2_wrong: assert property (@( posedge clk) req |-> ##[1:$] gnt);
or, equivalently,
a3_wrong: assert property (@( posedge clk) req |=> ##[ * ] gnt);
However, both assertions a2_wrong and a3_wrong are wrong . To understand
why, recall the definition of sequential property from Sect. 6.2 that we reproduce
here for convenience.