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 13:02:02 2004