DRAFT, 13-OCT-2003

SVA 3.1A PROPOSAL:  NEGATED BOOLEANS
------------------------------------

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

This proposal eliminates the special treatment of negated booleans
in the clock rewrite rules of the SVA formal semantics.  This special
treatment blurs the distinction between boolean negation and property
negation, which only complicates the semantics.

If b is a boolean expression, then the current rewrite rules treat 

1.   @(c) not b 

the same as 

2.   @(c) !b

and not the same as any of the following:

3.   @(c) not (b ##0 1'b1)

4.   @(c) not (b and 1'b1)

5.   @(c) not (b or b)

Under the proposal, 1. will be semantically equivalent to 3., 4., and 
5., while 2. will be semantically distinct.  The rationale for this
change is that "not" is a property-level negation and so the treatment
of "@(c) not b" should be consistent with first promoting "b" to be 
a sequence and then promoting that sequence to be a property.  The 
proposal also restores the distinction between "not" and "!" applied to
boolean expressions.

This change has been recommended as a matter of alignment by the 
SVA/PSL Alignment Subcommittee.


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

NONE.



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

NONE.   


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

1. p. 347, G.3.1.  Delete

      * @(c) not b ---> @(c) !b.

2. p. 347, G.3.1.  Change

      * @(c) not R ---> not @(c) R, provided R is not a boolean expression

   to 

      * @(c) not R ---> not @(c) R

If the proposal on Nested Implications and Boolean Property Connectives is 
approved, then replace 2 by

2'. p. 347, G.3.1.  Change

      * @(c) not R ---> not @(c) R, provided R is not a boolean expression

   to 

      * @(c) not P ---> not @(c) P