Tearless Formal Verification
Cooking can be a necessity, hobby or calming therapy depending on whom you talk to. Personally speaking, I cook occasionally but even when I am not cooking and I am just a mere silent admirer of this amazing process, onion peeling/cutting/chopping brings tears to my eyes 😀 There are few tricks that one could use to avoid or minimize tears while peeling onions. Some of these tricks work, some don’t.
Coming back to Formal verification, convergence, i.e. finding the conclusive answers to the verification problem (properties in the case of Formal verification) may require a good amount of effort, which can be tiring. If a property remains inconclusive, users invariably get into the tearful (metaphorically speaking) onion peeling exercise of simplifying the property and the logic driving the property, adding more constraints to limit the state space etc.; which sometimes works and sometimes does not.
Of course, design knowledge helps to know which part of the design logic is relevant for a given property but most of the times users need to know more specifically which specific set of registers, inputs and constraints are being evaluated by Formal mathematical engines.
Formal core is a subset of a property’s cone of influence (COI) logic and is a specific set of registers, inputs and constraints that are evaluated by Formal engines for a given property (or set of properties).
If users concentrate on these concise list of registers (reported by Formal core), they have a better chance of getting a conclusive answer.
As illustrated in this picture, COI for property P1 and P2 is significantly large, but whole COI logic is not required to prove these properties. Formal core for property P1 reports a large counter which is contributing to the real complexity of this property. Similarly, Formal core for property P2 reports a big multiplier which is contributing to the real complexity of the property.
By leveraging this very specific information, users can employ advanced abstraction techniques (one of the counter abstraction techniques was discussed in Iain’s blog “Driven to abstraction”) and add additional constraints; this reduces the overall effort and shortens the convergence time, resulting in significant time savings.
Formal core enables tearless Formal verification by delivering faster convergence and providing a good measure of verification performed as part of Formal verification.
Formal core data has a few additional useful applications like aiding vacuity debug, Formal coverage etc. which we will discuss in upcoming blogs. Stay tuned!!
