RE: [sv-ac] 1381 vacuous evaluation

Hi Daniel,

 

Sorry I missed the c=1,

 

Why do you think that vacuous pass is more sensible?

 

I can imagine a system where in every cycle either a or c are 0 and
still nothing wrong with it nor with the assertion. 

 

 

Doron

 

 

 

________________________________

From: danielm [mailto:danielm@aldec.com.pl] 
Sent: Thursday, January 03, 2008 10:01 AM
To: Bustan, Doron; sv-ac@server.eda-stds.org
Subject: 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 MailScanner <http://www.mailscanner.info/> , and is

believed to be clean. 

---------------------------------------------------------------------
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.