Hardware Reference
In-Depth Information
to be
recursive
iff it belongs to a nontrivial strongly connected component of the
dependency digraph. An instance of a named property p is said to be
recursive
iff
it appears within the declaration of a named property q such that p and q belong to
the same nontrivial strongly connected component of the dependency digraph. This
condition is satisfied iff there is a loop in the dependency digraph that has at least
one arc and that passes through both p and q.
9
Example 22.20.
Compute the dependency digraph for the following named pro-
perty declarations:
property
p1;
a
and nexttime
p2(p2(p3));
endproperty
property
p2(
property
p)
eventually
[0:1] p;
endproperty
property
p3;
b
and nexttime
p1;
endproperty
Identify which named properties are recursive and which instances are recursive.
Solution:
The node set of the dependency digraph is V
Df
p1
;
p2
;
p3
g
. The dec-
laration of
p1
instantiates
p2
(twice) and
p3
, so there are directed edges
p1
!
p2
and
p1
!
p3
in the edge set E. Similarly, there is a directed edge
p3
!
p1
in E.
Below is a graphical representation of the dependency digraph. There is a single
p1
p2
p3
nontrivial strongly connected component in the digraph consisting of the nodes
f
p1
;
p3
g
. Therefore,
p1
and
p3
are recursive properties. The instance of
p3
in the
declaration of
p1
and the instance of
p1
in the declaration of
p3
are both recursive
instances.
p2
is a non-recursive property. It is worth noting that, under rewriting, the
instance
p2(p2(p3))
expands to
eventually
[0:1]
eventually
[0:1] p3
;
which is equivalent to
eventually
[0:2] p3
.
t
For k
0,thek-fold approximation to a named property p is denoted pŒk and
is defined as follows:
pŒ0 is a named property whose declaration is obtained from that of p by replacing
the body property by
1'b1
.
9
In case p
D
q, the loop can be a self-loop on p.
Search WWH ::
Custom Search