RE: Proposal for Parameterized And/Or operators

erich, dana,

i agree with erich on the syntax issue, but i think his proposal can be
improved. how about this:

for i in 0..15: &(a[i])

?? (where the "&" can be replaced with any operator, and in particular "|"
or "&&".)

cindy.

--------------------------------------------------------------------
Cindy Eisner
Formal Methods Group
IBM Haifa Research Laboratory
Haifa 31905, Israel
Tel: +972-4-8296-266
Fax: +972-4-8296-114
e-mail: eisner@il.ibm.com

"Erich Marschner" <erichm@cadence.com>@eda.org on 16/12/2004 00:59:10

Sent by: owner-ieee-1850-extensions@eda.org

To: "Dana Fisman" <dana.fisman@weizmann.ac.il>
cc: <ieee-1850-extensions@eda.org>
Subject: RE: Proposal for Parameterized And/Or operators

Hi Dana,

I think I understand the proposal. I have a few concerns about it.

First, the fact that the operators come before the definition of the
parameter seems to imply that we could end up with strange-looking
sequences or formulas in which an infix operator and a prefix operator
appear in sequence - e.g.,

  a[*] && | [i in {0:7}] b[*i]

This seems to be at least difficult to read, and potentially confusing. It
might also make parsing difficult for some implementations (because the
infix operator is expecting an operand, not another operator, to follow).

Also, it does not appear to be possible to define two parameters for the
same parameterized sequence or property - e.g.,

  | [i in {0:3}] [j in i+1:6}] {a[*i]; b[*j]}

Would it be possible to change the order of the parameter definition and
the operator (to address the first issue) and allow for a sequence of
parameter definitions (to address the second issue)? For example

  a[*] && [i in {0:3}] [j in i+1:6}] | {a[*i]; b[*j]}

To accomplish this, I think the syntax additions would have to be something
more like the following:

Sequence ::= Parameterized_Sequence

Parameterized_Sequence ::=
  Parameter_Definition { Parameter_Definition } Prefix_Operator Sequence

and similarly for Properties.

Note that this would also allow use of braces or parentheses if the user
feels that would make the PSL more readable, e.g.,

  a[*] && {[i in {0:3}] [j in i+1:6}] | {a[*i]; b[*j]}}

Would this be possible?

Regards,

Erich

| -----Original Message-----
| From: Dana Fisman [mailto:dana.fisman@weizmann.ac.il]
| Sent: Tuesday, December 07, 2004 7:58 AM
| To: ieee-1850-extensions@eda.org
| Cc: Erich Marschner
| Subject: Proposal for Parameterized And/Or operators
|
| Erich, All,
|
| Below is a proposal for adding parameterized AND/OR operators
| for formula and SEREs. The proposal adds the parameters types
| as allowed for forall in the current version LRM v1.1. Any
| extensions decided for forall can be applied to the
| parameterized and/or operators as well.
|
| The idea is to first define what is a the set obtained by
| parameterizing a property (or a sequence) and then define what
| it means to perform an and/or operator on a (parameterized) set.
|
| For example, first we define that for a SERE A, and an identifier
| i, the expression [i in {6..8} ] A(i) is equivalent to the set
| S containing the 3 elements: A(6), A(7) and A(8).
| Then we define that && S is equivalent to A(6) && A(7) && A(8).
|
| The required changes are elaborated below.
|
| Best regards,
| Dana.
|
|
| 1. Changes in the BNF (Appendix A):
|
| The following productions should be added:
|
| Parameter_definition ::= [ PSL_Identifier [ Index_Range ]
| in Value_Set ]
| Parameterized_SERE_Set ::= Parameter_definition Compound_SERE
| Parameterized_ FL_Property _Set ::= Parameter_definition FL_Poperty
|
| Compound_SERE ::=
| | & Parameterized_SERE_Set
| | && Parameterized_SERE_Set
| | | Parameterized_SERE_Set
|
| FL_Property ::=
| | AND_OP Parameterized_ FL_Property _Set
| | OR_OP Parameterized_ FL_Property _Set
|
|
| 2. Changes in formal definition (Appendix B):
|
| Addition of the appropriate syntactic sugaring to section B.3.1
| (Additional SERE Operators) and to section B.3.2 (Additional SERE
| Operators) as indicated in RED in the attached pdf.
|
|
| 3. Changes in the body of the LRM:
|
| I. Two sections should be added:
| a. A section describing parameterized SEREs should be added between
| section 6.1.1.2 to 6.1.1.2.1.
| b. A section describing parameterized properties should be added
| between section 6.2.1.7 to 6.2.1.7.1
| Below is a section describing parameterized SEREs. A
| section describing
| parameterized properties can be defined similarly (by replacing
| "Compound SERE" with "FL Property").
|
| II. The following sections should be changed to include application
| of the respective operator to a (parameterized) set.
|
| a. Section 6.1.1.2.1 SERE or (|)
| b. Section 6.1.1.2.2 SERE non-length-matching and (&)
| c. Section 6.1.1.2.3 SERE length-matching and (&&)
| d. Section 6.2.1.7.3 Logical and
| e. Section 6.2.1.7.4 Logical or
|
| Below are sections for SERE or (|) and Logical and. The others
| sections can be defined similarly.
|
| -------------------------------------
|
| Parameterized SEREs
|
| Introduction:
| The parameterizing operators, shown in Box xxx,
| constructs a set of Compound SEREs, each element in the set is
| obtained by instantiating a different possible value of the given
| parameter in the given compound SERE.
|
| Box:
| Parameterized_SERE_Set ::= Parameter_definition Compound_SERE
| Parameter_definition ::= [ PSL_Identifier [ Index_Range ] in
| Value_Set]
|
| Text following the box:
| The operands of the parameterizing
| operator are a parameter definition and a parameterized Compound
| SERE. The PSL Identifier in the parameter definition is the name
| of the parameter in the Compound SERE. This parameter can be an
| array. The Value Set defines the set of values the parameter can
| obtain.
| 1.
| If the parameter is not an array, and the set of
| values has size K then the obtained set is of size K. Each element
| in the set is obtained by substituting the parameter with one of
| the possible values in the set of values.
| 2.
| If the parameter is an array of size N, and the set of
| values has size
| K then the obtained set is of size K^N. Each element in
| the set is
| obtained by substituting each element in the array with one of the
| possible values in the set of values.
|
| The set of values can be specified in three different ways
| - The keyword boolean specifies the set of values {True, False}.
| - A Value Range specifies the set of all values within the
| given range.
| - The comma (,) between Value Ranges indicates the union of
| the obtained
| sets.
|
| Restrictions:
| *** Same as in the replicated properties section (6.2.3) ***
| ....
|
|
| Informal semantics:
|
| For Compound SERE A
|
| - [i in boolean] A(i) is equivalent to the set containing the two
| elements A(false) and A(true)
|
| - [i in {j:k}] A(i) is equivalent to the set containing the
| k-j+1 elements: A(j), A(j+1), , A(k)
|
| - [i in {j,l,k}] A(i) is equivalent to the set containing the 3
| elements: A(j), A(l) and A(k)
|
| - [i[0:1] in boolean] A(i) is equivalent to the set containing
| the 4 elements: ({false,false}), A({false,true}), A({true,false})
| and A({true,true})
|
| - [i[0:2] in [c,d]] A(i) is equivalent to the set containing the
| 8 elements: A({c,c,c}), A({c,c,d}), A({c,d,c}), A({c,d,d}),
| A({d,c,c}), A({d,c,d}), A({d,d,c})and A({d,d,d})
|
|
| -------------------------------------
|
| 6.1.1.2.1 SERE or (|)
|
| Introduction:
| The SERE or operator (|), shown in Box 28,
| constructs a Compound SERE in which one of several alternative
| Compound SEREs hold at the current cycle.
|
| Box:
| Compound_SERE ::= Compound_SERE | Compound_SERE
| Compound_SERE ::= | Parameterized_SERE_Set
|
| Text following the box: The operands of |are either two Compound
| SEREs or a set of compound SEREs given by a Parameterized_SERE.
|
| Restrictions:
| If the operand of | is a parameterized SERE then the
| set it defines should be non-empty.
|
| Informal semantics:
|
| For Compound SEREs A and B: A|B holds tightly on a path iff at
| least one of A or B holds tightly on the path.
|
| For a Parameterized SEREs Set S: | S holds tightly on a path iff
| at least one of the compound SEREs A in S holds tightly on the
| path.
|
| -------------------------------------
|
| 6.2.1.7.3 Logical and
|
| Introduction: The logical and operator, shown in Box 60, is used
| to specify logical and.
|
| Box:
| FL_Property ::= FL_Property AND_OP FL_Property
| FL_Property ::= AND_OP Parameterized_FL_Property_Set
|
| Text following the box: The operands of the logical and operator
| are either two FL Properties or a set of FL Properties given by a
| Parameterized_ FL_Property _Set.
|
| Restrictions:
|
| If the operand of the logical and is a parameterized property then
| the set it defines should be non-empty.
|
| Within the simple subset (see section 4.4.4), if the logical and
| has two operands then the left operand of a logical and is
| restricted to be a Boolean expression, otherwise all the elements
| in the set defined by the parameterized FL property but one are
| restricted to be Boolean expressions.
|
| Informal semantics:
|
| A logical and property holds in a given cycle of a given path iff
| the FL Properties that are the operands all hold at the given
| cycle. That is,
|
| For FL Properties f and g: F AND_OP g holds on a path iff both A
| and B holds on the path.
|
| For a Parameterized FL Property Set S: AND_OP S holds on a path
| iff all the FL Properties defined by S holds on the path.
|
|
|
|
|
Received on Mon Dec 20 01:03:33 2004