Re: Proposal for Parameterized And/Or operators

Erich,

I am against your suggestion of default values. I am also against
using the word "forall" instead of the "for" Cindy suggested.

Regarding the first,
I believe your suggestion for having different default values for
properties and sequences will be confusing for users.
I also don't understand the motivation for disjunction of a sequence
(neither I understand exactly the proposal: does it apply to
standalone sequences? what about applying it to the entire left hand
side or right hand side of a suffix implication operator?).

Regarding the second,
part of the motivation for the parameterized and/or operators was to
leave "forall" for the directive as per Tej's proposal. Another
motivation was to avoid questions about replication and implementation
(having the semantics evident from the operator which is explicitly
stated in the syntax). And yet another motivation was to avoid
questions of the dual (is there a forsome? in what sense are they
dual? when forall applies to sequences is it && or &? what is the
dual when SEREs are in questions? etc.) I believe your suggestion
raises these questions again.

In short, I am against having the operator not part of the syntax of
the parameterized property. And I think the syntax Cindy suggested
(with the extension you suggested previously of having possibly
multiple parameters) is a very nice one, making the parsing easy and
(by having the operator present in the syntax) making the semantics
clear .

Regards,
Dana.

On Mon, 20 Dec 2004 05:21:43 -0800, Erich Marschner <erichm@cadence.com> wrote:
> Cindy, Dana,
>
> If we are going to go this route, then we should make the syntax for the parameter declaration as consistent as possible with that of the existing forall statement, which requires braces around the Value_Set. This would give us the following:
>
> Existing forall:
>
> forall i in {<values>} : P(i)
>
> New extension:
>
> forall i in {<values>} : OP P(i)
>
> which amounts to saying that, at the top level of a property, the operator OP is optional, and if it is left off, then conjunction is the default.
>
> If this is acceptable, it would nicely unify the existing forall construct and the new parameterized property extension.
>
> I would also suggest two further refinements of the above:
>
> 1. make conjunction the default operator for a top-level forall applied to a property, but make disjunction the default operator for a top-level forall applied to a sequence.
>
> 2. allow the default(s) to apply at any level, not just the top level.
>
> Regards,
>
> Erich
>
> | -----Original Message-----
> | From: Dana Fisman [mailto:dana.fisman@gmail.com]
> | Sent: Monday, December 20, 2004 7:33 AM
> | To: Cindy Eisner
> | Cc: Erich Marschner; ieee-1850-extensions@eda.org
> | Subject: 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 08:20:22 2004