Formal Tech Tip: What are Vacuous Proofs, Why They Are Bad, and How to Fix Them

By Joe Hupcey III

In formal verification, proving all of your properties is pretty much the main goal of the whole exercise – if all the assertions are proven, clearly the design has been exhaustively verified. This suggests that there is no such thing as a “bad proof”, right? Wrong! There is one case where a proof is bad – misleading, actually. It is when a proof is “vacuous”. What is this bad apple, how can you spot it, and how can you fix it? Read on …

What is a “vacuous proof”?

It often starts with a poorly written property: the “antecedent” – i.e. the definition on the left-hand-side of the operator – 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 “proof” result from such a “self-vacuous” property is an empty set, hence the term “vacuous proof”.

A similar source of “vacuity” is when your constraints (via “assume”, “assert”, or “cover” statements in SVA or PSL) constrict the input such that the “antecedent” in a property can never be true.

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 – 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’re getting ahead of ourselves …

How can you find out whether a property / proof is vacuous?

The good news is that quite often modern formal analysis tools like Questa PropCheck will flag vacuous properties immediately after the analysis is started. Building on this momentum, a related and easy “pro tip” to try is to temporarily remove ALL the constraint properties – just comment out all the “assume” statements for a moment, re-run PropCheck, and see which assertions are reported as “vacuous”. Fix these erroneous properties using the guidance below before proceeding.

Next, bring back in all the constraints and re-run PropCheck. This time some perfectly good properties could still be reported as being “vacuous”. Chances are this is due to either:

(A) An overly aggressive constraint, or set of constraints (as warned above)

(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’t happen because their property or DUT code completely skips intermediate states (as per the US vs. EU traffic light controller example)

How can you fix a property that caused a vacuous proof?

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.

But what if all the properties are “clean”, but some of these perfectly good properties are still being reported as being “vacuous”? As suggested above, your constraint properties somehow conflict with each other to produce a false positive result. There are two ways to address this:

1 – If your formal tool does not have a formal coverage analysis capability, there is very clever methodology described in the Verification Horizons article titled “Minimizing Constraints to Debug Vacuous Proofs” by Anshul Jain of Oski Technology. In a nutshell, Anshul outlines an easy-to-implement “divide and conquer” methodology that identifies a “minimum failing subset” (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.

2 – If you are using Questa PropCheck you are in luck: PropCheck includes formal coverage analysis – 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.

Detailing PropCheck’s coverage capabilities will be the subject of future posts, but in the meantime formal verification expert Mark Eslinger has posted some technical video presentations 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.

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 “vacuous with respect to the design” if the spec and implementation are mismatched. Once constraints are added into the picture, then proofs which are “vacuous with respect to the constraint” could show up. The good news is that Questa PropCheck has built-in capabilities to quickly discover and fix all these cases.

Joe Hupcey III,
for the Questa Formal Team

Reference links: