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

Hi Ben:
 
The committee's intent was that the notions of outcome of evaluation and
vacuity of evaluation are independent.
 
If we consider only the pass/fail outcomes, then there are four
possibilities pairing outcome with either vacuous or
non-vacuous.
 
J.H.

________________________________

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben
cohen
Sent: Monday, February 16, 2009 3:56 PM
To: Korchemny, Dmitry
Cc: sv-ac@eda.org; Daniel.Mlynek@aldec.com.pl; Ajeetha Kumari;
Srinivasan Venkataramanan
Subject: Re: [sv-ac] RE: P1800-2009 : Mantis 0002578 comments


Dmitry,  
Sorry, but I fail to understand your answer that addresses the a#-# b
rather than the 
(not(a #-# b)). 
Are you saying that if a==0, you get a "vacuous failure".  I don't
believe the LRM addressed the concept of "vacuous failure". Can we then
clarify this as :
6.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, otherwise the evaluation will be vacuous
(vacuous fail). 




On Mon, Feb 16, 2009 at 8:52 AM, Korchemny, Dmitry
<dmitry.korchemny@intel.com> wrote:


	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 <http://www.mailscanner.info/>
, and is 
	believed to be clean. 



-- 
This message has been scanned for viruses and 
dangerous content by MailScanner <http://www.mailscanner.info/> , and is

believed to be clean. 

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