Recursive Properties - SVA: The Power of Assertions in SystemVerilog - page 396

17.3.1 Negation and Strong Operators

RESTRICTION 1: The negation operator not and the strong operators
s_nexttime , s_eventually , s_always , s_until , and s_until_with can-
not be applied to any property expression that instantiates a recursive property.

In view of the Rewriting Algorithms in Annex F.4 of the LRM, this restriction
also forbids the application of these operators to an expression that, through
instances of nonrecursive properties, ultimately depends on an instance of a
recursive property.
Restriction 1 avoids the subtle interplay between negation and recursion.
Consider the following example:

property confounding;
nexttime not confounding;
endproperty
A naïve approach to the semantics of this property leads to contradiction. For
simplicity, consider the unclocked semantics (see Chap. 22 )of confounding over
an infinite trace w D ` ! , where ` is a normal letter (i.e., ` 62f> ; ?g ). Then also
w 1:: D ` ! D w and N w D w .Naïvely,

w ˆ confounding
iff w ˆ nexttime not confounding

w 1:: iff ˆ not confounding

[ w 1::

D w ]
w ˆ not confounding
iff [ N w D w ]
w 6ˆ confounding
Clearly, something is wrong with this argument. 3 SVA currently avoids the problem
by imposing Restriction 1 .
The strong operators are related to negation because negation interchanges weak
and strong. For example, s_eventually can be defined as a derived operator
according to

iff

s_eventually p not always not p

3 [ 40 ] provides an approach to negation and recursion that allows their free interplay. Additional
information is provided in the declarations of recursive forms that enables the interpretation
of satisfaction using either a co-Büchi or Büchi acceptance criterion. With this approach,
negation need not result in language complementation. For co-Büchi acceptance, one gets
w 6ˆ confounding and w 6ˆ not confounding . For Büchi acceptance, one gets w ˆ
confounding and w ˆ not confounding .[ 40 ] gives sufficient conditions on recursive
forms to ensure that co-Büchi and Büchi acceptance are equivalent and that negation results in
language complementation. Of course, confounding does not satisfy these conditions.