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

Yes, I think John is right here.

If the antecedent is vacuously true, that means that covering it is not an interesting result, but does not necessarily mean that the consequent is uninteresting.

In the example below, there may be complex logic involving 'ack' and 'done' that must be verified for chip functionality to be correct.

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of ben cohen
Sent: Friday, October 15, 2010 8:44 AM
To: Havlicek John-R8AAAU
Cc: Little Scott-B11206; sv-ac@eda.org; Korchemny, Dmitry
Subject: Re: [sv-ac] Re: More on vacuity of property implies

John,
After more thoughts, I agree with you.
1) Vacuity implies coverage or not. A fail is a disaster that you need to know about. A valid pass implies coverage. Vacuity is only an issue when all/most passes are vacuous, meaning it was not really tested.
2) If I wanted a failed req to cause the consequent of the implies to be ignored, I should write the antecedent as a sequence:
property pComplex2;
(req) and ( ##2 rdy) implies
    (master_mode |-> (t4 ##0 ack) and (##[5:8] done));
endproperty : pComplex2
Ben
On Fri, Oct 15, 2010 at 8:00 AM, ben cohen <hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>> wrote:
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<mailto: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> [mailto: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<mailto: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<mailto: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<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.