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

Dmitry,
Therefore, to be consistent we need to state that p1 implies p2 is
nonvacuous if p1 evaluates to true and p2 is nonvacuous. This leaves a
question open whether we want *p1 to evaluate nonvacuously *(as in Ben’s
proposal) *or not*. IMO if we don’t require non-vacuity of p1, we are more
consistent with other definitions where at least one non-vacuity is
required.
[Ben] My understanding or interpretation of vacuity is as follows:
*vacuity*: *A property is vacuous if it lacks serious purpose*. Vacuity
rules are usually applied when implication operator is used. A property
succeeds vacuously if the antecedent is FALSE. A property succeeds
non-vacuously only if the consequent of the implication contributes to its
success. Many applications have a triggering event that causes the thread to
start (in the antecedent), and if the triggering event does not occur (i.e.,
if false)* [this applies to the implication operator]*, then there is no
need to further evaluate the thread (i.e., the rest of the property for that
cycle), which is then considered vacuously TRUE.

In P_implies: *assert property*(p1 *implies *p2); if p1 is vacuously true,
the property of the assertion (i.e., the (p1 *implies *p2)lacks serious
purpose. For example, if p1 is vacuous and p2 is trrue nonvacuously,
reporting that the assertion P_implies was covered and succeeded is
misleading. As a user of the reports, I would be forced to write other
assertions to counter this false reporting of coverage, and that can get
complicated.

I agree that the definition of the *implies* vacuity should be as consistent
with the definition of the suffix implication |-> vacuity. With the
implication operator, the antecedent in non-vacuous because it is a
sequence;

Now, looking at the following 2 definitions in 16.15.8 Nonvacuous
evaluations, I do question "f" for the "and" property operator.
[16.15.8]* e) An evaluation attempt of a property of the form property_expr1
or 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.*
[Ben] That makes sense because if p1 is vacuous (i.e, a don't case about
it's outcome since it results contributes nothing to the assertion), then we
would care about p2.

[16.15.8] *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.*
[Ben] That does not make sense because if p1 is vacuous (i.e, a don't case
about it's outcome since it results contributes nothing to the assertion),
then why would the true (NV) success p2.be the only criteria for
a successful coverage? Example, let p1 define a successful data fetch and
p2 define a bus transfer
(e.g., p1: fetch_sequence |-> ##[1:4]rdy ##1 mem_data_valid)
(e.g., p2: rdy ##1 bus_grant |-> ##[1:4]data_bus==mem[addr])
In (*p1 and p2)*, it seems that for a good coverage, both of them need to be
non-vacuously true. Thus, in the above example, if *fetch_sequence* fails,
but we go ahead and evaluate p2, and it is non-vacuously true, then this
*(p1 and p2)*counts toward the coverage. I maybe wrong, but that does not
sound like an "and" operation to me.
The point of all this: coverage.
Ben Cohen

On Sun, Aug 14, 2011 at 9:45 AM, Korchemny, Dmitry <
dmitry.korchemny@intel.com> wrote:

> Hi all,****
>
> ** **
>
> As Ben mentioned in one of his previous mails I think that the definition
> of the *implies* vacuity should be as consistent with the definition of
> the suffix implication |-> vacuity. The latter is given by the following
> statement:****
>
> ** **
>
> h) An evaluation attempt of a property of the form *sequence_expression **|->
> **property_expr *is****
>
> nonvacuous if, and only if, there is a successful match of the antecedent
> *sequence_expression *and****
>
> the evaluation attempt of *property_expr *that starts at the end point of
> the match is nonvacuous.****
>
> ** **
>
> Therefore, to be consistent we need to state that p1 implies p2 is
> nonvacuous if p1 evaluates to true and p2 is nonvacuous. This leaves a
> question open whether we want p1 to evaluate nonvacuously (as in Ben’s
> proposal) or not. IMO if we don’t require non-vacuity of p1, we are more
> consistent with other definitions where at least one non-vacuity is
> required.****
>
> ** **
>
> Whatever the decision be, we need to update Annex F accordingly. Also, this
> Mantis is a good opportunity to fix the first paragraph of 16.15.8: we need
> to delete the sentence that I put into square brackets.****
>
> ** **
>
> An evaluation attempt of a property is either vacuous or nonvacuous. [In
> the following, nonvacuous evaluation is described for the following kinds of
> properties: sequence, negation, disjunction, conjunction, if–else,
> implication, and instantiation.]****
>
> ** **
>
> Thanks,****
>
> Dmitry****
>
> ** **
>
> *From:* ben cohen [mailto:hdlcohen@gmail.com]
> *Sent:* Friday, August 12, 2011 00:16
>
> *To:* Little Scott-B11206
> *Cc:* Eduard Cerny; Korchemny, Dmitry; sv-ac@eda-stds.org
> *Subject:* 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. ****
>
> ** **
> ---------------------------------------------------------------------
> 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, and is
believed to be clean.