11 Myths About Formal Verification
By Tom Anderson, Electronic Design
Formal verification, which uses mathematical analysis rather than simulation tests, has been available in commercial EDA tools for more than 20 years and in academia much longer. As with many new technologies, initial adoption was slow and limited to companies who had in-house formal experts. This has changed dramatically in the last dozen years or so. Almost every chip-development team makes some use of formal tools, and the market continues to grow. Nevertheless, some myths about formal persist, and they may still be deterring some engineers who could benefit from it. It’s time for the truth to be told.
The main attraction of a formal methodology is clear: Exhaustive analysis of a semiconductor design. Simulation provides only scattershot verification by its very nature. No matter how long simulation (or emulation) runs, only a tiny portion of possible design behavior will be exercised. Unverified scenarios may hide serious bugs.
Since formal verification is exhaustive, it considers all legal design behavior over all time throughout the entire design. It finds corner-case design bugs, but also proves that no bugs are remaining. It relies on assertions about intended design functionality and constraints to keep the analysis restricted to legal behavior. This ensures that no false “bugs” are found by violating the input rules or protocols for which the chip was designed.