Question

This section defines the neutral semantics of instances of recursive properties in terms of the neutral semantics of instances of non-recursive properties. The latter can be expanded to properties in the abstract syntax by appropriate substitutions, and so their semantics is assumed to be understood.

According to Restriction 1 in Section 17.11.3, it is understood below that the negation operator not cannot be applied to any property expression that instantiates a recursive property. Restriction 2 in Section 17.11.3 is not represented here because disable iff is treated as a general property-building operator in this appendix. A precise version of Restriction 3 is given below.

Named property p is said to depend on named property q if there exist n > 0 and named properties p0,...,pn such that p0 = p, pn = q, and for all 0 < i < n, the declaration of property pi instantiates property pi+1. In particular, by taking q = p and n = 0, it follows that property p depends on property p.

A named property p has an associated dependency digraph. The nodes of the digraph are all the named properties on which p depends. If q and r are nodes of the digraph, then there is an arc from q to r for each instance of r in the declaration of q. Such an arc is labelled by the minimum number of timesteps that are guaranteed from the beginning of the declaration of q until the particular instance r. For example, if q is declared by:

property q;
(a |-> r)
and
((b ##1 c[*0:3]) |=> r);
endproperty

where a, b, c are boolean expressions, then there is one arc from q to r labeled by “0” due to a |-> r and there is a second arc from q to r labeled by “2” due to (b ##1 c[*0:3]) |=> r.

A named property p is called recursive if its node appears on a cycle in the dependency digraph of p. The following is a precise version of Restriction 3:

RESTRICTION 3: The sum of the arc labels around any cycle of the dependency digraph of a recursive property must be positive.

Let p(X) be an instance of a recursive named property p, where X denotes the actual arguments of the instance.

For k > 0, the k-fold approximation to p(X), denoted p[k](X), is an instance of a non-recursive property p[k] defined inductively as follows.

— The declaration of p[0] is obtained from the declaration of p by replacing the body property_expr with the literal 1’b1.

— For k > 0, the declaration of p[k] is obtained from the declaration of p by replacing each instance of a recursive property by its (k – 1)-fold approximation.

The semantics of the instance p(X) is then defined as follows. For any word w over Σ and local variable context

L, w, L |= p(X) iff for all k > 0, w,L |= p[k](X).