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

read or write request happens simultaneously with end_t and start_t , and the
transactions do not overlap, we need to rewrite the assertion as
a2: assert property (start_t |=>
!start_t throughout (read[=2] ##1 !read) intersect
(write[=3] ##1 !write) intersect end_t[->1]);
Exercise 11.8 introduces yet another interpretation of this assertion: read and
write request may happen at any time, but when they happen at the end of the
transaction they are not counted as part of the current transaction.

t

intersect operator does not really add more expressive power to the language,
but it makes formulas exponentially more concise [ 23 ]. One can get a feeling why
it is so by attempting to rewrite the assertion in Example 11.14 without intersect
(see Exercise 11.7 ). Moreover, Example 11.15 is even more convincing. To rewrite
assertions a1 and a2 without intersect , it is necessary to explicitly list all possible
combinations of read and write :
read[=2] ##[0:1] write[=3] or read[=1] ##[0:1] write[=2] ##[0:1]
read[=2] or ...

Efficiency Tip. Operator intersect may be expensive in FV. The reason is that
most FV engines in their internal representation eliminate the intersect operator
and generate all possible combinations of events. The greater the number of these
combinations, the more expensive it is for FV. However, it should be understood that
intersect does not introduce inefficiency by itself (though some FV engines may
process intersect less efficiently than the equivalent explicit representation), but
it allows concise coding of complex sequences. Therefore, if intersect is really
needed, there is no choice but to use it. However, if it is possible to write a more
specific assertion instead, eliminating the need for intersect , this should be the
first choice. For instance, if it is known in Example 11.15 that all write requests
precede the read requests, read[=2] intersect write[=3] should be replaced
by write[=3] ##1 read[=2] .
In simulation, the overhead of intersect is acceptable except when sequence is
compiled into an automaton in which case memory blow-up may occur during the
automaton construction (see Sect. 19.3 ). This blow-up occurs in FV too.

Limiting Sequence Size. Sometimes it is desirable to keep only those sequence
matches that occur during some number of first clock ticks. This can be done
using the idiom s intersect 1[ * 1:n] , where s is a sequence, and n is an integer
constant. Sequence 1[ * 1:n] has matches in clock ticks 1, ..., n ; therefore, only
matches of s that happen during the first n clock ticks are retained, while all others
are ignored.
This method may be used to truncate the antecedent sequences to boost simula-
tion performance, as shown in Example 11.16 . Note, however, that it is inefficient
in FV.

Example 11.16. If acknowledgment ack is received after req , ready should be
asserted simultaneously with the acknowledgment receipt.