DRAFT, 2-NOV-2003

SVA 3.1A PROPOSAL:  GENERALIZED IMPLICATION
-------------------------------------------

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

This proposal extends the SVA language by generalizing the implication
opertors.  Under the proposal, any property expression is allowed as
the consequent of an implication.  Multilple clock support is
generalized to the overlapping implication (|->) provided the clock is
guaranteed not to change across the implication.

In particular, this proposal allows nesting of implications.  This
generalization gives flexibility to the user in deciding how to code
properties that involve multiple temporal events.

EXAMPLE 1:  By allowing nested implications, an implication such as 

   (s1 ## s2 ## s3) |=> s4

can be coded alternatively as 

   ((s1 ## s2) |=> (s3 |=> s4))

or as 

   (s1 |=> ((s2 ## s3) |=> s4))

or as 

   (s1 |=> (s2 |=> (s3 |=> s4)))

provided the emptyword does not tightly satisfy any of s1, s2, s3.

////

This proposal will provide the most benefit to users if the 
proposals on property instances and boolean property operators
are also passed.

* If the proposal on property instances is passed, then instances of
  defined properties can be consequents of implications.

* If any of the proposals on boolean property operators is passed,
  then combinations of properties formed using the associated
  operators can be consequents of implications.

EXAMPLE 2:  If the proposal on property instances is passed, then 
the following will be legal:

   property p1;
      ((s2 ## s3) |=> s4);
   endproperty

   property p2;
      (s1 |=> p1);
   endproperty

////

EXAMPLE 3:  If the proposal on property conjunction passes,
then instead of coding two separate property expressions

   (s1 |=> (s2 ## s3))

and

   (s1 |=> (s4 |=> s5))

which tends to hide the fact that the antecedent is shared, the 
user can combine them into one property expression

   (
      s1 
      |=> 
      (
         (s2 ## s3)
         and
         (s4 |=> s5)
      )
   )

////

This proposal is in alignment with proposed Accellera PSL 1.1.


PRECEDENCE AND ASSOCIATIVITY
----------------------------

The operators |->, |=> must be of the same precedence and right 
associative, since the antecedent of any implication must be a 
sequence expression, not a property expression.


SEMANTICS
---------

1. Unclocked Semantics.

      w |= r |-> p  
      iff  
      for all 0 <= i < |w| such that {\bar w}^{0..i} |== r, w^{i..} |= p

   In the presence of local variables,

      w,L0 |= r |-> p
      iff
      for all 0 <= i < |w| and L such that {\bar w}^{0..i},L0,L |== r,
      w^{i..},L |= p

2. Clock Rewrite Rule.

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

3. Derived Operator.  Semantically, "|=>" continues to be a derived operator, 
   defined by

      s |=> p  \equiv  (s ## @(1)1) |-> p
   

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

As in SVA 3.1, the clock can be changed after "##" in a sequence
expression and after "|=>" in a property expression.  Additionally,
the "|->" operator is explicitly allowed in multiply-clocked 
property expressions provided the clock doesn't change across this
operator.

To see the rationale for allowing "|->" in multiply-clocked sequences,
Let r1,s1,s2,t be unclocked sequences.  The implication

   (@(c)r1 ## @(d)(s1 ##0 s2)) |=> @(e)t

is legal in SVA 3.1, so we allow both

   @(c)r1 |=> (@(d) s1 |-> (@(d) s2 |=> @(e) t))

and

   (@(c)r1 ## @(d) s1) |-> (@(d) s2 |=> @(e) t))

under the generalized implication.

To make the condition that the clock not change across "|->" 
more precise,  define the "ending" and "leading" clocks as follows.

*. Let r be an unclocked sequence.  Then the leading and ending 
   clocks of @(c) r are c.

*. Let s1 and s2 be clocked sequences.  If the leading clocks of s1
   and s2 are the same and are not UNCERTAIN, then the leading clock
   of s1 ## s2 is the leading clock of s1.  Otherwise, if the
   emptyword does not tightly satisfy s1, then the leading clock of 
   s1 ## s2 is the leading clock of s1.  Otherwise the leading clock 
   of s1 ## s2 is UNCERTAIN.

*. Let s1 and s2 be clocked sequences.  If the ending clocks of s1 and
   s2 are the same and are not UNCERTAIN, then the ending clock of s1
   ## s2 is the ending clock of s2.  Otherwise, if the emptyword does
   not tightly satisfy s2, then the ending clock of s1 ## s2 is the
   ending clock of s2.  Otherwise the ending clock of s1 ## s2 is
   UNCERTAIN.

*. Let s be a clocked sequence and let q be a clocked property.  Then
   the leading clocks of s |-> q and s |=> q are both the leading
   clock of s.

*. Let r be an unclocked sequence and let p be an unclocked property.
   Then the leading clocks of @(c)(r |-> p) and @(c)(r |=> p) are c.

Then the requirement that the clock not change across "|->" is 
that the ending clock of the antecedent sequence expression equal
the leading clock of the consequent property expression and that
neither be UNCERTAIN.

If the proposal on property conjunction passes, then the leading clock
of "q1 and q2" is UNCERTAIN if the leading clocks of q1 and q2 are not
the same and is otherwise the common leading clock.  Similarly for
other property operators.


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.]