{"id":12921,"date":"2017-12-06T15:56:28","date_gmt":"2017-12-06T22:56:28","guid":{"rendered":"https:\/\/blogs.mentor.com\/verificationhorizons\/?p=12921"},"modified":"2026-03-27T08:51:34","modified_gmt":"2026-03-27T12:51:34","slug":"formal-tech-tip-what-are-vacuous-proofs-why-they-are-bad-and-how-to-fix-them","status":"publish","type":"post","link":"https:\/\/blogs.sw.siemens.com\/verificationhorizons\/2017\/12\/06\/formal-tech-tip-what-are-vacuous-proofs-why-they-are-bad-and-how-to-fix-them\/","title":{"rendered":"Formal Tech Tip: What are Vacuous Proofs, Why They Are Bad, and How to Fix Them"},"content":{"rendered":"

\"\"<\/a>In formal verification, proving all of your properties is pretty much the main goal of the whole exercise \u2013 if all the assertions are proven, clearly the design has been exhaustively verified. This suggests that there is no such thing as a \u201cbad proof\u201d, right? Wrong! There is one case where a proof is bad \u2013 misleading, actually. It is when a proof is \u201cvacuous\u201d. What is this bad apple, how can you spot it, and how can you fix it?\u00a0 Read on \u2026<\/p>\n

What is a \u201cvacuous proof\u201d?<\/u><\/p>\n

It often starts with a poorly written property: the \u201cantecedent\u201d \u2013 i.e. the definition on the left-hand-side of the operator \u2013 defines an inconsistent state that can never be true. The most common occurrence of this is when you mistakenly AND a signal to its complement somehow. This seems like it would be an easy mistake to spot, but when signals go through a lot of combinatorial logic, and\/or change names when they cross IP boundaries or layers of hierarchy, you can lose track of such things pretty quickly. Regardless, the \u201cproof\u201d result from such a \u201cself-vacuous\u201d property is an empty set, hence the term \u201cvacuous proof\u201d.<\/p>\n

A similar source of \u201cvacuity\u201d is when your constraints (via \u201cassume\u201d, \u201cassert\u201d, or \u201ccover\u201d statements in SVA or PSL) constrict the input such that the \u201cantecedent\u201d in a property can never be true.<\/p>\n

Finally, if the behavior described by a property is simply not supported by the design, or vice-versa, you can also get a vacuous proof. For example, imagine you are verifying a traffic light controller where the spec says the light will go from Red-to-Green, Green-to-Yellow, Yellow-to-Red, and then loop back again. You write properties for this, but the tool comes back reporting them as vacuous \u2013 what gives? As it turns out, your colleague sent you the DUT code for a type of European traffic light controller that briefly flashes the Yellow light after a Red signal, THEN goes to Green. In this case, the vacuous proof is the fault of a spec or DUT configuration bug, and not a problem with the constraint properties, per se. But we\u2019re getting ahead of ourselves \u2026<\/p>\n

How can you find out whether a property \/ proof is vacuous?<\/u><\/p>\n

The good news is that quite often modern formal analysis tools like Questa PropCheck<\/a> will flag vacuous properties immediately after the analysis is started. Building on this momentum, a related and easy \u201cpro tip\u201d to try is to temporarily remove ALL the constraint properties \u2013 just comment out all the \u201cassume\u201d statements for a moment, re-run PropCheck<\/a>, and see which assertions are reported as \u201cvacuous\u201d.\u00a0 Fix these erroneous properties using the guidance below before proceeding.<\/p>\n

Next, bring back in all the constraints and re-run PropCheck<\/a>. This time some perfectly good properties could still be reported as being \u201cvacuous\u201d. Chances are this is due to either:<\/p>\n

(A) An overly aggressive constraint, or set of constraints (as warned above)<\/p>\n

or<\/p>\n

(B) A bug in the specification, or either the property code writer or the DUT developer misread the spec such that they coded state transitions that simply can\u2019t happen because their property or DUT code completely skips intermediate states (as per the US vs. EU traffic light controller example)<\/p>\n

How can you fix a property that caused a vacuous proof?<\/u><\/p>\n

Naturally, the first step is to go ahead and fix any obvious errors in the antecedent (left hand side) of properties reported as vacuous by editing the property to describe possible behavior between the signals.<\/p>\n

But what if all the properties are \u201cclean\u201d, but some of these perfectly good properties are still being reported as being \u201cvacuous\u201d?\u00a0 As suggested above, your constraint properties somehow conflict with each other to produce a false positive result. There are two ways to address this:<\/p>\n

1 \u2013 If your formal tool does not have a formal coverage analysis capability, there is very clever methodology described in the Verification Horizons article titled \u201cMinimizing Constraints to Debug Vacuous Proofs<\/em><\/a>\u201d by Anshul Jain of Oski Technology. In a nutshell, Anshul outlines an easy-to-implement \u201cdivide and conquer\u201d methodology that identifies a \u201cminimum failing subset\u201d (MFS) of constraints with a minimum number of formal runs. As the article shows, even if you have 1,000 constraint properties, if one constraint is the culprit the worst-case is that you will only have to do 15 iterations to find your needle in a haystack.<\/p>\n

2 \u2013 If you are using Questa PropCheck<\/a> you are in luck: PropCheck<\/a> includes formal coverage analysis \u2013 no separate license is needed! Specifically, the formal coverage on the vacuously proven property tells you what logic\/assumptions, if any, were used to determine the property as vacuous. With this information, you can immediately zero in on places to look to debug and fix the vacuous property by removing\/rewriting constraints, fixing the antecedent to match spec\/design behavior, or fixing self-vacuous conditions.<\/p>\n

Detailing PropCheck\u2019s coverage capabilities will be the subject of future posts, but in the meantime formal verification expert Mark Eslinger has posted some technical video presentations<\/a> on Verification Academy on how formal coverage can be used to debug properties — vacuous and otherwise; as well as help resolve Inconclusives, and expedite over-constraint and state reachability analysis.<\/p>\n

In conclusion, vacuous proofs need to be addressed because they give you no information about the DUT behavior you are looking to verify. They can be caused by self-vacuous properties (the A & !A clear conflict), or be \u201cvacuous with respect to the design\u201d if the spec and implementation are mismatched. Once constraints are added into the picture, then proofs which are \u201cvacuous with respect to the constraint\u201d could show up. The good news is that Questa PropCheck<\/a> has built-in capabilities to quickly discover and fix all these cases.<\/p>\n

Joe Hupcey III,
\nfor the Questa Formal Team<\/p>\n

Reference links:<\/strong><\/p>\n