DRAFT, 31-OCT-2003

SVA 3.1A PROPOSAL:  BOOLEAN PROPERTY CONNECTIVES
------------------------------------------------

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

This proposal extends the SVA language by allowing boolean property
connectives.  In particular:

1. "and" and "or" are provided as a general binary connectives on property 
   expressions.

2. "not" is promoted to a general unary operator on property expressions.

3. "if-else" is provided as a boolean case-splitting connective on property
   expressions.

Boolean combinations of properties arise naturally when a single
precondition obligates a combination of responses.  The user will want
to have the freedom to decide how to partition the obligations and
code them.  

EXAMPLES:

* (s1 |=> (p1 and (not p2))

* (s1 |=> if (b) p1 else p2)

which intuitively means, "if s1 is observed, then s2 must be observed
and, concurrently with s2, if s3 is observed, then s4 must be
observed".

The proposal also promotes the abort operator to a general
property-building construct.  As a result, nesting of abort operators
will be possible, with the effect that the abort conditions
accumulate.

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

The extensions are achieved with little disruption to the current
LRM because they are accomplished by relaxing restrictions.  The
formal semantics is simplified by these changes.  All the extensions
are in alignment with Accellera PSL.


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

1. p. 168, Box 17-12.  Change

      property_expr ::=                              
         ... 
         | sequence_expr |-> [ not ] sequence_expr 
         | sequence_expr |=> [ not ] sequence_expr 

   to 

      property_expr ::=                              
         ...
         | sequence_expr |-> property_expr
         | sequence_expr |=> property_expr

2. p. 168, Box 17-12.  Change

      multi_clock_property_expr ::= 
         ... 
         | multi_clock_sequence |=> [ not ] multi_clock_sequence

   to

      multi_clock_property_expr ::=                     
         ...
         | multi_clock_sequence |=> multi_clock_property_expr

3. p. 176, Box 17-14.  Change

      property_expr ::=                              
           sequence_expr
         | sequence_expr |-> [ not ] sequence_expr 
         | sequence_expr |=> [ not ] sequence_expr 
         | (property_expr)

   to 

      property_expr ::=                              
           sequence_expr
         | (property_expr)
         | not property_expr
         | property_expr or property_expr
         | property_expr and property_expr
         | disable iff (expression) property_expr
         | sequence_expr |-> property_expr
         | sequence_expr |=> property_expr
         | property_instance

4. p. 176, Box 17-14.  Change

      multi_clock_property_expr ::= 
           multi_clock_sequence 
         | multi_clock_sequence |=> [ not ] multi_clock_sequence
         | (multi_clock_property_expr)

   to

      multi_clock_property_expr ::=                     
           multi_clock_sequence
         | (multi_clock_property_expr)
         | not multi_clock_property_expr
         | multi_clock_property_expr or multi_clock_property_expr
         | multi_clock_property_expr and multi_clock_property_expr
         | disable iff (expression) multi_clock_property_expr
         | multi_clock_sequence |=> multi_clock_property_expr
         | clocking_event property_expr
         | property_instance

5. p. 177, Box 17-15.  Change

      multi_clock_property_expr ::= 
           multi_clock_sequence 
         | multi_clock_sequence |=> [ not ] multi_clock_sequence
         | (multi_clock_property_expr)

   to

      multi_clock_property_expr ::=                     
           multi_clock_sequence
         | (multi_clock_property_expr)
         | not multi_clock_property_expr
         | multi_clock_property_expr or multi_clock_property_expr
         | multi_clock_property_expr and multi_clock_property_expr
         | disable iff (expression) multi_clock_property_expr
         | multi_clock_sequence |=> multi_clock_property_expr
         | clocking_event property_expr
         | property_instance

6. p. 279.  Change

      assert_property_statement ::= 
           assert property ( property_spec ) action_block 
         | assert property ( property_instance ) action_block

   to

      assert_property_statement ::= 
           assert property ( property_spec ) action_block 

7. p. 279.  Change

      cover_property_statement ::= 
           cover property ( property_spec ) action_block 
         | cover property ( property_instance ) action_block

   to

      cover_property_statement ::= 
           cover property ( property_spec ) action_block 

8. p. 280.  Change

      property_spec ::= 
           [clocking_event ] [ disable iff ] ( expression ) [ not ] property_expr 
         | [ disable iff ( expression ) ] [ not ] multi_clock_property_expr

   to 

      property_spec ::= 
           property_expr
         | multi_clock_property_expr

9. p. 280.  Change

      property_expr ::=                              
           sequence_expr
         | sequence_expr |-> [ not ] sequence_expr 
         | sequence_expr |=> [ not ] sequence_expr 
         | (property_expr)

   to 

      property_expr ::=                              
           sequence_expr
         | (property_expr)
         | not property_expr
         | property_expr or property_expr
         | property_expr and property_expr
         | disable iff (expression) property_expr
         | sequence_expr |-> property_expr
         | sequence_expr |=> property_expr
         | property_instance

10. p. 280.  Change

      multi_clock_property_expr ::= 
           multi_clock_sequence 
         | multi_clock_sequence |=> [ not ] multi_clock_sequence
         | (multi_clock_property_expr)

   to

      multi_clock_property_expr ::=                     
           multi_clock_sequence
         | (multi_clock_property_expr)
         | not multi_clock_property_expr
         | multi_clock_property_expr or multi_clock_property_expr
         | multi_clock_property_expr and multi_clock_property_expr
         | disable iff (expression) multi_clock_property_expr
         | multi_clock_sequence |=> multi_clock_property_expr
         | clocking_event property_expr
         | property_instance



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

1. p. 168, first line of 17.7.11.  Change

      monitor sequences based on satisfying some criteria

   to 

      monitor properties based on satisfying some criteria

2. p. 168, paragraph after box 17-12.  Change

      This clause is used to precondition monitoring of a sequence

   to 

      This clause is used to precondition monitoring of a property

   Also change

      the right-hand side operand sequence_expr is called consequent

   to

      the right-hand side operand property_expr is called consequent

3. p. 169, first line.  Change

      consequent sequence_expr

   to

      consequent property_expr

4. p. 169, line 3.  Change 

      start point of the consequent sequence_expr

   to

      start point of the evaluation of the consequent property_expr

5. p. 169, line 4.  Change

      consequent sequence_expr

   to
   
      consequent property_expr

6. p. 169, line 4.  Change

      The satisfaction of the consequent sequence_expr means that there 
      is at least one match of the sequence_expr

   to

      If the consequent property_expr is a sequence_expr, then it is
      satisfied as a property_expr provided there is at least one match
      match of the sequence_expr.

7. p. 169, line 6.  Delete

      Nesting of implications is not allowed.

8. p. 169, line 8.  Change

      the first element of the consequent sequence_expr is evaluated 
      on the same clock tick

   to
   
      the evaluation of the consequent property_expr begins
      on the same clock tick

9. p. 169, line 9.  Change

      the first element of the consequent sequence_expr is evaluated
      on the next clock tick

   to

      the evaluation of the consequent property_expr begins
      on the next clock tick

10. p. 169, line 11.  Change 

      sequence_expr |=> [not] sequence_expr

   to

      sequence_expr |=> property_expr

11. p. 169, line 13.  Change

      sequence_expr ##1 `true |-> [not] sequence_expr

   to   

      sequence_expr ##1 `true |-> property_expr

12. p. 170, paragraph after figure 17-14, line 3.  Change
 
      before continuing to match those sequences

   to

      before evaluating their consequents

14. p. 170, paragraph after figure 17-14, line 4.  Change

      by removing the precondition for the sequence

   to 

      by removing the precondition for the consequent 

15. p. 171, after example p16.  Add

      This property can be coded alternatively as a nested 
      implication:

         property p16_nested;
            (write_en & data_valid) |->
               (write_en && (retire_address[0:4]==addr)) [*2] |-> 
                  ##[3:8] write_en && !data_valid && (write_address[0:4]==addr);
         endproperty

16. p. 176, paragraphs after box 17-14.  Change

      The result of property evaluation is either true or false. There are
      two kinds of property: sequence, and implication. If the property is
      just a sequence, the result of a sequence for every evaluation attempt
      is true or false. This is accomplished by implicitly transforming
      sequence_expr to first_match(sequence_expr). That is, as soon as a
      match of sequence_expr is determined, the result is considered to be
      true, and no other matches are required for that evaluation
      attempt. However, if the property is an implication, then the
      semantics of implication determine whether the property is true or
      false.

      The disable iff clause allows asynchronous resets to be specified. For
      a particular attempt, if the expres-sion of the disable iff becomes
      true at any time during the evaluation of the attempt, then the
      attempt for the property is considered to be a success. Other attempts
      are not affected by the evaluation of the expression for an
      attempt. 
      
      The not clause states that the property_expr associated with the
      property must never evaluate to true. Effectively, it negates
      property_expr. For each attempt, property_expr results in either true
      or false, based on whether there is a match for the sequence. The not
      clause reverses the result of property_expr. It should be noted that
      there is no complementation or any form of negation for the sequence
      in property_expr.

   to

      The result of property evaluation is either true or false. There are
      six kinds of property: sequence, negation, disjunction, conjunction,
      implication, and reset.

      A property that is a sequence evaluates to true if and only if
      there is a match of the sequence.  Since there is a match if and
      only if there is a first match, evaluation of such a property is
      the same as implicitly transforming its sequence_expr to
      first_match(sequence_expr).  As soon as a match of sequence_expr
      is determined, the evaluation of the property is considered to
      be true, and no other matches are required for that evaluation
      attempt.

      A property is a negation if it has the form 

         not property_expr

      For each evaluation attempt of the property, there is an
      evaluation attempt of property_expr.  The keyword not states
      that the evaluation of the property is the opposite of the
      evaluation of the underlying property_expr.  Thus, if
      property_expr evaluates to true, then not property_expr
      evaluates to false, and if property_expr evaluates to false,
      then not property_expr evaluates to true.

      A property is a disjunction if it has the form 

          property_expr1 or property_expr2

      The property evaluates to true if and only if at least one of 
      property_expr1 and property_expr2 evaluates to true.

      A property is a conjunction if it has the form 

          property_expr1 and property_expr2

      The property evaluates to true if and only if both
      property_expr1 and property_expr2 evaluate to true.

      A property is an implication if it has the form

          sequence_expr |-> property_expr

      or

          sequence_expr |=> property_expr

      The meaning of implications has already been discussed in 17.7.11.

      A property is a reset if it has the form 

         disable iff (expression) property_expr

      The expression of the disable iff is called the reset
      expression.  The disable iff clause allows asynchronous resets
      to be specified.  For an evaluation of the property, there is an
      evaluation of the underlying property_expr.  If the reset
      expression becomes true at any time before the evaluation of the
      underlying property_expr has completed, then the overall
      evaluation of the property is true.  Otherwise, the evalution of
      the property is the same as that of the property_expr.  The
      reset expression is tested independently for different
      evaluation attempts of the property.

      An instance of a defined property can be used as a property_expr.
      If an instance of a defined property is used as the consequent of 
      an overlapping implication, then the defined property must have 
      the same clock event as the antecedent of the implication.  See 
      Section 17.11.

17. p. 177, after line 8.  Add examples illustrating the new
   property forms.  [TBD]

18. p. 177, after box 17-15.  Change

      Two cases are allowed:

      1) Concatenation of two sequences, where each sequence can have
         a different clock

      2) The antecedent of an implication on one clock, while the 
         consequent is on another clock

   to

      As in the case of singly-clocked properties, the result of 
      evaluating a multi-clock property is either true or false. 
      The meanings of negation, disjunction, conjunction, and reset
      are the same for multi-clock properties as they are for 
      singly-clocked properties, with the exception that the 
      underlying property expressions can be multiply clocked.

      The two multi-clock features that require special attention are:

      1) Building a multi-clock sequence by multi-clock concatenation of 
         two sequences.  The two sequences can have different clocks or 
         can be multiply clocked.

      2) Building a multi-clock implication from an antecedent sequence 
         and a consequent property.  The antecedent and consequent can
         have different clocks or can be multiply clocked.

19. p. 178, line 6.  Change 

      to the nearest clock tick of the clock of the consequent sequence

   to

      to the nearest clock tick of the leading clock of the consequent
      property

20. p. 178, end of 17.11.  Add examples of boolean combinations and 
   nesting in multi-clocked properties.  [TBD]

21. [TBD]  Add tables of precedence for the property operators.
   Ideally, the precedence will be aligned with Accellera PSL.

   

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

1. p. 344, G.2.1.  Change the abstract grammar for unclocked properties 
   from

      P ::= [disable iff ( b )] [not] R                // "sequence" form 
         | [disable iff ( b )] [not] ( R |-> [not] R ) // "implication" form
   
   to 
   
      P ::= R                    // "sequence" form
   	 | (P)                   // "parenthesis" form
   	 | not P                 // "negation" form
   	 | (P or P)              // "or" form
   	 | (P and P)             // "and" form
   	 | (R |-> P)             // "implication" form
   	 | disable iff (b) P     // "reset" form
   
2. p. 344, G.2.1.  Change the abstract grammar for clocked properties from

      Q ::= @(b) P                                   // "clock" form 
   	 | [disable iff ( b )] [not] S               // "sequence" form 
   	 | [disable iff ( b )] [not] (S |-> [not] S) // "implication" form

   to 

      Q ::= @(b) P               // "clock" form
   	 | S                     // "sequence" form
   	 | (Q)                   // "parenthesis" form
   	 | not Q                 // "negation" form
   	 | (Q or Q)              // "or" form
   	 | (Q and Q)             // "and" form
   	 | (S |-> Q)             // "implication" form
   	 | disable iff (b) Q     // "reset" form

3. p. 344, G.2.2.  Delete 

      * \phi is an unclocked property fragment provided 
        disable iff (b) \phi is an unclocked property. 
   
      * N is a negation specifier if N is either the empty token or not.

   Delete also 
  
      \phi denotes an unclocked property fragment; N, N_1 , N_2 denote 
      negation specifiers;

4. p. 345, G.2.3.1.  Change

      * ( R_1 |=> N R_2 ) \equiv (( R_1 ##1 1 ) |-> N R_2 ) . 

   to 
   
      * (R |=> P) \equiv ((R ##1 1) |-> P).

   Change

      * ( S_1 |=> N S_2 ) ((S_1 ## @(1) 1 ) |-> N S_2 ) .

   to 

      * (S |=> Q) \equiv ((S ## @(1) 1) |-> Q).


5. p. 346, G.3.1.  Change

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

   to

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

6. p. 347, G.3.1.  Change

      * @(c) disable iff (b) \phi ---> disable iff (b) @(c) \phi.

   to

      * @(c) disable iff (b) P ---> disable iff (b) @(c) P.

7. p. 347, G.3.1.  Delete

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

8. 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
   
9. p. 347, G.3.1.  Change

      * @(c) N_1 ( R_1 |-> N_2 R_2 ) \equiv N_1 ( @(c) R_1 |-> @(c) N_2 R_2 ) .

   to

      * @(c) (R |-> P) ---> (@(c) R |-> @(c) P).

10. p. 347, G.3.1.  Add

      * @(c) (P1 or P2) ---> (@(c) P1 or @(c) P2).

      * @(c) (P1 and P2) ---> (@(c) P1 and @(c) P2).


11. p. 348, Neutral satisfaction of properties.  Add

      * w |= (P) iff  w |= P.

12. p. 348, Neutral satisfaction of properties.  Change

      * w |= disable iff (b) \phi iff either w |= \phi or there 
        exists 0 <= k < |w| such that w^k |= b and 
        w^{0,k-1}\top^\omega |= \phi.  Here, w^{0,-1} denotes the 
        empty word.
   to

      * w |= disable iff (b) P iff either w |= P or there exists 
        0 <= k < |w| such that w^k |= b and w^{0,k-1}\top^\omega |= P.  
        Here, w^{0,-1} denotes the empty word.

13. p. 348, Neutral satisfaction of properties.  Change

      * w |= not \phi iff not({\bar w} |= \phi).

   to

      * w |= not P iff not(\bar w |= P).


14. p. 348, Neutral satisfaction of properties.  Change

      * w |= (R_1 |-> N R_2) iff for every 0 <= j < |w| such that 
        {\bar w}^{0,j} |== R_1, w^{j..} |=  N R_2 . 

   to 

      * w |= (R |-> P) iff for all 0 <= j < |w| such that 
        {\bar w}^{0,j} |== R, w^{j..} |= P.

15. p. 348, Neutral satisfaction of properties.  Add

      * w |= (P1 or P2) iff w |= P1 or w |= P2.

      * w |= (P1 and P2) iff w |= P1 and w |= P2.

16. p. 351, Neutral satisfaction of properties (with local variables).
   Change

      * w,L0 |= disable iff (b) \phi iff either w,L0 |= \phi or there exists 
      	0 <= k < |w| such that w^k |= b and w^{0,k-1}\top^\omega,L0 |= \phi.  
      	Here, w^{0,-1} denotes the empty word.

   to

      * w,L0 |= disable iff (b) P iff either w,L0 |= P or there exists 
      	0 <= k < |w| such that w^k |= b and w^{0,k-1}\top^\omega,L0 |= P.  
      	Here, w^{0,-1} denotes the empty word.

17. p. 351, Neutral satisfaction of properties (with local variables).
   Change

      * w,L0 |= not \phi iff not(\bar w,L0 |= \phi).

   to
      
      * w,L0 |= not P iff not(\bar w,L0 |= P).

18. p. 351, Neutral satisfaction of properties (with local variables).
   Change

      * w,L0 |= (R_1 |-> N R_2) iff for all 0 <= j < |w| and L1 such that 
      	{\bar w}^{0,j},L0,L1 |== R_1, w^{j..},L1 |= N R_2.
      
   to
      
      * w,L0 |= (R |-> P) iff for all 0 <= j < |w| and L1 such that 
      	{\bar w}^{0,j},L0,L1 |== R, w^{j..},L1 |= P.

19. p. 351, Neutral satisfaction of properties (with local variables).
   Add

      * w,L0 |= (P) iff  w,L0 |= P.
   
      * w,L0 |= (P1 or P2) iff w,L0 |= P1 or w,L0 |= P2.

      * w,L0 |= (P1 and P2) iff w,L0 |= P1 and w,L0 |= P2.

