RE: [sv-ac] 1381 vacuous evaluation

Proposal says:
OR:
"an evaluation attempt of a property of the form property_exp1 or
property_exp2 is non-vacuous iff either the underlying evaluation attempt of
property_exp1 is non-vacuous or the underlying evaluation attempt of
property_exp2 is non-vacuous"
|->
 "an evaluation attempt of a property of the form seq_expr |-> prop_expr is
non-vacuous iff there is a success match of seq_expr, and the evaluation of
prop_expression starting at that point is nonvacuous"
 
In my case a |-> b has vacuous evaluation,
but c|->d has non-vacuous evaluation
 
From both above I can tell that evaluation of all my property (a|->b) or
(c|->d) is non-vacuous.
 
Where am I wrong?
 
 
 
DANiel

  _____  

From: Bustan, Doron [mailto:doron.bustan@intel.com] 
Sent: Thursday, January 03, 2008 7:18 AM
To: danielm; sv-ac@server.eda-stds.org
Subject: RE: [sv-ac] 1381 vacuous evaluation



Hi Daniel,

 

I think you are wrong. 1381 defines your example as vacuous.

 

Doron

 

  _____  

From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
Behalf Of danielm
Sent: Wednesday, January 02, 2008 2:42 PM
To: sv-ac@server.eda-stds.org
Subject: [sv-ac] 1381 vacuous evaluation

 


assert property (@(posedge clk) (a|->b) or (c|->d));
where:
a=0, b=0, c=1, d=0;

According to rules from 1381 above assertion should have NON-VACUOUS PASS
(LHS of or operator has vacuous evaluation, while RHS is failing). IMHO more
sensible result for this would be Vacuous Pass - am I missing something?

 



DANiel

---------------------------------------------------------------------

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

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