Hardware Reference

In-Depth Information

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
):

Search WWH ::

Custom Search