RE: [sv-ac] [SV-AC] F.5.3.3 Vacuity // Clarification on "implies" and suggestion

Hi Ben, Scott,

If we want to have that two semantically equivalent formulas have the same vacuity result, then we should use a semantic definition for vacuity (rather than a syntactic definition as we currently have).
For instance, we can define that a formula is vacuous if it suffers from temporal antecedent failure (TAF). A formula suffers from TAF on a give trace if it can be expressed as always (past_formula implies future_formula) and the past_formula does not hold on any prefix of the given trace. This will give us the same result for a property using |-> and an equivalent one using implies or the or operator. And it will not give us unintuitive results for other formulas using or.
It also gives an efficient algorithm for answering whether a formula suffers from TAF (and what are the reasons for that) -- see [BFR07].

Of course it has some limitations, as it focuses on a certain aspect of vacuity. But I think you would agree that's a very fundamental and non-arguable one. And if we wish we can add other semantic definitions for vacuity (or aspects of it).

Best,
Dana

[BFR07] Shoham Ben-David<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/b/Ben=David:Shoham.html>, Dana Fisman, Sitvanit Ruah<http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/r/Ruah:Sitvanit.html>: Temporal Antecedent Failure: Refining Vacuity. CONCUR 2007<http://www.informatik.uni-trier.de/~ley/db/conf/concur/concur2007.html#Ben-DavidFR07>: 492-506
http://www.cs.huji.ac.il/~danafi/publications/TAF_CONCUR07.pdf

From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On Behalf Of Little Scott-B11206
Sent: Thursday, September 30, 2010 2:50 PM
To: ben@systemverilog.us
Cc: sv-ac@eda.org
Subject: RE: [sv-ac] [SV-AC] F.5.3.3 Vacuity // Clarification on "implies" and suggestion

Hi Ben:

I agree that the vacuity definition for implies should be changed. It is obviously not good.

I don't think that the solution for or is quite as simple as you suggest. Your suggestion is

(not p1) implies p2

in this case if p1 succeeds vacuously and p2 succeeds nonvacuously I presume the updated vacuity definition of implies would return vacuous in this case. For a reasonable definition of or I can see nonvacuous returned. In fact, the current vacuity definition of or returns nonvacuous in this case, but I can't just swap properties back and forth to get the vacuity result I prefer....

I guess my conclusion is that we should fix the definition for implies, but there are still a number of unsatisfactory/surprising results hanging around in the vacuity definitions.

Erik: Have you thought much about how a language mechanism for controlling vacuity would look/function?

Thanks,
Scott

From: ben cohen [mailto:hdlcohen@gmail.com]
Sent: Wednesday, September 29, 2010 1:51 PM
To: Little Scott-B11206
Cc: sv-ac@eda.org
Subject: Re: [sv-ac] [SV-AC] F.5.3.3 Vacuity // Clarification on "implies" and suggestion

Scott,
Thanks for your detailed explanations. Your observations and assumptions are correct.
[Scott]You could look at changing the definition of implies to be consistent with |->, but then what about case c? How would you change the definitions of not and or to make that result consistent?

[Ben] I would like to see the implies operator behave like a true "implication", meaning that if the antecedent if false then the property expression is vacuous. If you take a look at the definition in 16.13.6 Implication, "The implication construct specifies that the checking of a property is performed conditionally on the match of a sequential antecedent".
I understand that this was meant for the implication operators, but the English use of the word implies truly suggests implication. Thus, I strongly believe that with regards to vacuity, the implies should behave like the overlapping implication operator. I also recommend that we do not change the definition of vacuity for the or operator. Thus, except for vacuity, the "p1 implies p2" is same as "(not p1) or p2". This will provide the option to choose how an antecedent is handled in terms of vacuity.
I see the following equivalences of operators :
  sequence |-> property // implication, LHS==sequence; RHS== property
  sequence |=> property // implication, LHS==sequence; RHS== property
  property implies property // implication, LHS==property; RHS== property
  sequence #-# property // concatenation of sequence and a property
  sequence #=# property // concatenation of sequence and a property
  sequence or sequence // ORing of 2 sequences
  property or property // ORing of 2 properties

[Scott] For another potentially thought provoking case consider the results of p1 or p2 where p1 has vacuous success and p2 has nonvacuous failure. There are other cases like this.

[Ben] With the adoption of vacuity for the implies, one could use "(not p1) implies p2" if we want the result of the equivalent "p1 or p2" to be vacuous if the antecedent is vacuous. Otherwise, vacuous success is TRUE. However, I am open to other alternatives.

Ben Cohen
ben@systemverilog.us<mailto:ben@systemverilog.us>
On Wed, Sep 29, 2010 at 7:10 AM, Little Scott-B11206 <B11206@freescale.com<mailto:B11206@freescale.com>> wrote:

Hi Ben:

There are some problems with the vacuity definitions in the LRM. What isn't clear is what the correct solution is. Erik recently floated the idea of having some language mechanisms to control vacuity (http://www.eda-stds.org/sv-ac/hm/9443.html). I think this is an interesting idea. To give some flavor to the problems with defining vacuity in a consistent way let's use your example. I am going to use the English descriptions from 16.15.8 as they may be easier to understand.

1. An evaluation of a property that is a sequence is always nonvacuous.

2. 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.

3. 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.

4. An evaluation attempt of a property of the form not property_expr is nonvacuous if, and only if, the underlying evaluation attempt of property_expr is nonvacuous.

5. An evaluation attempt of a property of the form property_expr1 implies property_expr2 is nonvacuous if, and only if, the evaluation attempt of property_expr1 is nonvacuous.

Given those definitions let's look at a few forms.

a. sequence_expression implies property_expr

b. sequence_expression |-> property_expr

c. (not sequence_expression) or property_expr

I am assuming that in the implies and not case the sequence_expression is promoted to a property and definition 1 above applies. I am also assuming that you would like to see the same vacuity results from these three forms.

Let's assume that sequence_expression is evaluated but does not have a match. This results in the associated property as having nonvacuous failure. Let's say that property_expr has vacuous success. Based on the definitions above the results would be:

a. nonvacuous success

b. vacuous success

c. nonvacuous success

You could look at changing the definition of implies to be consistent with |->, but then what about case c? How would you change the definitions of not and or to make that result consistent?

For another potentially thought provoking case consider the results of p1 or p2 where p1 has vacuous success and p2 has nonvacuous failure. There are other cases like this.

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: Tuesday, September 28, 2010 6:05 PM
To: Korchemny, Dmitry; sv-ac@eda.org<mailto:sv-ac@eda.org>
Subject: [sv-ac] [SV-AC] F.5.3.3 Vacuity // Clarification on "implies" and suggestion

F.5.3.3 Vacuity states: An evaluation of P on w is nonvacuous provided w P.
w non-vacuous on "P1 implies P2" iff w is non-vacuous on P1.
I can't type the symbology, but I don't quite understand it totally.
But, if I understand it correctly,
 "P1 implies P2" is vacuous if P1 is vacuous; correct?
If P1 is a sequence, it is never vacuous. Yet wouldn't it be desirable to
have the property "P1 implies P2" be vacuous if the antecedent if false, like the implication operator?
Thus, I could write something like:
sequence t; 1; endsequence
sequence t1; t ##1 1; endsequence
sequence t4; t ##4 1; endsequence
property P;
   (t ##0 a) implies
     (t ##0 b) and
     (t1 ##0 c) and
     (t4 ##0 d);
endproperty

Please, don't educate me on how to write this with the implication operator; that is not my point.
My point is that this is another style where I want to use the "implies" operator, yet, if the antecedent if false, I don't want the property P to be TRUE non-vacuously. In simulation, the success count would be high.
Question: Do we want to entertain the idea of an "implies" property to be vacuous if the antecedent is false?
The "p1implies p2" is same as "(not p1) or p2".
Ben Cohen

--
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.