overlapped implication vs logical AND. |-> vs. &&

[ljepson74]

When used in a coverpoint, what is the difference between overlapped implication and logical AND?

 

|-> vs. &&

 

   cp_test : cover property ( @(posedge clk) disable iff (!resetn)

      A |-> B );

 

   cp_test : cover property ( @(posedge clk) disable iff (!resetn)

      A && B );

 

?

 

A colleague asked me.  It seems to me they are the same and the logical AND is more readable.

[apfitch]

Hi,

  firstly that isn't a coverpoint, it's a cover property :-)

 

The difference between A |-> B and A && B is that implication also evaluates to true if A is false, i.e.

A |-> B is the same as (not A or (A and ) 

The standard says that the cover property statement will also report the number of vacuous passes (i.e. the case where  you cover A |-> B and A is false).

 

I guess the other difference is that the implication operator applies to sequences (which doesn't really affect your example as A and B are just sequences of length 1 in a sense). Whereas && won't work on a sequence, you'd have to use "and" or "intersect".

 

So I guess in this case of just testing logical values that have a sequence length of 1, && is more readable.

 

regards

Alan

[tudor.timi]

I don't think it's just readability. When you cover stuff like this I'd assume you don't want to see vacuous hits (when A is false); you want to see that you had A and B high at the same time. In any case, they're not the same.

[sri.cvcblr]

It is bad coding style and discouraged to use implication in cover property for the vacuity reason that Tudor has explained. This question often comes up and we now have it as part of our SV Quiz @ http://www.verifjobs.com 

 

We discuss this in our SVA book in the coding guidelines chapter and we are adding it as a rule to our upcoming DVRules-SVA product too!

 

Regards

Srini