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