Hardware Reference
In-Depth Information
nexttime
[0]
does not guarantee an advance in time, and infinitely many evalua-
tions of
p
are specified beginning in the same time step.
17.3.4
Actual Arguments
RESTRICTION 4: For every recursive instance of property
q
in the declara-
tion of property
p
, each actual argument expression
e
of the instance satisfies
at least one of the following conditions:
e
is a formal argument of
p
.
No formal argument of
p
appears in
e
.
e
is bound to a local variable formal argument of
q
.
This restriction is intended to avoid problematic recursive instances that result
from passing compound actual argument expressions. Such instances can lead
to an explosion of distinct actual argument expressions as the recursion unfolds.
Such explosion has undesirable consequences for the complexity and tractability of
checking the properties.
As an example of a problematic recursive instance, consider the following
example that violates
Restriction 4
:
property
illegal_arg(
longint unsigned
u, v, w);
u==v
*
w
and nexttime
illegal_arg(u, v+w, v
*
w);
endproperty
Since the formal arguments of
illegal_arg
are not local variables, they are treated
as reference arguments. This means that successive recursive instances require
composition of the compound actual argument expressions. Tracking the evolution
of the recursion, the comparison
u==v
*
w
expands to
cycle comparison
0
u==v
*
w
1
u == (v+w)
*
(v
*
w)
2
u == ((v+w)+(v
*
w))
*
((v+w)
*
(v
*
w))
3
u == (((v+w)+(v
*
w))+((v+w)
*
(v
*
w)))
*
(((v+w)+(v
*
w))
*
((v+w)
*
(v
*
w)))
and so on, where the arithmetic is performed modulo 2
64
, as specified by the
unsigned
longint
type of the formal arguments and the rules for bitwidths in
expressions. Even though the data type is bounded, the management of these
expressions quickly gets out of hand.
4
4
See [
22
] for an example, due to D. Bustan, that shows how a recursive form violating the
restrictions can represent a language that is not omega-regular.
Search WWH ::
Custom Search