Formal Tech Tip: How Good Properties Can be Over-constrained and How to Fix It
Given the dramatic increase in the scalability of formal engines over the past 5 years, “formal testbenches” have grown to comprise hundreds, if not thousands, of assertions, constraint properties, and cover properties. Like with simulation-based constrained-random verification, the number of constraints and the overlap and dependencies among them can quickly exceed what a single engineer can envision. Rephrasing, as the number of constraint properties grows from dozens to hundreds, it’s easy for them to constrain the input state space such that some of the legal input scenarios are omitted, thus causing assertions to be vacuous and/or cover statements unreachable. Fortunately, there is a clear procedure you can follow to untangle your formal constraints and move forward with verification.
First, temporarily remove ALL the constraints, run Questa PropCheck, and see which assertions are reported as being “vacuous” – i.e. the property itself is inconsistent such that it never can be true — a trivial example is if you mistakenly ANDed a signal to its complement somehow. Naturally, the first step is to debug and fix any obvious errors. Vacuity can also be due to inconsistency with the design’s operation. Regardless of the source of the vacuity, these cases will need to be fixed regardless of external constraints.
Next, bring back in all the constraints and rerun PropCheck. This time some perfectly good properties could still be reported as being “vacuous”. Thus, if the properties ran clean before, without the constraints, chances are you are over-constraining the design with constraint properties that somehow conflict with each other to produce a false positive result – i.e. an error is reported when there really is none. This is where a very straightforward methodology described by Anshul Jain of Oski Technology comes in.
In his Verification Horizons article titled “Minimizing Constraints to Debug Vacuous Proofs”, 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. In a nutshell, the recommended process is to split the number of constraints in half, execute a formal run with only one of the halves, and see if the formal tool still reports a vacuous proof and/or shows over-constraining. Then try the “other half” and see if vacuity/over-constraining is detected. If the properties run clean on one half or the other, you know the issue is in the other half. Next, keep recursively commenting out “half of the halves” until you’ve isolated the overwrought constraint properties.
As the article shows, even if you have 1,000 constraint properties, if one constraint is the culprit the worst-case is that you’ll only have to do 15 iterations to find your needle in a haystack.
I trust this tip will help you reach your verification goals faster – please share your questions and experiences in the Comments section.
Happy verifying!
Joe Hupcey III,
on behalf of the Questa Formal and CDC team
