The advantages of formal verification are well-known and accepted in semiconductor development. This wasn’t always the case; a few decades ago, formal technology was widely regarded as an exotic technique requiring “magic” to be used successfully on a real project. Over this span, many success stories of truly scary bugs found before signoff have helped to raise awareness of—and confidence in—formal verification.
The ability to mathematically prove exhaustively that a chip design meets a set of assertions is a clear contrast with simulation, which can’t come up with proof of bug absence. If proof can’t be achieved due to legal design scenarios that violate the assertions, the formal tool presents these as counterexamples and provides information to help designers debug them. Users provide constraints that keep the formal analysis within legal bounds, ensuring that counterexamples are real failure scenarios that could occur in post-silicon chip usage.