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

So what rewrites you would like to see?
Also, will (p1 implies p2) be same as ((not p1) or p2), or more like
the implication operator where a false in the antecedent causes the (p1
implies p2) to be vacuous.
The latter is what I want to see.
I am open to suggestions on the rewrites.
BTW, I won't be able to make the Tuesday meeting.
Ben

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

> Hi Ben:****
>
> ** **
>
> See my response below.****
>
> ** **
>
> Thanks,****
>
> Scott****
>
> ** **
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Thursday, August 11, 2011 11:10 AM
> *To:* Little Scott-B11206
> *Cc:* Eduard Cerny; Korchemny, Dmitry; sv-ac@eda-stds.org
> *Subject:* Re: [sv-ac] RE: Issue 2578: Vacuity definition****
>
> ** **
>
> There is another more important issue: What do we really want from the
> implies operator? ****
>
> ** **
>
> [SL]: I would like something a bit more sane than is in the current LRM
> although I also believe that the definitions in the LRM aren’t usable in
> practice. I would be in favor of a major overhaul of all definitions if we
> knew what that overhaul should look like. My impression based on previous
> discussions is that we don’t.****
>
> ****
>
> 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***
> *
>
> [SL] There isn’t enough information in the above line to determine the
> result. The antecedent c has a successful match, so the question is does
> the evaluation of d have a vacuous or nonvacuous result? See my comment
> about a vacuous fail below. The information needed in the table is truth
> value and vacuity result for p1 and vacuity result for p2. The truth value
> of p2 is irrelevant when computing vacuity based on the above definition
> (although if c doesn’t match you know the vacuity result).****
>
> 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? ****
>
> ** **
>
> [SL] Not true. It is possible for a property to evaluate to true and be
> vacuous or false and vacuous. Vacuity and the result of the evaluation are
> two different things. For instance, let’s say I have a property not(p |->
> q) then if p doesn’t match I have a property that evaluates to false and is
> vacuous. If I remove the not() then I have a property that evaluates to
> true and is vacuous.****
>
> ** **
>
> 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.****
>
> ** **
>
> [SL] I agree and prefer the definition in the current version of the
> proposal. However, Dmitry points out that it isn’t consistent with the rest
> of the LRM (e.g., the definitions for ‘and’ and ‘until’). We should
> probably be consistent with what is there as I don’t think it is prudent to
> change those definitions as well.****
>
> ****
>
> 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.