RE: Proposal for Parameterized And/Or operators

Dana,

I would argue that such an "automatic reduction" is no less a tool implementation choice than the implementation choices I mentioned - and for 'cover', where the goal is to get detailed information about what has been tested, rather than to verify the design, the tool implementation choices I suggested might be preferable for a given implementor. Also, the language will be simpler if we avoid "multiplying entities" unnecessarily, to quote Occam. If the issue is indeed a tool implementation choice - whether to optimize a parameterized operator, or whether to elaborate it to collect more information - then let's leave that decision to the tool.

Perhaps others on the working group have an opinion about this?

Regards,

Erich

| -----Original Message-----
| From: Dana Fisman [mailto:dana.fisman@gmail.com]
| Sent: Tuesday, December 21, 2004 3:48 AM
| To: Erich Marschner
| Cc: Cindy Eisner; ieee-1850-extensions@eda.org
| Subject: Re: Proposal for Parameterized And/Or operators
|
| Erich,
|
| I still think we cannot use the parameterized-or to do what
| you want for cover. You are relying too much on the
| implementation, which may vary from tool to tool. Note for
| example, that you are disallowing an automatic reduction that
| replaces (for j in {0..15}: | {data=j}) with
| (true) in cases where indeed data can only assume values in 0..15.
| This is unacceptable – since semantically they are the same.
| If you have a different replicator for the directive, this
| problem does not occur.
|
| Regards,
| Dana.
|
|
|
| On Mon, 20 Dec 2004 13:43:23 -0800, Erich Marschner
| <erichm@cadence.com> wrote:
| > Hi Dana,
| >
| > I understand your point, but I would argue that your key
| assumption is false.
| >
| > First, it would rarely be the case that the range given for
| the parameter is the entire range of the data value it is
| being compared to. For example, I may have an address value
| whose range is 0..2^32-1, for which I might write the
| following cover directives:
| >
| > A_0: cover {addr==0};
| > A_1: cover for i in {1:4095} {addr==i};
| > A_2: cover for j in {4096:65535} {addr==j};
| > A_3: cover {65536 <= addr};
| >
| > This effectively creates 4 "bins" that we want to cover,
| corresponding to ranges of address values that have
| particular meanings - e.g., address==0 is the null address,
| perhaps addresses in the range up to 4K are in ROM, and
| addresses above that, up to 2^16-1, are reserved for some
| special usage. In doing data coverage, we want to know if
| any of the addresses in a given bin have been hit, so the
| 'or' semantics is exactly what we want here.
| >
| > The first level of coverage only tells us whether or not we
| have hit some bin. Here, the PSL semantics of cover
| directives suffice. However, in production verification
| flows, users want to know not only whether, but how many
| times, a given coverage bin has been hit. So the first and
| most obvious addition for PSL implementors is to count how
| many times a cover directive has been satisfied, rather than
| just registering yes or no.
| >
| > Beyond that, if we have defined parameters for cover
| directives, the next obvious thing to do would be to record
| the parameter values for which the cover directive was
| satisfied. Doing this would allow an implementation to track
| individual values within a bin, and chart the distribution of
| those values over the range. So even if a cover directive
| specified the entire possible range of values for a variable
| (creating one bin for the entire range), thereby making the
| directive equivalent to "cover {True}", a tool could use the
| parameter values to give more detailed information about
| *how* the cover directive was satisfied in a given cycle.
| This goes beyond PSL cover directive semantics, but it is
| entirely consistent with the disjunction semantics that I
| proposed - it simply provides more detail.
| >
| > So the key point here is that we are NOT assuming that the
| range specified for a cover directive is all-inclusive, i.e.,
| that by definition a parameterized cover directive (with
| disjunction semantics) will reduce to cover {True}. Instead,
| this proposed capability assumes a typical use model in which
| different cover statements are provided for different subsets
| or subranges of the values of a variable, and furthermore
| that tools may elect to use the parameter values that satisfy
| a cover directive to provide more detail.
| >
| > Regards,
| >
| > Erich
| >
| > | -----Original Message-----
| > | From: Dana Fisman [mailto:dana.fisman@gmail.com]
| > | Sent: Monday, December 20, 2004 4:02 PM
| > | To: Erich Marschner
| > | Cc: Cindy Eisner; ieee-1850-extensions@eda.org
| > | Subject: Re: Proposal for Parameterized And/Or operators
| > |
| > | Erich,
| > |
| > | I guess I understand your motivation, but I don't think
| the details
| > | work.
| > |
| > | > cover for i in {0:4095} : |({data==i}); ...
| > | >
| > | > is essentially shorthand for
| > | >
| > | > cover {data==0};
| > | > cover {data==1};
| > | > cover {data==2};
| > | > ...
| > | > cover {data==4095};
| > |
| > | I disagree.
| > |
| > | cover for i in {0:4095} : |({data==i});
| > |
| > | is equivalent to
| > |
| > | cover {data==0} | {data==1} | {data==2} | ... | {data==4095}
| > |
| > | which is in turn
| > |
| > | cover {true} assuming data can only assume values
| > | between 0 to 4095.
| > |
| > | (the dual of what you noted. i.e. that with the conjunction
| > | semantics we get cover{false}).
| > |
| > | This is why I still think we need a replication operator
| that can be
| > | applied to directive. So that for example
| > |
| > | > forall i in {0:4095} : cover {data==i};
| > |
| > | will be equivalent to 4096 cover statements (as above).
| > |
| > | Regards,
| > | Dana.
| > |
| > |
| > | On Mon, 20 Dec 2004 10:16:16 -0800, Erich Marschner
| > | <erichm@cadence.com> wrote:
| > | > 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 Tue Dec 21 06:26:20 2004