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

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] On Behalf Of ben
cohen
Sent: Tuesday, September 28, 2010 6:05 PM
To: Korchemny, Dmitry; 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, and is
believed to be clean.