[sv-ac] RE: P1800-2009 : Mantis 0002578 comments

Hi Ben,

According to this LRM definition, the failure may also be vacuous: this assertion fails in a "non-interesting" way - because a was false and not because b did not happen. Consider the following statement:

cover property (@(posedge clk) start #-# cond);

saying that we want to check cond when start happens. If start hasn't happened - there is no attempt, if it has and cond did not happen - we failed to cover it.

Note that a #-# b is not (a |-> not b).

Dmitry

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Saturday, February 14, 2009 7:05 AM
To: sv-ac@eda.org
Cc: Daniel.Mlynek@aldec.com.pl; Korchemny, Dmitry; Ajeetha Kumari; Srinivasan Venkataramanan
Subject: P1800-2009 : Mantis 0002578 comments

Dmitry
The issue is the LRM
16.15.8 Nonvacuous evaluations
d) An evaluation attempt of a property of the form not property_expr is nonvacuous if, and only if, the underlying evaluation attempt of property_expr is nonvacuous.

Question, when is it ever vacuous?
 a |-> b --> Vacuous success if a == 0. The "not" will negate it and hence:
not (a |-> b) --> when"a == 0" is a FAILURE

But logically, the intent here is as follows:
not (a |-> b) should mean "never the case that (if a==1, b==1)", and if a==0, we don't care".  But this is not what "not (a |-> b)" says.  It says "never the case that (if a==1, b==1)", and if a==0, It's a ERROR".c

Answers to Daniel Mlynek:
 <1. rule for or operator e)Results should be also vacuous if both prop1 and prop2 are vacuous.

I'm assuming than if prop1 is non-vacuous pass and prop2 is vacuous pass then result is nonvacuous>

Ben: But either one or the other satisfy the requirement.  Doesn't that imply both? It's redundant.


<4. Operator "not" also introduces ambiguity (for definition see below) - what should happen if property under not passes vacuously? We are geting a vacuous fail ?
An evaluation attempt of a property of the form not property_expr is nonvacuous if, and only if, the underlying evaluation attempt of property_expr is nonvacuous.>

Ben: Agree with the ambiguity.  The way the LRM stands, I don't see how the not operator on a property can produce a vacuous result.  In "16.13.16 Case", LRM brings the concept of true vacuous in "...and the evaluation of the case property statement from that start point succeeds and returns true (vacuously)." Thus, the not of a property that is vacuous, which is true vacuous, must be FALSE.   Consider the property expression:  a |-> b.  If "a==0", property expression is vacuous.  But "not(a |-> b)" sates never the case that if "a" then "b".  What happens if "a==0"? we should not really care, and the not of a vacuous property should  result in a vacuous result.

The  statement "An evaluation attempt of a property of the form not property_expr is nonvacuous if, and only if, the underlying evaluation attempt of property_expr is nonvacuous." Seems to imply that result of a not of vacuous property is vacuous.  But vacuous is also considered as "true", thus not of true is false.

---------------------------------------------------------------------
Intel Israel (74) Limited

This e-mail and any attachments may contain confidential material for
the sole use of the intended recipient(s). Any review or distribution
by others is strictly prohibited. If you are not the intended
recipient, please contact the sender and delete all copies.

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.