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

Hi Scott,

I think that what gets us to the this point where we ask “should we consider this (formula, model) pair a vacuous/nonvacuous given that one subformula is vacuous and another one is non-vacuius” is that we are seeking for a yes/no answer. We can easily solve this if we introduce the notion of being vacuous with respect to a sub-formula. So a formula can be vacuous with respect to one sub-formula and non-vacuous with respect to another. Then one can say that a formula \phi is vacuous if there exists a sub-formula \psi of it such that is vacuous with respect to \psi. (This is standard in literature on vacuity.) A good tool can then not only give a vacuous/non-vacuous report, but also point to a sub-formula (or a set of sub-formulas) the formula is vacuous with respect to.

Best,
Dana

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Little Scott-B11206
Sent: Wednesday, October 13, 2010 3:05 PM
To: ben@systemverilog.us; sv-ac@eda.org; Korchemny, Dmitry
Subject: [sv-ac] More on vacuity of property implies

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