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

On Wed, Sep 29, 2010 at 7:10 AM, Little Scott-B11206
<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] 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.