Hardware Reference
In-Depth Information
Fork>0, pŒk is a named property whose declaration is obtained from that of p
by the following replacements:
- Each instance of a recursive property q in the declaration of p is replaced by
the instance of qŒk
1 obtained by passing the same actual arguments.
- Each instance of a non-recursive property q in the declaration of p is replaced
by the instance of qŒk obtained by passing the same actual arguments.
For any property ,thek-fold approximation to is denoted Œk and is obtained
from by replacing each instance of a named property p by the instance of pŒk
obtained by passing the same actual arguments. For a trace
w
and a local variable
context L, unclocked satisfaction of is defined by
w
;L
ˆ
iff
w
;L
ˆ
Œk for
all k>0.
Several examples are given below to illustrate how these definitions work.
Example 22.21.
Show that for
k
>0,
my_always[k](
q
)
is equivalent to
(
always
[0:k-1]
q
)
and nexttime
[k] 1'b1
;
where
my_always
is as declared in Fig.
17.1
.
Solution:
The definitions above imply the following declarations:
property
my_always[0] (
property
p);
1'b1;
endproperty
property
my_always[k] (
property
p);
(
nexttime
[0] p)
and nexttime
my_always[k-1](p);
endproperty
for
k
positive. Then we get
my_always[1](
q
)
(
nexttime
[0]
q
)
and nexttime
1'b1
(
always
[0:0]
q
)
and nexttime
[1] 1'b1
Suppose inductively that
my_always[k](
q
)
(
always
[0:k-1]
q
)
and nexttime
[k] 1'b1
Then
my_always[k+1](
q
)
(
nexttime
[0]
q
)
and nexttime
my_always[k](
q
)
(
nexttime
[0]
q
)
and
nexttime
(
(
always
[0:k-1]
q
)
and nexttime
[k] 1'b1
)
(
always
[0:k]
q
)
and nexttime
[k+1] 1'b1
Search WWH ::
Custom Search