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
------------------------------------------------------------