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

Fig. 11.5 Sequence
intersection

r

clock ticks

s

Solution:

a1: assert property (
start_t ##1 (!end_t throughout sent[=0:1]) ##1 end_t
|-> shortt);

t

Efficiency Tip. Big factors and ranges in nonconsecutive repetition are inefficient
both in simulation and in formal verification. In simulation, a nonconsecutive
repetition may be expensive if it causes long or never-ending and overlapping
attempts, as explained in Sect. 19.3 .

11.1.4 Intersection

Intersection of two sequences r and s is a sequence r intersect s , which has a
match when both sequences have a match simultaneously (see Fig. 11.5 ).

Example 11.14. A command consists of two in-order read actions and one write
action. After the command is issued ( command is asserted), the completion of the
write action ( write_complete ), and the completion of the second read action
( read_complete ) should happen simultaneously.
Solution: To express simultaneous completion, we use the intersect operator:
a1: assert property (
command |->
write_complete[->1] intersect read_complete[->2]);

t

Example 11.15. Each transaction delimited by start_t and end_t should contain
two read requests and three write requests.
Solution: In this case, we need to spot a clock tick t with the following

characteristics:

￿ There should be exactly two read requests issued before t .
￿ There should be exactly three write requests issued before t .
￿ At clock tick t , the first occurrence of end_t should happen.
We can express this using the following assertion:

a1: assert property (start_t |->
read[=2] intersect write[=3] intersect end_t[->1]);
Assertion a1 allows the last read or write request to happen simultaneously
with the end of the transaction end_t and also with start_t . If we require that no