Subject: [sv-ac] revised proposal: nesting and boolean connectives
From: John Havlicek (john.havlicek@motorola.com)
Date: Mon Sep 08 2003 - 14:05:42 PDT
REVISION, 09-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 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
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
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
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
| clocking_event property_expr
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
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.
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
| (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
| (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.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 - 14:06:47 PDT