DRAFT, 2-NOV-2003

SVA 3.1A PROPOSAL:  PROPERTY NEGATION
-------------------------------------

DISCUSSION:
-----------

This proposal assumes that the proposal removing the special treatment
of negated boolean expressions in the clock rewrite rules has passed.

This proposal simplifies the SVA language by generalizing negation
to a unary property operator.  The syntax for property-level negation
is "not".

In SVA 3.1, negation can be applied only at the top level to entire 
sequence implications or to the consequent of a sequence implication.

If the proposal on generalized implication passes, then the top-level
criteria for negation become muddled.  For example, a property
expression whose consequent is negated may not be usable as a
consequent of an implication if negation is limited to the top level.

Therefore, it is proposed that negation be promoted to a general
property expression operator.

EXAMPLE:  If "p" is a property expression, then "not p" is also a 
property expression.


SEMANTICS
---------

1. Unclocked Semantics.

      w |= not p  iff  not({\bar w} |= p)

   In the presence of local variables:

      w,L |= not p  iff  not({\bar w},L |= p) 

2. Clock Rewrite Rule.  Here we must have the special treatment of 
   negated booleans eliminated.

      @(c)(not p)  |-->  not (@(c) p)



MULTIPLE CLOCK SUPPORT
----------------------

Property-level negation can be applied equally well to 
singly-clocked and multiply-clocked property expressions.

The leading clock of "not p" is the leading clock of "p".


PROPOSED CHANGES TO THE BNF:
----------------------------

[TBD.  Depends on the combination of proposals that pass.
Should be developed from a subset of the changes in the 
original combined proposal.]


PROPOSED CHANGES TO LRM TEXT:
-----------------------------

[TBD.  Depends on the combination of proposals that pass.
Should be developed from a subset of the changes in the 
original combined proposal.]
   

PROPOSED CHANGES TO THE FORMAL SEMANTICS:
-----------------------------------------

[TBD.  Depends on the combination of proposals that pass.
Should be developed from a subset of the changes in the 
original combined proposal.]