Y can also use #-# or #=# and p be something else than |-> |=>.
Best...
ed
From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Monday, August 15, 2011 4:14 PM
To: Korchemny, Dmitry
Cc: Little Scott-B11206; Eduard Cerny; sv-ac@eda-stds.org
Subject: Re: [sv-ac] RE: Issue 2578: Vacuity definition
Dmitry,
I uploaded Mantis_2578_vacuity_5.pdf<http://www.eda-stds.org/svdb/file_download.php?file_id=5305&type=bug> [^<http://www.eda-stds.org/svdb/file_download.php?file_id=5305&type=bug>] (319,802 bytes) 2011-08-15 12:29
per your recommendations. However, when I provide guidelines on the use of the implies operator, I'll recommend that the antecedent be non-vacuous (i.e., use a sequence) to insure that the coverage is more meaningful.
Except for a simulation performance, coverage, and vacuity, the 2 properties below are identical:
Prop1: (sequenceA |-> sequenceB) implies sequenceC
Prop2: (sequenceA ##0 sequenceB) implies sequenceC
Note that in this mantis, I also made a change to 16.13.7 Implies and iff properties and to F.5.3.3 Vacuity
On 2578, I vote YES (in the event that you guys vote) as I'll not be able to attend Tuesday's meeting.
Ben Cohen
On Sun, Aug 14, 2011 at 11:29 PM, Korchemny, Dmitry <dmitry.korchemny@intel.com<mailto:dmitry.korchemny@intel.com>> wrote:
Hi Ben,
I can see reasons for either definition, but I think that the discussion is mostly theoretic. I've never seen assertions like (s1|-> p1) implies (s2 |-> p2), etc. Therefore the most important issue is consistency. From the practical point of view there is no difference between your and my definition of implies vacuity.
I think that much more important to define a more general notion of vacuity as property redundancy relative to the model. This is related to Dana's presentation. But this is a different issue.
Thanks,
Dmitry
From: ben cohen [mailto:hdlcohen@gmail.com<mailto:hdlcohen@gmail.com>]
Sent: Sunday, August 14, 2011 22:32
To: Korchemny, Dmitry
Cc: Little Scott-B11206; Eduard Cerny; sv-ac@eda-stds.org<mailto:sv-ac@eda-stds.org>
Subject: 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<http://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<mailto: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<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<mailto: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<mailto: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> [mailto: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<mailto: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<mailto:B11206@freescale.com>> wrote:
Hi Ben:
See my response below.
Thanks,
Scott
From: ben cohen [mailto:hdlcohen@gmail.com<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<mailto: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<mailto: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<mailto:Eduard.Cerny@synopsys.com>]
Sent: Thursday, August 11, 2011 10:19 AM
To: Korchemny, Dmitry; Little Scott-B11206; sv-ac@eda-stds.org<mailto: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> [mailto: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<mailto: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<mailto:B11206@freescale.com>]
Sent: Thursday, August 11, 2011 18:08
To: Korchemny, Dmitry; sv-ac@eda-stds.org<mailto: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<mailto:dmitry.korchemny@intel.com>]
Sent: Thursday, August 11, 2011 10:04 AM
To: Little Scott-B11206; sv-ac@eda-stds.org<mailto: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<mailto:B11206@freescale.com>]
Sent: Thursday, August 11, 2011 16:18
To: Korchemny, Dmitry; sv-ac@eda-stds.org<mailto: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> [mailto: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<mailto: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. --------------------------------------------------------------------- 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.Received on Mon Aug 15 13:27:19 2011
This archive was generated by hypermail 2.1.8 : Mon Aug 15 2011 - 13:27:25 PDT