RE: Proposal for Parameterized And/Or operators

Dana,

I made a mistake in the final examples I gave earlier. I meant:

| The proposed syntax could also be applied to the LHS or RHS
| of a suffix implication operator, e.g.,
|
| for i in {0:3} : |({a[*i]}) |=> for j in {0:3} : |({b[*j]}) <== corrected
|
| One question that remains to be addressed is the scope of the
| 'for' parameter - does it only extend over the property or
| sequence to which it applies, or does it extend beyond that?
| For example, would it be possible to write
|
| for i in {0:3} : |({a[*i]}) |=> for j in {4:7} : |({b[*j-i]}) <== corrected
|
| so that the number of b's is a function of the number of a's?

Regards,

Erich

| -----Original Message-----
| From: owner-ieee-1850-extensions@eda.org
| [mailto:owner-ieee-1850-extensions@eda.org] On Behalf Of
| Erich Marschner
| Sent: Monday, December 20, 2004 1:16 PM
| To: dana.fisman@weizmann.ac.il
| Cc: Cindy Eisner; ieee-1850-extensions@eda.org
| Subject: RE: Proposal for Parameterized And/Or operators
|
| Hi Dana,
|
| This is the separate response I mentioned regarding the
| motivation for disjunction of sequences.
|
| | 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?).
|
| The notion of disjunction on sequences came from the idea of
| using a forall-like parameter in a cover directive, to say
| "cover any sequence that includes a value in the range of the
| parameter" - e.g.,
|
| cover forall i in {0:4095} : {data==i};
|
| However, the fact that forall is hardwired to mean
| conjunction makes this meaningless - clearly the conjunction
| (either & or &&) of the sequences implied by the above cannot
| hold, because data cannot take on any more than one value in
| any given cycle. What we want is the disjunction of the
| above sequences, i.e., to cover the case where any one of the
| sequences occurs. This is what originally caused to me to
| suggest a "for some" operator, which led to the discussion of
| parameterized and/or operators on properties and sequences.
|
| With the proposed parameterized and/or operators, we can say instead
|
| cover for i in {0:4095} : |({data==i});
|
| (It is not clear to me that we need the parentheses around
| {data==i} in addition to the braces, but I'll leave that to
| be discussed later.)
|
| This is essentially shorthand for
|
| cover {data==0};
| cover {data==1};
| cover {data==2};
| ...
| cover {data==4095};
|
| Note that disjunction is in some sense a natural semantics
| for cover directives (and sequences), whereas conjunction is
| a natural semantics for assert directives (and properties).
| For the cover directive, which detects a sequence that may or
| may not occur in a given verification run, we want to detect
| ANY (a_0 or a_1 or ... a_n) occurrence of any form of the
| parameterized sequence - but for assert directives, which are
| expected to hold at every cycle in every verification run, we
| want to require EVERY (a_0 and a_1 and ... a_n) form of the
| parameterized property to hold.
|
| Note also that, if we can say the above, then this is hardly
| different from applying forall to a directive, e.g.,
|
| forall i in {0:4095} : cover {data==i};
|
| In fact, since 'forall' suggests conjunction, it seems odd to
| apply it to cover directives, which as I've just mentioned
| are not all required to hold at any given time; the semantic
| sense of 'cover' is more disjunction-oriented. So I believe
| allowing disjunction on sequences, using the syntax that has
| been proposed, gives us the ability to 'apply forall to
| directives' as has been requested, but with a more natural semantics.
|
| The proposed syntax could also be applied to the LHS or RHS
| of a suffix implication operator, e.g.,
|
| for i in {0:3} : {a[*i]} |=> for j in {4:7} : {b[*j]}
|
| One question that remains to be addressed is the scope of the
| 'for' parameter - does it only extend over the property or
| sequence to which it applies, or does it extend beyond that?
| For example, would it be possible to write
|
| for i in {0:3} : {a[*i]} |=> for j in {4:7} : {b[*j-i]}
|
| so that the number of b's is a function of the number of a's?
| At the very least, we would need the value of the parameter
| to be reported as part of any message associated with an
| assert or cover directive.
|
| Regards,
|
| Erich
|
|
|
|
Received on Mon Dec 20 11:06:40 2004