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

Dana,
Sounds good. Quick observation that needs to be considered.
1) Order of grouping. Consider (p1 *or* p2 *or* p3):
      RH_1st: ( (p1 *or *(p2 *or *p3))
      LH_1st: ( ( p1 *or *p2) *or *p3)
If p2 is vacuous, what should the result be?
With the |-> operator, if p1 and p2 are sequences, then
 (p1 |-> p2 *|->* p3):
      RH_1st: ( (s1 *|-> *(s2 *|-> *p3))
      LH_1st: ( ( s1 *|-> *s2) *|-> *p3)
they are interpreted as RH_1st since ( s1 *|-> *s2) is a property, and
(property |-> property) is illegal.

If p1==1, p2==1, p3 == vacuous, what is the result ?

2) What about the *and *operator* ? *
* ( p1 and p2 and p3) *
* If p1==1, p2==1, p3 == vacuous, what is the result ? *

Just some thoughts for now.
Thanks for the excellent suggestions.
Ben

On Sun, Oct 3, 2010 at 12:34 AM, Dana Fisman <Dana.Fisman@synopsys.com>wrote:

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