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