Formal Verification for Post-silicon Debug

OK, let’s face it, when you think of post-silicon debug then formal verification is not the first thing that springs to mind. But once a design has been manufactured, debugging can be very expensive. As then-CEO of MIPS John Bourgoin said at DesignCon 2006, “Finding bugs in model testing is the least expensive and most desired approach, but the cost of a bug goes up 10× if it’s detected in component test, 10× more if it’s discovered in system test, and 10× more if it’s discovered in the field, leading to a failure, a recall, or damage to a customer’s reputation.”

But formal verification at the chip level is a major challenge. There are capacity issues, of course, since chips are much larger than individual blocks (yeah, who knew?). The properties to be validated are high-level and complex. So basic assertion-based verification (ABV) is inadequate and deep formal is required.

Traditionally when a bug is found in silicon, additional simulation is done to try and identify the source of the undesired behavior. But this approach can be very time-consuming and is inadequate for finding those bugs that only occur in actual silicon after a long time (and so only appear in simulation after a geological era has gone by). Of course the original testbench doesn’t exhibit the behavior (or the chip wouldn’t have been released to manufacturing) meaning that more vectors need to be created without necessarily having much idea about what vectors would be good.

Formal verification avoids this problem since it ignores the testbench completely and uses its own input stimuli. As a result, formal analysis is capable of generating conclusive answers to verification problems.

Formal verification has the capability to cut through this. Declare a property that the bad behavior does not exist. But since it is known to exist, formal verification should fail this property and, at the same time, generate an exact sequence of waveforms to reproduce the problem.

Only formal tools with a focus on full proofs of complex design properties will have the capacity to converge on the problem within an acceptable time. Additionally, once the problem has been identified and a fix proposed, formal verification can be used to prove that the problem really is fixed.

With formal’s unique ability to remove verification ambiguity, it becomes an invaluable tool in reducing the time and effort spent addressing post-silicon debug issues. Formal’s ability to quickly identify bugs, assure the cleanliness of sub-blocks, and verify the completeness of design fixes provides the highest value post-silicon debug tool in the team’s arsenal.

For the Jasper white paper on the subject, go here.