DRAFT, 2-NOV-2003

SVA 3.1A PROPOSAL:  PROPERTY IF-ELSE
------------------------------------

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

This proposal assumes that the proposals on generalized implication
and property conjunction pass.

This proposal extends the SVA language by allowing if-else combination
of property expressions as a property expression.  The syntax of the 
if-else is

   if (boolean_expr) property_expr [else property_expr]

Cascading if-else can be used to achieve the effect of a case split.

The need for if-else combination of properties arises when a
precondition can be matched in several ways that obligate different
consequents.  This is especially important for coding assertions when
the precondition must be sensitive to several temporal events, as is
the case when transactions can evolve in several different ways.

This proposal is important for giving the user a way to record
syntactically that the combination of properties is exclusive.  Note
that the user can derive singly-clocked "if-else" in the usual way:

   if (b) p1 else p2  \equiv  ((b |-> p1) and (!b |-> p2))

However, coding using the style of the righthand side requires both
users and tools to recognize the semantic relationship between the
antecedents of the conjoined implications.


EXAMPLE:  Suppose there is a defined sequence 

   sequence trans_start(type, config);
      ...
   endsequence

that detects the start of a transaction and samples the type 
and configuration of the transaction into the local variable
arguments "type" and "config", respectively.  Suppose that
for each of types 0 through 3 there is a corresponding defined
property

   property check_trans_type_<i>(config);
      ...
   endproperty

that checks correctness of a transaction of type <i> according
to its configuration argument.  Then we can write a property to 
check correctness of any transaction such as

   property check_trans;

      [0:1] type;
      <config_type> config;
      
      trans_start(type,config)
      |->
      if (type == 0)
         check_trans_type_0(config)
      else if (type == 1)
         check_trans_type_1(config) 
      else if (type == 2)
         check_trans_type_2(config) 
      else if (type == 3)
         check_trans_type_3(config) 
      ;

   endproperty

[By the way, I do not understand why we require ";" after a 
sequence/property expression in a defined sequence/property
just before the keyword endsequence/endproperty.  Isn't it
clear that it is not needed due to the ending keyword?]

////

The current proposal enhances the usefulness of the proposals on
generalized implication and property instances.

This proposal is in semantic alignment with proposed Accellera PSL 1.1.

SEMANTICS
---------

1. Unclocked Semantics.  "if-else" is a derived operator, defined by

      if (b) p1  \equiv  (b |-> p1)
      if (b) p1 else p2  \equiv  (b |-> p1) and (!b |-> p2)

2. Clock rewrite rule.  Since "if-else" is derived, no clock rewrite 
   rule is needed.

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

For multiple clock support, "if (b) p1 else p2" (respectively, 
"if (b) p") must have an unambiguous leading clock.  This clock 
is the clock for the testing the boolean expression b, and each 
of p1 and p2 (resp. p) must also have the same leading clock.


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

[TBD.  Depends on the combination of proposals that pass.]


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

[TBD.  Depends on the combination of proposals that pass.]
   

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

[TBD.  Depends on the combination of proposals that pass.]