Formal Verification Capability Maturity Model
Demystifying “Formal Verification”
The Formal Verification Capability Maturity Model (Formal CMM) defines the progression of formal verification methodologies as “Levels”, thereby bringing much needed-precision to discussions about formal verification.
All five Formal CMM Levels are useful, but the goals, training, and tool requirements for each level are different.
Level 1 through Level 3: Time to First Bug
Level 1: Automatic Formal
Automatic Formal or “push-button formal” is convenient for RTL designers to leverage formal verification for:
- Sandbox verification,
- Sanity checks,
- X-propagation verification.
Level 2: Formal Apps
Formal Apps verify simple properties of a design in ways that require much less effort from the formal verification engineer than Assertion-Based Verification (Level 3). The most classic Formal App is clock domain crossing (CDC), but there are newer Apps such as connectivity verification and control and status register checking.
Level 3: Assertion-Based Verification
ABV provides some simple, yet important properties in the design that can be verified for all cases, such as:
- Two state machines cannot be in specific states at the same time,
- FIFOs are never written into when full,
- The design cannot remain in a given state for more than 12 cycles, i.e., deadlock properties.
Level 4 and Level 5: Time to Last Bug
Formal Sign-Off with Level 4 and Level 5 Formal delivers higher-quality designs much faster by focusing on blocks where the risk of post-silicon bug escapes is high.
Level 4: Block-Level Formal Sign-Off
Level 4 introduces end-to-end formal, which means the DUT is exhaustively verified and block-level simulation is completely replaced for that DUT. Level 4 catches all bugs including corner case bugs earlier and faster than simulation. Once all bugs are found, the DUT is formally signed-off with proof that every bug has been found.
For Level 4 Formal, the size of the DUT is typically a block or a module or a small IP. If the DUT is a larger IP, such as an IP designed by several people, then the IP is broken into different DUTs. For example, a PCI Express IP designed by 10 engineers might be broken into Physical Layer, Link Layer, and Transaction Layer DUTs.
Level 5: System Architecture Formal Sign-Off
The goal for Level 5 Formal is to prove that the system architecture is correct for specific requirements such as cache coherence or to prove that the system will not deadlock. System Architectural Formal Sign-Off requires significant effort and decomposition of the problem and is a new area of formal verification.