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.