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.