Re: [sv-ac] More on vacuity of property implies

scott, all,

i typically follow your discussions from afar, but as a co-author of the
very first paper on vacuity [1], i feel a strong need to make one comment.
the view that scott takes here is reminiscent of the generalization of
antecedent failure that we addressed in [1]. and dana's paper that she
pointed you to previously discusses the cases where that generalization is
too general. so these two papers take roughly the opposite view on the
question scott raises.

i think that studying the existing work on vacuity (there are tens of paper
other than the two i discuss above -- search on google scholar) is
necessary. most probably you will find that one of the many existing
definitions is suitable for you. probably there is no need to reinvent the
wheel.

have fun,

cindy.

[1] Ilan Beer, Shoham Ben-David, Cindy Eisner, Yoav Rodeh: Efficient
Detection of Vacuity in ACTL Formulaas. CAV 1997: 279-290

From: Little Scott-B11206 <B11206@freescale.com>
To: <ben@systemverilog.us>, <sv-ac@eda.org>, "Korchemny, Dmitry"
            <dmitry.korchemny@intel.com>
Date: 13/10/2010 15:05
Subject: [sv-ac] More on vacuity of property implies
Sent by: owner-sv-ac@eda.org

Hi Ben:

I changed the subject line to be more clear about the topic of discussion.
See my comments below.

Thanks,
Scott

<snip>

Consider this variation:

property pComplex;

(req |-> ##2 rdy) implies
(master_mode |-> (t4 ##0 ack) and (##[5:8] done));
endproperty : pComplex

What is that saying?

       1) If req is false, then we don't care about the value of rdy @t2.
       What about master_mode, ack, and done?

This is the case where the differences between the proposed definitions for
implies1 and implies2 may become interesting.  If req is false and
master_mode is true then the antecedent of implies is vacuous and the
consequent is nonvacuous.  If we use implies1 the vacuity result for
implies would be nonvacuous.  If we use implies2 the vacuity result for
implies would be vacuous.  It seems to me that the result of implies2 is
what I want.  I would like to hear the opinions of others on this case and
maybe other potentially problematic cases.

<snip>

--
This message has been scanned for viruses and
dangerous content by 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.