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