[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, and is
believed to be clean.