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

11.1.7 First Match of a Sequence

It is sometimes convenient to discard all sequence matches but the first one. This
can be achieved using the operator first_match . Sequence first_match (s) has
a match in clock tick t iff sequence s has a match in clock tick t , and it has no match
in any clock tick <t.

Example 11.22. If a and b have values 1 in clock ticks 0-4 then sequence
a[ * 1:2] ##1 b[ * 2:3] has matches in clock ticks 2, 3, and 4. In contrast, sequence
first_match (a[ * 1:2] ##1 b[ * 2:3]) has only one match in clock tick 2.

t

Example 11.23. When request req is issued and thereafter the first data chunk is
received as identified by data bit asserted, acknowledgment ack should be sent.
Solution:
a1: assert property ( first_match (req ##[+] data) |-> ack);

Discussion: Here, the first_match operator guarantees that the acknowledgment
is only sent when data is asserted for the first time. The same assertion rewritten
using the goto repetition should be more efficient:
a2: assert property (req ##1 data[->1] |-> ack);

t

Example 11.24. Let us modify the requirement of Example 11.23 : Acknowledg-
ment ack should be sent in response to a request, when two data chunks are received
in consecutive clock ticks for the first time. The first solution can be easily adapted
as follows:

a3: assert property ( first_match (req ##[+] data[ * 2]) |-> ack);
The second solution can also be modified in the following way:
a4: assert property (req ##1 data[->1] ##1 data |-> ack);
Again, assertion a4 is likely to be more efficient than a3 .

t

Trailing first_match in Sequential Properties. Trailing first_match in sequen-
tial properties, both weak and strong is redundant and can be omitted. For
simplicity we explain this statement for strong sequential properties. Property
strong (r ##1 s) is true iff there exists a match of sequence r ##1 s . This match
exists if there exists a match of r followedbyamatchof s , but this is equivalent
to the statement that there exists a match of r followedbythe first match of s .
Therefore, strong (r ##1 s) is equivalent to strong (r ##1 first_match (s)) .
Similarly, it can be shown that a trailing first_match in the outermost and or or
branch in a sequential property is redundant. For example, the sequential property
r1 ##1 first_match (s) or r2 is equivalent to r1 ##1 s or r2 .
Example 11.25. The property a |-> b ##1 first_match (c[ * ] ##1 d) is

equivalent to a |-> b ##1 c[ * ] ##1 d . The following properties are not

equivalent (see Exercise 11.13 ):