Re: [sv-ac] When does an assertion fail vacuously?

Dana,
Thanks for the explanation. I have a different view on the definition of
vacuity. Specifically, I see the following definition, using your
definition:

*vacuity*: A property is considered vacuous if it lacks serious purpose. 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.

Other definitions:
http://www.thefreedictionary.com/vacuity
*1. *Total absence of matter; emptiness.
*2. *An empty space; a vacuum.
*3. *Total lack of ideas; emptiness of mind.
*4. *Absence of meaningful occupation; idleness: "the crew, being patient
people, much given to slumber and vacuity" (Washington Irving).
*5. *The quality or fact of being devoid of something specified: a vacuity
of taste; a vacuity of emotions.
*6. *Something, especially a remark, that is pointless or inane: a
conversation full of vacuities.

http://www.merriam-webster.com/dictionary/vacuity
 <http://www.merriam-webster.com/dictionary/vacuity>
Related to VACUITY
Synonyms: black hole, blank, blankness, emptiness, vacancy, void
Antonyms: fullness

Actually, the concept of PASS/FAIL vacuity does not make sense to me;
something is either vacuous or nonvacuous. That concept of PASS/FAIL
vacuity sounds convoluted. If an assertion attempt is vacuous, then it
means that attempt does not contribute to the assessment of that attempt as
to its success or failure, and does not contribute to the verification of
the property.

Per the LRM, the tools are not required to show PASS/FAIL vacuity, but just
vacuity.

More comments on your remarks below:

2010/10/6 Dana Fisman <Dana.Fisman@synopsys.com>

> Hi Ben,
>
>
>
> Section 16.15.8 starts with:
>
> “An evaluation attempt of a property is either vacuous or nonvacuous. In
> the following, nonvacuous
>
> evaluation is described …”
>
>
>
> and ends with
>
> “An evaluation attempt of a property succeeds nonvacuously if, and only if,
> the property evaluates to true and
>
> the evaluation attempt is nonvacuous.”
>
>
>
> So yes, it does not explicitly say that
>
> “An evaluation attempt of a property fails nonvacuously if, and only if,
> the property evaluates to false and
>
> the evaluation attempt is nonvacuous.”
>
[Ben] The above line addresses the nonvacuous failure, i.e., a real
failure. It says nothing about vacuous failure.

>
>
> And yes, the property not (a |-> b) should fail vacuously if a never
> holds.
>
[Ben] Above just states that the attempt when a==0 is vacuous, irrelevant,
not important, does not contribute to the assessment of the property.

>
>
> Regarding, accept_on (b) \phi – suppose that b never occurs and \phi fails
> vacuously, then the whole property fails, and according to item ab)
>
> “An evaluation attempt of a property of the form *accept_on*(*
> expression_or_dist*) *property_expr *is
>
> nonvacuous if, and only if, the underlying evaluation attempt of *property_expr
> *is nonvacuous and
>
> *expression_or_dist *does not hold in any time step of that evaluation
> attempt.”
>
> it is vacuous.
>
>
>
> Best,
>
> Dana
>
>
>
>
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *ben
> cohen
> *Sent:* Wednesday, October 06, 2010 5:12 AM
> *To:* sv-ac@eda.org; Korchemny, Dmitry
> *Subject:* [sv-ac] When does an assertion fail vacuously?
>
>
>
> Where is vacuous fail defined in the LRM? I could not find it.
>
> Consider the property (*not* (a |-> b)), and "a"==0; Then (a|-> b) is
> vacuous success.
>
> Does that mean that *not*(a|->b) is vacuous fail?
>
> Also, at our meeting today, I heard that* accept_on* can produce vacuous
> fail. I don't get it.
>
> Can you point me to cases of vacuous failure, and where in the LRM this
> defintion exists?
>
>
>
> 16.15.8 defines nonvacuous, but the LRM does not define vacuous (I don’t
> think).
>
> I can't find vacuous fail or vacuous pass. It can succeed vacuously, but
> that is not a pass or a fail.
>
> Also, here is a pass counter, fail counter, vacuous counter.
>
>
>
> Thanks,
>
> Ben
>
>
> --
> 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.