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.