RE: [sv-ac] 1381 vacuous evaluation

Thanks Doron,
 
Why do you think that vacuous pass is more sensible?

It was just my impression.
IMHO my property doesn't PASS NON VACUOUSLY (it passes vacuously) because
1st sub-property passes vacuously and the 2nd fails - so  how we can tell
that whole property passes non-vacuosly if none of the subproperties had
passed non-vacuously?
 
But rules from 1381 clearly says that this is non-vacuous pass.
 
This is why i'm a little unhappy with the 1381.
 
But OK - I can live with that;)
 
 
DANiel

 
  _____  

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