Hardware Reference
In-Depth Information
empty sequence is rarely used explicitly, but it is often used implicitly as part of
other sequences, for example, in repetition ranges of the form
[
*
]
or
[
*
0:n]
.Inthis
section, we provide several examples illustrating a peculiar behavior of sequences
admitting an empty match.
Example 6.37.
The following assertion is
illegal
:
assert property
(@(
posedge
clk) a[
*
]);
The reason is that in this assertion the sequence
a[
*
]
is promoted to a property
while it admits an empty match.
t
Example 6.38.
Sequence
a ##1 b[
*
0:2] ##1 c
matches traces
ac
,
abc
, and
abbc
. Note that in the trace
ac
there is no gap between
a
and
c
:
b[
*
0]
does not
have any duration in time!
t
Example 6.39.
Sequence
a[
*
] ##0 b[
*
]
is equivalent to
a[+] ##0 b[+]
, since
the sequence fusion does not admit an empty match (Sect.
6.5.1
).
Discussion:
a[
*
] ##1 b[
*
]
is
not
equivalent to
a[+] ##1 b[+]
.
t
6.8.1
Antecedents Admitting Empty Match
Sequences admitting an empty match have many subtle points when they are used
as antecedents. We will illustrate their behavior on sequence
a[
*
]
. Other sequences
admitting an empty match exhibit a similar behavior. Consider overlapping imp-
lication
a[
*
] |-> p
first. According to the definition of zero-or-more repetition
(Sect.
6.7.1.2
), it is equivalent to
a[
*
0]
or
a[+] |-> p
. All nonempty matches
of the antecedent are matches of
a[+]
, and therefore
a[
*
] |-> p
is equivalent
to
a[+] |-> p
. Therefore, it is possible to limit antecedents of overlapping
implications with sequences that do not admit an empty match. The sequences
admitting empty matches add nothing new in this case.
4
Now consider nonoverlapping implication
a[
*
] |=> p
. It can be rewritten as
(a[
*
0]
or
a[+]) ##1 1 |-> p
, which is equivalent to
(a[
*
0] ##1 1)
or
(a[+] ##1 1) |-> p
(see Exercise
6.2
). The first disjunct
of the antecedent is equivalent to 1, and the whole property can be reduced to
p
(see Sect.
6.5.1.1
). Therefore, in the nonoverlapping implication the antecedents
admitting an empty match are
completely redundant
when the assertion is contin-
uously monitored. To summarize, antecedents admitting an empty match in suffix
implications usually indicate a problem in the assertion.
Search WWH ::
Custom Search