Hardware Reference
In-Depth Information
Fig. 11.7
Sequence
containment
r
clock ticks
s
11.1.6
Sequence Containment
The operator
r
within
s
checks that sequence
r
is contained within sequence
s
.
More precisely,
r
within
s
has a match in clock tick t iff
s
begins in clock tick
t
0
and has a match in clock tick t , and sequence
r
beginning in clock tick t
2
has a
match in clock tick t
3
, such that t
0
t
1
t
2
t , as shown in Fig.
11.7
.
The sequence containment operator belongs to the
intersect
family, and
r
within
s
is a shortcut for
1[
*
] ##1 r ##1 1[
*
]
intersect
s
. Notice that
r
may have more than one match while
s
is evaluated.
Example 11.19.
There should be at least one
read
request between two
write
requests.
Solution:
a1:
assert property
(write |=> (read ##1 1)
within
write[->1]);
Discussion:
Specifying
read ##1 1
and not just
read
is important when the case
of
read
appearing together with the second
write
should be excluded.
t
Example 11.20.
Two consecutive
write
requests cannot appear within a transac-
tion delimited by
start_t
and
end_t
(including transaction delimiters).
Solution:
assert property
(
start_t |->
not strong
(write[
*
2]
within
end_t[->1]));
Discussion:
We need to specify the
strong
qualifier here to keep the property
weak because the negation of a weak operator is strong (Chap.
10
). Without it,
this assertion would check among other things that each transaction eventually
completes. This is usually not part of the assertion intent. In addition, checking
the eventuality would impose heavy burden on FV tools.
t
Efficiency Tip.
within
operator has similar overhead as
intersect
(Sect.
11.1.4
).
Example 11.21.
The sequence
(a ##1 1)
within
b[->1]
is relatively efficient in
FV since it is equivalent to
!b[
*
] ##1 a ##0 !b[+] ##1 b
In contrast, sequence
a[->2]
within
b[->2]
is more expensive since it intro-
duces many combinations of
a
and
b
:first
a
then
b
then
a
then
b
; first two
a
and
then two
b
;
a
and
b
happening simultaneously, etc.
t
Search WWH ::
Custom Search