Re: [sv-ac] Checking for nonvacuity of ORed properties

Dana,
[Dana]By giving the vacuity information to the user, she can decide to
split that property or code it otherwise if she wishes to check other parts
of it.
[Ben] Your points are well taken; however, there is no guarantee that
vacuity information is always provided. That would occur if one of
properties of the "or" operator succeeds first. For example;
  a |-> (b |=> c) or (d ##10 e |-> f);
For all cycles in simulation, assume a==1, b==1, c==1, d==1, e==0.
Since the LHS (b |=> c) succeeds first, the ORed property succeeds
nonvacuously, and the vacuity of the RHS (d ##10 e |-> f) is never
provided. That should be checked with a cover of each sub-property. The
bottom line here is that the user is not necessarily given vacuity
information.

What got me into this is because the ORing of anything is by definition a
choice. By using the nonvacuous(property_expr) The user can be assured that
at least one successful path was searched. Of course, if one path is found,
it does not mean that the other path was ever attempted. The user still
needs to check the coverage of each sub-property, regardless of the use or
non-use of this "nonvacuous" property qualifier.

Thanks for your feedback,
Ben Cohen

On Mon, Mar 19, 2012 at 7:09 AM, Dana Fisman Ofek
<Dana.Fisman@synopsys.com>wrote:

> Hi Ben,****
>
> ** **
>
> You are saying:****
>
> ** **
>
> *If the property has a vacuous sub-property, then search for all other
> sub-properties for a nonvacuous success. If none is found then, then the
> property is vacuous.*
>
> ** **
>
> But that misses the intent of vacuity. The intent of vacuity is, in case a
> property holds, then alert to the user if some parts of the specification
> was not examined at all, in order to conclude that it holds. This may
> indicate that there is something wrong with the property or the design or
> the environment. You seem to be suggesting to ignore some vacuity
> indication, and not report them to the user. No?****
>
> ** **
>
> Indeed, in your example ap_or0 and ap_or are tautologies, so clearly
> something is wrong with the specification. For the property
> ap_reqack1_or_cache_hit, it is clearly valuable to alert if fetch==1 andreq==0.
> I don’t see why the property should be further examined once it is find to
> hold. By giving the vacuity information to the user, she can decide to
> split that property or code it otherwise if she wishes to check other parts
> of it.****
>
> ** **
>
> Best,****
>
> Dana****
>
> ** **
>
> ** **
>
> *From:* owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] *On Behalf Of *Ben
> Cohen
> *Sent:* Saturday, March 17, 2012 3:28 PM
> *To:* sv-ac@eda-stds.org
> *Subject:* [sv-ac] Checking for nonvacuity of ORed properties****
>
> ** **
>
> See http://www.eda-stds.org/svdb/view.php?id=4081****
>
> ** **
>
>
> --
> 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.