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.
1. Formal verification can only be performed by PhDs.
This was largely the case for the early academic tools targeted at research projects rather than industrial applications. Today, proving end-to-end properties for large designs may require significant formal expertise, though not a PhD in mathematics. Moreover, many applications of formal analysis are being used every day by designers and verification engineers who have no special training. The tools, languages, and methodologies have all improved a great deal since the pioneer days.
2. It takes a lot of work to get results from formal tools.
This is another myth that applied to early tools, but is no longer the case. Electronic design automation (EDA) vendors offer a wide range of formal applications (apps) that run automatically on the design and deliver results immediately. These include such important verification challenges as connectivity checking, tracing clock and reset networks, avoiding propagation of unknown values, and analyzing the effects of random faults during chip operation.