Hardware Reference
In-Depth Information
Fig. 11.4
Sequence
e[=2]
!
e
e
!
e
!
e
e
!
e
e
clock ticks
Solution:
Using consecutive repetition this assertion may be written as:
a1:
assert property
(start_t |=>
(!end_t
throughout
(!sent[
*
] ##1 sent)[
*
4]
##1 !sent[
*
]) ##1 end_t);
Using goto repetition, this assertion may be rewritten in a more compact way:
a2:
assert property
(start_t |=>
(!end_t
throughout
sent[->4] ##1 !sent[
*
]) ##1 end_t);
t
The situation discussed in Example
11.10
where some Boolean must be true
a predefined number of times between the match of one sequence and the begin-
ning of another is rather common. There is a sequence operator
[=...]
, called
nonconsecutive repetition
, that designates it. More precisely, sequence
e[=n]
has a
match in some clock tick if before this clock tick
e
occurs exactly
n
times, as shown
in Fig.
11.4
.
Like goto repetition, the nonconsecutive repetition may be applied only to
Boolean (integral) values.
Example 11.11.
Using nonconsecutive repetition, the assertion from Example
11.10
may be rewritten as
a3:
assert property
(
start_t |=> (!end_t
throughout
sent[=4]) ##1 end_t);
t
It is possible to specify ranges in nonconsecutive repetition:
e[=m:n]
,
0
m
n, has a match when e is true for the mth, m
C
1st,..., and the nth
time. The upper bound of the range may also be infinite (
$
). The formal definitions
are as follows (we assume that
m
n
):
b[=m:n]
b[->m:n] ##1 !b[
*
]
.
b[=m:$]
b[->m:$] ##1 !b[
*
]
.
b[=m]
b[->m] ##1 !b[
*
]
.
Example 11.12.
During one transaction delimited by
start_t
and
end_t
, packets
ranging from 2 to 4 should be sent (
sent
asserted).
sent
is not to be checked when
start_t
or
end_t
is asserted.
Solution:
a1
assert property
(
start_t |=> (!end_t
throughout
sent[=2:4]) ##1 end_t);
t
Example 11.13.
If during one transaction less than two packets are sent (
sent
asserted), the
shortt
bit should be asserted when
end_t
is asserted.
sent
is not
to be checked when
start_t
or
end_t
is asserted.
Search WWH ::
Custom Search