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

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.