RE: forall and cover

Hi Johan,

Looks like we are in agreement with the expected semantics and what each type of verification engine would do. Thanks.

So, the only question is: What is the issue? Is it there a question of whether forall cover implies an OR'ing of the replicated covers? Again, I think you and I are in agreement, that it should not.

-Steve Bailey

> -----Original Message-----
> From: owner-ieee-1850-extensions@eda.org
> [mailto:owner-ieee-1850-extensions@eda.org] On Behalf Of
> Johan Mårtensson
> Sent: Wednesday, December 22, 2004 1:29 PM
> To: ieee-1850-extensions@eda.org
> Subject: Re: forall and cover
>
> Steve,
>
> I wrote this from the perspective of static verification where 'cover'
> is used mainly for asking the question whether a sequence can
> occur at all. My point can be expressed in this way: A forall
> on the directive level is the same as directive replication so a
>
> forall i in {0..3}: cover {a;b(i)};
>
> is the same as
>
> cover {a;b(0)};
> cover {a;b(1)};
> cover {a;b(2)};
> cover {a;b(3)};
>
> This is satisfied for a design if for each of the covers
> there is at least one possible run of the design in which the
> respective sequence occurs. There need not exist one single
> possible run satisfying all of them at once. This cannot be
> expressed by a single cover directive.
> Because a single cover is satisfied exactly in the case where
> there is at least one possible run that satisfies the
> sequence of the cover. This means that you are going to need
> some kind of replication mechanism on the cover level.
>
> The case is different for the assert directive
>
> assert {a;b(0)};
> assert {a;b(1)};
> assert {a;b(2)};
> assert {a;b(3)};
>
> These are satisfied for a design if all of them are true for
> all possible runs of the system. This means that from a
> semantical point of view we could as well write (with
> parameterized and)
>
> assert for i in {0..3}: and({a;b(i)});
>
> I agree that for simulation you would like to know more than
> just whether a sequence can occur or not. You want to count
> occurrences and for example, but I also agree with Cindy that
> this is not something that should be defined by us. It is
> rather something a dynamic tool can choose to report or not.
>
> Best Regards, Johan M
>
>
> On Wed, Dec 22, 2004 at 08:02:27AM -0800, Bailey, Stephen wrote:
> > All,
> >
> > I'll stick to the informal description as I've been in
> marketing too
> > long and the formal math hurts my head ;-)
> >
> > > A way to explain this informally is that a directive
> level forall on
> > > a cover directive instructs the tool to check if there is
> for every
> > > instantiation of the variable a possible run in which the sere is
> > > covered. This means that possibly different runs are
> required for
> > > different instances of the cover directive. No operator inside a
> > > cover directive can achieve this. A single cover
> directive is either
> > > (entirely) satisfied in a some single run or not at all.
> >
> > What is of interest to the user is whether or not all of
> his "bins" have been covered, not just entire directive, and
> that a user may have coverage thresholds that are relevant to
> them. For them, it is not enough to know that the "typical"
> range was hit once. They may want to know that the typical
> range was hit some statistically significant number of times
> to provide a relative high level of assurance that it wasn't
> the same value in the typical range being hit each time.
> >
> > Since the idea is to create different "bins" for each
> forall generated/replicated cover, I guess the OR semantics
> doesn't have much meaning as it says a single bin is created
> that is incremented each time one of the covers is "hit". If
> that were the only information that a tool collected, then it
> wouldn't be very useful. However, practically, the tool is
> likely to aggregate (or provide the user the option to
> aggregate) the coverage of all bins up to the forall directive level.
> >
> > So, if your point is that forall at the directive level is
> more like an HDL generate than a single property which must
> hold or not (it isn't the sum or product of the parts, it is
> a convenient way of generating the parts), then I would agree.
> >
> > -Steve Bailey
> >
> > > With directive level forall on an assert directive the tool is
> > > instructed to check whether for all instantiations and
> for all runs
> > > the property is satisfied, and that is the same as to
> check whether
> > > for all runs the corresponding conjunction is satisfied.
> > >
> > > Best Regards, Johan M
> > >
> > > On Tue, Dec 21, 2004 at 06:26:12AM -0800, Erich Marschner wrote:
> > > > 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
> > > > | > | >
> > > > | > |
> > > > | > |
> > > > | >
> > > > |
> > > > |
> > >
> > > --
> > > ------------------------------------------------------------
> > > Johan Martensson, PhD Office: +46 31 7451913
> > > R&D Mobile: +46 703749681
> > > Safelogic AB Fax: +46 31 7451939
> > > Arvid Hedvalls Backe 4 johan.martensson@safelogic.se
> > > SE-411 33 Gothenburg, SWEDEN
> > > PGP key ID A8857A60
> > > www.safelogic.se
> > > ------------------------------------------------------------
> > >
> > > --
> > > ------------------------------------------------------------
> > > Johan Martensson, PhD Office: +46 31 7451913
> > > R&D Mobile: +46 703749681
> > > Safelogic AB Fax: +46 31 7451939
> > > Arvid Hedvalls Backe 4 johan.martensson@safelogic.se
> > > SE-411 33 Gothenburg, SWEDEN
> > > PGP key ID A8857A60
> > > www.safelogic.se
> > > ------------------------------------------------------------
> > >
> > >
>
> --
> ------------------------------------------------------------
> Johan Martensson, PhD Office: +46 31 7451913
> R&D Mobile: +46 703749681
> Safelogic AB Fax: +46 31 7451939
> Arvid Hedvalls Backe 4 johan.martensson@safelogic.se
> SE-411 33 Gothenburg, SWEDEN
> PGP key ID A8857A60
> www.safelogic.se
> ------------------------------------------------------------
>
>
Received on Wed Dec 22 15:50:49 2004