RE: Proposal for Parameterized And/Or operators

Hi Erich,

I do agree with you that in presence parameterized And/Or operator,
there is no need for replicator on directive. In proposing replicator
on directive, since my intention was not to force tools to replicate the

directive multiple times (which can be done using %for or for-generate
of HDL,
if user desires), but rather have them report the replicator index value
for
which directive property holds/fails, it can be done using parameterized
And/Or
operator. As for reporting the parameter value, that should be left to
the tool
if and how they want to present that information.

My only concern with parameterized property And/Or replacing forall in
LRM 1.1 is
can these operands take non-Boolean operands in simple subset? If yes,
it violates
simple subset restriction on property And/Or. If no, then it does not
cover forall
as far as simple subset is concerned.

Tej

> -----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:43 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,
>
> 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 Mon Dec 20 20:10:39 2004