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.
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.
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);
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
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 .
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 .
property a |-> b ##1 first_match (c[ * ] ##1 d) is
to a |-> b ##1 c[ * ] ##1 d .
equivalent (see Exercise 11.13 ):