What is a vacuous proof? How dangerous are they?
Answered by Anshul Jain | June 3, 2020
A vacuous proof is a dangerous thing in formal verification and needs immediate attention. It is an extreme case of a false positive where your checker says that everything is working fine while often checking nothing meaningful. The most common reason to arrive at a vacuous proof is the presence of conflicting constraints in the formal verification environment. So, meticulous management of constraints goes a long way in helping to avoid them. However, there are other reasons as well.
Read on for the complete answer…
Let us now focus on the major cause of vacuous proofs.
The process of building a Level 4 formal verification testbench involves writing the checkers, running them and debugging the failing checkers. While debugging, we may find that the root-cause indicates a design bug, a flaw in the checker itself, or we may identify missing constraints on the behavior of the input signals. In case of the last option, we would then add the missing constraints, re-run the checkers and the cycle continues until the checkers stop failing or it starts reporting real issues in the design.
Adding constraints on an as-needed basis is a good technique and provides the advantage of keeping the formal verification environment under-constrained. However sometimes, human errors while managing incremental implementation of constraints leads to conflicting constraints, which in turn over-constrain the environment accidentally. Let us take a simple example to understand this phenomenon.
Say we have a design with two inputs,
q. And somehow, we made a blunder of writing two conflicting constraints,
p |-> q and
p |-> !q on the inputs. How would you resolve this conflict and still honor the conflicting constraints? Simple, do not assert
p at all. That’s exactly how formal tools resolve such conflicts. Here, we ended up over-constraining the formal verification environment with two constraints that are seemingly harmless when taken individually, but conflicting with each other.
Since we now know how conflicting constraints may lead to accidental over-constraints, let us move ahead and understand how over-constraints may cause vacuous proofs. Logic defines a vacuous proof as one where a statement is true because its hypothesis is false. Say we want to prove
a -> b,
a(the hypothesis) is always false.
a -> b(the statement) is always true.
Checkers are statements about design behavior that we expect to hold true in the design implementation. For example, the checker shown below intends to verify that once the slave sends a non-last beat and it gets accepted by the master, then the slave must send the last beat within a finite duration.
In an over-constrained formal verification environment, where input stimulus has been completely blocked, outputs may get muted. In our example, if
rvalid never gets asserted due to lack of input stimulus, the checker would pass vacuously.
Your formal tool may sense the presence of conflicting constraints and throw an error or at least a warning. However, identifying the exact set of conflicting constraints can become a time-consuming exercise. What makes it worse is when the conflict involves the RTL as well. (Wondering how RTL would conflict with constraints? Then please read this article. It uses a real-world example to explain how RTL too can contribute to conflicts with constraints.)
In order to mitigate the risk of introducing conflicting constraints and save the time of debugging them, we can rely on a strict methodology to avoid such a situation in the first place.
Some of the best practices for avoiding conflicting constraints and thereby, vacuous proofs are:
#1 Think “cause” and “effect”
It is advisable, although not required, that property expressions be thought in terms of “cause” and “effect” where the “cause” becomes antecedent of the expression and the “effect” becomes consequent. Next, carefully identify the signals that need to be constrained and ensure that they always land into the “effect” i.e., consequent of the expression. For example, both
empty |-> !pop and
pop |-> !empty property expressions implies the same truth, i.e., empty FIFO is never popped. However, only the first one fits into the “cause” and “effect” paradigm.
It is also important to include the “cause” in the property expression, in the form of an antecedent, as much as possible, even if it makes the code more verbose. For example, both the property expressions,
(count <= MAX) and
(count == MAX) |-> !incr implies that the counter value remains less than equal to maximum value. However, the second property expression is recommended.
#2 Constrain only “inputs”
Ensure the constraints are being applied on signals that are input to the design. If it is required to apply constraints on an internal signal of the design, place a cutpoint on that internal signal first and then apply the constraint.
#3 Review your constraints
While implementing a new constraint in your formal verification environment, review the existing set of constraints for overlapping signals. Best practice #1 would help speed-up the review.
Other causes of vacuous proofs…
Faulty checkers can also result in vacuous proofs in formal verification. Sometimes, the implementation of a checker is incorrect and sometimes the intent itself is incorrect. Let us take a look at some examples.
Example #1: Checker implementation is incorrect
The following checker will pass vacuously for a design using active-high reset. Reason being, it is mistakenly disabled forever due to the incorrect expression used in “disable iff” condition. The correct expression would be reset high instead of reset low.
Example #2: Checker intent is incorrect
“Once the sender asserts valid, it should keep it asserted until the receiver asserts ready”
This is a correct checker description for a standard valid-ready handshake protocol, where the sender does not need to wait for ready from the receiver before asserting valid, nor does the receiver need to wait for valid from the sender before asserting ready. However, in a modified version of the valid-ready protocol where the sender waits for ready from the receiver before asserting valid, the aforementioned checker description would become incorrect. And, if implemented as described, would cause the checker to pass vacuously.
Follow-up questions? — #AskOski