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

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 and req==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.