Re: [sv-ac] RE: Issue 2578: Vacuity definition

 There is another more important issue: What do we really want from the
implies operator?
The '09 definition is
(p1 implies p2) is ((not p1) or p2)
With the update that we approved, I believe that the meaning is more like
p1 |-> p2 // with the |-> working on properties, and p1 starts at the same
time as p2,
In other words,
(p1 implies p2) is more like (p1 and p2), but
if p1 fails, then (p1 implies p2) is vacuous
That's a major redefinition.

Here's what's in the new update, and a table used as an example.
z) An evaluation attempt of a property of the form property_expr1 implies
property_expr2 is nonvacuous if, and only if,
the underlying evaluation attempt of property_expr1 is true,
the underlying evaluation attempt of property_expr1 is nonvacuous,
and the underlying evaluation attempt of property_expr2 is nonvacuous

(a |-> b) implies (c -> d);
 a b c d
 0 x 0 x p1==vacuous, p2==vacuous (p1 implies p2) is vacuous
 0 x 1 0 p1==vacuous, p2==FALSE (p1 implies p2) is vacuous
 0 x 1 1 p1==vacuous, p2==TRUE (p1 implies p2) is vacuous
 1 0 0 x p1==FALSE, p2==vacuous (p1 implies p2) is vacuous
 1 0 1 0 p1==FALSE, p2==FALSE (p1 implies p2) is vacuous
 1 0 1 1 p1==FALSE, p2==TRUE (p1 implies p2) is vacuous
-------------------NONVACUOUS CONDITIONS -------------------------------
 1 1 1 0 p1==TRUE, p2==FALSE (p1 implies p2) is FALSE
 1 1 1 1 p1==TRUE, p2==TRUE (p1 implies p2) is TRUE

With Ed's comments:
the underlying evaluation attempt of property_expr1 is true and the
underlying evaluation attempt of property_expr1 or property_expr2 is
nonvacuous.
[Ben] but 1st part of sentence says "property_expr1 is true",
2nd part says "property_expr1 or property_expr2 is nonvacuous"
The ""property_expr1" is not needed because it must be true from 1st part.
True?

I think we have the same thing about this redefinition.
p1 p2 (p1 implies p2)
0 0 vacuous
0 1 vacuous
1 0 fail
1 1 pass
1 V vacuous.

I like this definition of the implies operator as it is more in line with
the |-> operator.
But that is a big change, non-backward compatible.
Ben

On Thu, Aug 11, 2011 at 8:22 AM, Little Scott-B11206
<B11206@freescale.com>wrote:

> Hi Ed, Dmitry:****
>
> ** **
>
> Okay, that is fine. How about the following then…****
>
> ** **
>
> the underlying evaluation attempt of property_expr1 is true and the
> underlying evaluation attempt of property_expr1 or property_expr2 is
> nonvacuous.****
>
> ** **
>
> Thanks,****
>
> Scott****
>
> ** **
>
> *From:* Eduard Cerny [mailto:Eduard.Cerny@synopsys.com]
> *Sent:* Thursday, August 11, 2011 10:19 AM
> *To:* Korchemny, Dmitry; Little Scott-B11206; sv-ac@eda-stds.org
>
> *Subject:* RE: Issue 2578: Vacuity definition****
>
> ** **
>
> I tend to agree with Dmitry.****
>
> ** **
>
> ed****
>
> ** **
>
> ** **
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Korchemny,
> Dmitry
> *Sent:* Thursday, August 11, 2011 11:15 AM
> *To:* Little Scott-B11206; sv-ac@eda-stds.org
> *Subject:* [sv-ac] RE: Issue 2578: Vacuity definition****
>
> ** **
>
> The LRM essentially says that the expression is non-vacuous if *some* of
> its subexpressions are non-vacuous. If you want to change this, we need to
> update all the definitions accordingly. Of course, there are different
> approaches to the vacuity definition.****
>
> ** **
>
> Thanks,****
>
> Dmitry****
>
> ** **
>
> *From:* Little Scott-B11206 [mailto:B11206@freescale.com]
> *Sent:* Thursday, August 11, 2011 18:08
> *To:* Korchemny, Dmitry; sv-ac@eda-stds.org
> *Subject:* RE: Issue 2578: Vacuity definition****
>
> ** **
>
> Hi Dmitry:****
>
> ** **
>
> That is correct. The LRM isn’t consistent, and I don’t think we can make
> it so.****
>
> ** **
>
> Thanks,****
>
> Scott****
>
> ** **
>
> *From:* Korchemny, Dmitry [mailto:dmitry.korchemny@intel.com]
> *Sent:* Thursday, August 11, 2011 10:04 AM
> *To:* Little Scott-B11206; sv-ac@eda-stds.org
> *Subject:* RE: Issue 2578: Vacuity definition****
>
> ** **
>
> Hi Scott,****
>
> ** **
>
> But your concept is not consistent with the LRM. E.g.,****
>
> ** **
>
> f) An evaluation attempt of a property of the form property_expr1 and
> property_expr2 is nonvacuous****
>
> if, and only if, either the underlying evaluation attempt of property_expr1
> is nonvacuous *or* the****
>
> underlying evaluation attempt of property_expr2 is nonvacuous.****
>
> ** **
>
> Regards,****
>
> Dmitry****
>
> ** **
>
> *From:* Little Scott-B11206 [mailto:B11206@freescale.com]
> *Sent:* Thursday, August 11, 2011 16:18
> *To:* Korchemny, Dmitry; sv-ac@eda-stds.org
> *Subject:* RE: Issue 2578: Vacuity definition****
>
> ** **
>
> Hi Dmitry:****
>
> ** **
>
> Can you provide some justification for why you think the given definition
> doesn’t work? To me this is one of those areas where sometimes you want the
> definition to be one way and sometimes you want it to be the other way. It
> sort of depends on how you look at vacuity… ****
>
> ** **
>
> I personally prefer the way it is currently written as I feel it is a
> higher bar for something to be declared nonvacuous. What you suggest allows
> the property in the antecedent to be vacuous while the overall property
> could be nonvacuous. That definition feels a bit weak to me. When I get a
> result of nonvacuous I want to know that all of the constituent parts also
> have nonvacuous evaluations.****
>
> ** **
>
> Thanks,****
>
> Scott****
>
> ** **
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Korchemny,
> Dmitry
> *Sent:* Thursday, August 11, 2011 7:42 AM
> *To:* sv-ac@eda-stds.org
> *Subject:* [sv-ac] Issue 2578: Vacuity definition****
>
> ** **
>
> Hi all,****
>
> ** **
>
> I am sorry to reopen the discussion about a resolved issue. Should have
> done it at the last meeting. There are two problems that I would like to
> discuss.****
>
> ** **
>
> **1. **The following vacuity conditions for implies operator were
> suggested:****
>
> * If the antecedent is false, then (P1 implies P2) should be vacuous.****
>
> * Also, if the antecedent is vacuous, then (P1 implies P2) is vacuous.****
>
> * Also, if the antecedent is nonvacuous true, then (P1 implies P2) is
> nonvacuous if consequent is nonvacuous****
>
> ** **
>
> My question is why the second condition has been added. If P1 is vacuously
> true, it does not mean that P1 implies P2 is vacuous.****
>
> ** **
>
> **2. **Whatever the reply to my first question be, F.5.3.3 should be
> updated accordingly.****
>
> ** **
>
> Thanks,****
>
> Dmitry****
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
> --
> This message has been scanned for viruses and
> dangerous content by *MailScanner* <http://www.mailscanner.info/>, and is
> believed to be clean. ****
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.****
>
> ---------------------------------------------------------------------
> Intel Israel (74) Limited
>
> This e-mail and any attachments may contain confidential material for
> the sole use of the intended recipient(s). Any review or distribution
> by others is strictly prohibited. If you are not the intended
> recipient, please contact the sender and delete all copies.
> --
> 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.