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.

The 5 Levels of the Formal Verification CMM

Formal Verification CMM Levels

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,
  • Linting,
  • 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.
Typically, ABV is used on a “best effort” basis and is not meant to replace simulation.

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.

Complementary Strengths of Simulation and Formal Verification

Complementary Strengths: Chip-Level Impact of Formal CMM Levels

Formal Verification Sign-Off Methodology