Re: Proposal for Parameterized And/Or operators

Cindy,

I like your suggestion even better.

Dana.

PS
I assume that when SERE operators are used curly brackets ({}) are
used instead of the parenthesis below. For example:
 for i in 0..15: && {a;b[i];c}

On Mon, 20 Dec 2004 11:01:23 +0200, Cindy Eisner <EISNER@il.ibm.com> wrote:
>
>
> 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 04:32:52 2004