Best Effort: Shift Left Some Bugs (Levels 1, 2, and 3)
The primary goal of Best Effort Formal methods is to find some bugs earlier than simulation. Best Effort Formal can also provide resiliency benefits to a simulation strategy since some bugs missed by simulation may be found. Levels 1 to 3 can replace simulation in specialized areas, e.g., clock domain crossing, sequential equivalence checking, connectivity checking.
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 is used on a “best effort” basis to shift left some bugs and is not meant to replace simulation, e.g., the Formal Engineer is not accountable for bug escapes.
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 X cycles, i.e., deadlock properties.
ABV properties are written using SVA (SystemVerilog Assertions).
Exhaustive Formal: Sign-Off (Levels 4 and 5)
Exhaustive Formal Sign-Off’s primary goal is to exhaustively verify the DUT by catching all bugs, including high-impact corner-case bugs that simulation will always miss, earlier and faster than simulation, i.e., the Formal Engineer is accountable for bug escapes.
Formal Sign-Off is typically more cost-effective than simulation for most newly written RTL.
A popular target for Formal Sign-Off’s initial application is unproven, concurrent logic since post-silicon bugs are frequently root-caused to these “simulation-resistant” design areas. Concurrent logic overwhelms simulation and emulation with its enormous state space and extreme corner cases, making it difficult to close in “project time.”
Formal Sign-Off testbenches are written using SystemVerilog.
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. Once all bugs are found, the DUT is formally signed-off with proof that every bug has been found.
For Level 4 Formal, the DUT’s size is typically a block, module, or small IP. If the DUT is a larger IP, such as an IP designed by several people, the IP is broken into different DUTs. For example, a PCI Express IP designed by ten engineers might be broken into Physical Layer, Link Layer, and Transaction Layer DUTs.
Level 5: System Architecture Formal Sign-Off
Level 5 Formal aims 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.