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

Scott,
Lots of good work with that table! Here's a 1st cut at my reactions.
the underlying evaluation attempt of property_expr1 is true
and the underlying evaluation attempt of property_expr1 or property_expr2
is nonvacuous.
1 = ((not p) or q)
2 = p |-> q (in this case column p we interpret 1 as a matching sequence
    and 0 as not a matching sequence the vacuity information is ignored)
3 = definition in current proposal
4 = definition in this e-mail
 Prop=(a|->b implies c|->d);
p q 1 2 3 4 Evaluation
0,V 0,V V V V V tv --
0,V 0,N N V V V tv OK
0,N 0,V N V V V tv OK
0,N 0,N N V V V tv OK
0,V 1,V V V V V tv OK
0,V 1,N N V V V tv OK
0,N 1,V N V V V tv OK
0,N 1,N N V V V tv OK
1,V 0,V V V V V fv OK
1,V 0,N N N V N f <<- CASE A: with 4, if antecedent is 1V, and
                           consequent is 0N property is nonvacuous fail.
                           With 3, property is vacuous fail
1,N 1,V N V V N t <<- CASE B: with 4, if antecedent is 1V, and
                           consequent is 0N property is nonvacuous true.
                           With 3, property is vacuous true
1,N 0,V N V V N f <<- CASE C: with 4, if antecedent is 1N, and
                           consequent is 0V property is nonvacuous fail.
                           With 3, property is vacuous fail
1,V 1,N N N V N t <<- CASE D: with 4, if antecedent is 1N, and
                           consequent is 1N property is nonvacuous true.
                           With 3, property is vacuous true
1,N 0,N N N N N f OK
1,V 1,V V V V V t OK
1,N 1,N N N N N t OK

Consider the property below
(get_cache_status && cache_entry[addr]==INVALID |->
     request_main_mem_bus |-> main_mem_bus_ready) implies
(main_mem_bus_ready |-> ##[1:5] cache_entry[addr]==VALID);
*CASE A: if get_cache_status==0, and main_mem_bus_ready==1, *
* but cache_entry[addr]==0 then with 3 we fail 0N, *
* with 4 we're vacuous fail, or 0V *
*What do want? If I don't care about getting from the cache, why should *
*I fail nonvacuously? *

16.13.7 Implies and iff properties
A property is an implies if it has the following form:
property_expr1 implies property_expr2
A property of this form evaluates to true if, and only if,
either property_expr1 evaluates to false or
property_expr2 evaluates to true.

On Thu, Aug 11, 2011 at 1:04 PM, Little Scott-B11206
<B11206@freescale.com>wrote:

> Hi Ben:****
>
> ** **
>
> The rewrite that I think is most appropriate is below:****
>
> ** **
>
> the underlying evaluation attempt of property_expr1 is true and the
> underlying evaluation attempt of property_expr1 or property_expr2 is
> nonvacuous.****
>
> ** **
>
> Unfortunately it isn’t like ((not p1) or p2) or like |->. ((not p1) or p2)
> does not use the truth result of p1 to determine vacuity. This definition
> above requires that p1 evaluate to true for the overall property to be
> nonvacuous. The definition of |-> doesn’t have a vacuity result for the
> antecedent so it can’t be used and that introduces differences with the
> definition above.****
>
> ** **
>
> Why don’t we make a table to make this more concrete. Hopefully the table
> makes sense.****
>
> 0 = evaluates to false****
>
> 1 = evaluates to true****
>
> V = vacuous****
>
> N = nonvacuous****
>
> ** **
>
> 1 = ((not p) or q)****
>
> 2 = p |-> q (in this case column p we interpret 1 as a matching sequence
> and 0 as not a matching sequence the vacuity information is ignored)****
>
> 3 = definition in current proposal****
>
> 4 = definition in this e-mail****
>
> ** **
>
> p q 1 2 3 4****
>
> 0,V 0,V V V V V****
>
> 0,V 0,N N V V V****
>
> 0,N 0,V N V V V****
>
> 0,N 0,N N V V V****
>
> 0,V 1,V V V V V****
>
> 0,V 1,N N V V V****
>
> 0,N 1,V N V V V****
>
> 0,N 1,N N V V V****
>
> 1,V 0,V V V V V****
>
> 1,V 0,N N N V N****
>
> 1,N 0,V N V V N****
>
> 1,N 0,N N N N N****
>
> 1,V 1,V V V V V****
>
> 1,V 1,N N N V N****
>
> 1,N 1,V N V V N****
>
> 1,N 1,N N N N N****
>
> ** **
>
> What do you think? Do any of those definitions seem like what we should
> have?****
>
> ** **
>
> Thanks,****
>
> Scott****
>
> ** **
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *ben
> cohen
> *Sent:* Thursday, August 11, 2011 2:26 PM
>
> *To:* Little Scott-B11206
> *Cc:* Eduard Cerny; Korchemny, Dmitry; sv-ac@eda-stds.org
> *Subject:* 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* <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.