Subject: [sv-ac] draft proposal for nested implication, boolean property connectives
From: John Havlicek (john.havlicek@motorola.com)
Date: Mon Sep 08 2003 - 07:21:00 PDT
DRAFT, 08-SEP-2003
SVA 3.1A PROPOSAL: NESTED IMPLICATIONS AND BOOLEAN PROPERTY CONNECTIVES
------------------------------------------------------------------------
DISCUSSION:
-----------
This proposal extends the SVA language by allowing nested implications
and boolean property connectives. These changes give significantly
more flexibility to the user in deciding how to code properties that
involve multiple temporal events and how best to code shared
subproperties.
By allowing nested implications, an implication such as
(s1 ## s2) |=> s3
can be coded alternatively as
(s1 |=> (s2 |=> s3))
The user can also render "(s2 |=> s3)" as a defined property, say p1,
and code yet another alternative
(s1 |=> p1)
By allowing general properties on the right-hand side of implications,
the usefulness of defined properties is magnified.
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. The proposal allows general negation of properties and
combination of properties using "and" and "or". Thus, one can
write a form such as
(s1 |=> (s2 and (s3 |=> s4))) ,
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 very 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)
| 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
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)
| 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
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
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
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
6. 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
7. 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
PROPOSED CHANGES TO LRM TEXT:
-----------------------------
[To be determined.]
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
| (R |-> P) // "implication" form
| disable iff (b) P // "abort" 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
| (S |-> Q) // "implication" form
| disable iff (b) Q // "abort" 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.2.3.5. Add
* (P1 and P2) \equiv not(not P1 or not P2).
* (Q1 and Q2) \equiv not(not Q1 or not Q2).
6. p. 346, G.3.1. Change
* @(c) (R) ---> (@(c) R).
to
* @(c) (P) ---> (@(c) P).
7. 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.
8. p. 347, G.3.1. Delete
* @(c) not b ---> @(c) !b.
9. 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
10. 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).
11. p. 347, G.3.1. Add
* @(c) (P1 or P2) ---> (@(c) P1 or @(c) P2).
12. p. 348, Neutral satisfaction of properties. Add
* w |= (P) iff w |= P.
13. 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.
14. p. 348, Neutral satisfaction of properties. Change
* w |= not \phi iff not({\bar w} |= \phi).
to
* w |= not P iff not(\bar w |= P).
15. 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.
16. p. 348, Neutral satisfaction of properties. Add
* w |= (P1 or P2) iff w |= P1 or w |= P2.
17. 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.
18. 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).
19. 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.
20. 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.
This archive was generated by hypermail 2b28 : Mon Sep 08 2003 - 07:22:08 PDT