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

John,
Interesting debate..
[John] The reason for this is that falsity of req ensures that the
antecedent of “implies” is true,
[Ben] Question: How does formal verification consider vacuity (true
vacuously) in an antecedent?
I was considering the case of a vacuously true antecedent that represents
the supposition of a property. If that supposition is vacuous, whether it
be True vacuous or False vacuous (e.g., *not (*true vacuous), then there is
no need to verify the consequent, or the proof.
I understand that T/F and vacuity are orthogonal, but I still still vacuity
as non-essential cases.
Ben

On Fri, Oct 15, 2010 at 7:17 AM, Havlicek John-R8AAAU
<r8aaau@freescale.com>wrote:

> Hi Ben:
>
>
>
> I disagree with your analysis. If req is false and master_mode is true,
> then
>
>
>
> (t4 ##0 ack) and (##[5:8] done)
>
>
>
> [i.e., the consequent of the consequent] must be true in order for
> pComplex itself to be true. The reason for this is that falsity of req
> ensures that the antecedent of “implies” is true, and truth of master_mode
> obligates truth of the consequent of the consequent.
>
>
>
> A formal tool will explore this scenario.
>
>
>
> These circumstances illustrate that it is the passing/failing behavior
> antecedents and consequents that is of first importance, while vacuity is of
> second importance.
>
>
>
> J.H.
>
>
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *ben
> cohen
> *Sent:* Wednesday, October 13, 2010 10:55 AM
> *To:* Little Scott-B11206
>
> *Cc:* sv-ac@eda.org; Korchemny, Dmitry
> *Subject:* [sv-ac] Re: More on vacuity of property implies
>
>
>
> Scott,
>
> In formal verification the antecedent is considered as a "supposition" and
> the consequent is interpreted as a "proof".
>
> Thus, for
>
> *property* pComplex;
> (req |-> ##2 rdy) *implies **
> *(master_mode |-> (t4 ##0 ack) *and* (##[5:8] done));
> *endproperty* : pComplex
>
> *<If req is false and master_mode is true then the antecedent of implies
> is vacuous and the consequent is nonvacuous. >*
>
> In this case, the supposition is vacuous, thus there is no need to evaluate
> the proof with those input stimuli.
>
> <* 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 agree, we need implies2 since, in this example, when the antecedent that
> represents the supposition is vacuous there is no need to verify the
> consequent, or the proof. With the implies1, we're imposing a proof on
> something that needs none.
>
>
>
> Ben
>
>
>
> On Wed, Oct 13, 2010 at 6:04 AM, Little Scott-B11206 <B11206@freescale.com>
> wrote:
>
> 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.