Re: Proposal for Parameterized And/Or operators

Hi Erich,

It seems we are in agreement now. :-)

Regards,
Dana.

PS
I did not understand how the parameterized and/or operators can be
used to support what Tej has proposed.

On Mon, 20 Dec 2004 09:46:02 -0800, Erich Marschner <erichm@cadence.com> wrote:
> Hi Dana,
>
> Thanks for your comments. After reading this and thinking about it some more, I understand and agree, for the most part. I'd like to clarify some points.
>
> First, I should not that I didn't notice that Cindy's proposed syntax used 'for' instead of 'forall' until you pointed it out. What I noticed was the lack of braces around the value set. I would recommend that we stick to the same syntax for the value set as we have already for forall.
>
> Second, you haven't said, but I think it is the case that, 'forall' has special significance formally, i.e., that it represents the universal quantifier, which implies conjunction. So if we are going to allow the operator to be something other than conjunction, we must use a more general term: "for". This is fine with me; I just want to make sure the reason is clear.
>
> Third, after further thought, I realize that since a sequence can be promoted to a property, it may be ambiguous whether a (new, nested) for construct is applied to a sequence or to a (sequence that has been promoted to) a property, so defaulting the operator based on the operand type is not feasible.
>
> Fourth, I've also realized that defining a 'for(some)' top-level construct that applies to sequences, to parallel the 'forall' construct that applies to properties, would involve more change to the LRM than would be acceptable (probably another whole section), so I withdraw that suggestion also.
>
> So let me simply recommend that we refine Cindy's proposal slightly, to use the same syntax for the Value_Set (i.e., enclosed in braces) as is used in the forall construct.
>
> I would like to point out that the parameterized and/or properties are more general than the forall construct, and furthermore that they can be used to support what Tej has proposed (and without requiring replication), so I don't think there will be a need for both (hence the issue about using 'forall' for a separate purpose is moot). Also, I don't believe my suggestions in any way required revisiting the issue of duality; but that is also moot now since I've withdrawn the suggestions.
>
> I'll respond separately regarding your questions about the motivation for disjunction of a sequence.
>
> Regards,
>
> Erich
>
> | -----Original Message-----
> | From: Dana Fisman [mailto:dana.fisman@gmail.com]
> | Sent: Monday, December 20, 2004 11:20 AM
> | To: Erich Marschner
> | Cc: Cindy Eisner; ieee-1850-extensions@eda.org
> | Subject: 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 12:50:39 2004