On the Practice of Formal Verification
Many tools for end-to-end verification are powerful and productive. Yet the practice of formal verification of hardware RTL designs is mystifying: there are more builders of tools than full-time dedicated users of such tools. Surprising perhaps, except that few places teach the practical application of formal verification. This blog is dedicated to formal verification and methodology, driven by an in the trenches perspective and based on years of full-time experience with the application of formal verification.
RTL formal verification methods
The two most practical kinds of RTL formal verification solutions are model checking (MC) and RTL-vs-C equivalence checking (SEC).
Model checking proves a set of checkers (a.k.a. assertions) written in Verilog and SVA, against an RTL design. Commercial model checking tools include tools from the large EDA vendors, such as Cadence IFV/IEV, Mentor Graphics 0-In and Synopsys Magellan. Smaller startups also offer tools in this space: Averant Solidify, Jasper JasperGold, OneSpin MV and Real Intent Ascent.
Sequential Equivalence Checking
RTL-vs-C (sequential) equivalence checking is used to formally verify RTL designs against a reference C/C++ model. Only one large EDA vendor has a commercial RTL-vs-C equivalence checking tool: Synopsys Hector. There is another tool from a startup, Calypto SLEC.
When to Use Which Solution
The kinds of design where model checking is best applicable for verification, is typically a very different class of design than those where RTL-vs-C equivalence checking is the better choice. We will cover the suitability of different classes of designs to these techniques, in a later post.
It is worth noting that other RTL formal verification tools exist, such as theorem proving and symbolic trajectory evaluation. But these are only academic tools; no commercially available tools are available for these technologies.