Functional Verification using Formal on Million Gate Designs

Verification engineers are the unsung heroes making sure that our smart phone chips, smart watches and even smart cars function logically, without bugs or unintended behavior. Hidden bugs are important to uncover, but what approach is best suited for this challenge?

With the Universal Verification Methodology (UVM) there’s the constrained-random approach that can find bugs that designers or verification engineers never thought of. The only downside of using constrained-random is the limitation to smaller DUTs, not covering all state spaces, missing corner-case bugs and not finding all Trojan paths.

So the good news is that adding formal verification tools can nicely complement traditional verification approaches by enabling:

• Exhaustively verifying all IO versus expected results for all states
• Million gate capacity

You may recall that early formal tools required a PhD user to get the best results, and that the learning curves were quite high. With time these obstacles have been addressed and overcome, so now there are formal apps that target specific goals:

• Clock Domain Crossing (CDC)
• Reset Domain Crossing (RDC)
• X-state propagation
• Finite State Machine (FSM) coverage
• Dead code analysis

Vendors like Mentor have been able to create such formal verification apps that automate these verification tasks, all while keeping a low learning curve. Here’s a list of verification challenges and formal apps available:

Verification Challenge	Formal App
Asynchronous clock failures	Formal CDC App – asynchronous boundary crossings.
Formal CDC-FX – metastability injection.	Formal RDC – reset domain crossings.
X-state propagation	Formal XCheck – identifies sources of X, possible propagations.
RTL structure	Formal AutoCheck – synthesis ready, undriven logic, unconnected ports, uninitialized regs, etc.
FSM design	Formal AutoCheck – FSM state reach, arcs, reachable blocks, driver logic, etc.
RTL code coverage	Formal CoverCheck – unreachable code.
AMBA bus protocols	Formal AMBA QFL – protocol compliance.
Secure data path	Formal Secure Check – confidentiality, integrity of secure data.
IP integration	Formal Connect Check – connectivity spec followed.
Register policies	Formal Register Check – control registers follow policy specs.

OK, so formal apps seem to be a good approach in theory to improve my functional coverage, but what do actual formal tool users experience.

FPGA Example

RTL and gate-level simulation passed, but testing the DUT in the lab showed unstable results, so they tried the Formal CDC app which uncovered some combinational logic before a synchronizer:

The timing waveforms for signal adat show that the signal is not stable when it’s being sampled by the bclkdomain, causing data-dependent timing errors.

The second logic error uncovered was the use of asynchronous resets:

Finally, formal uncovered synchronous de-asserts and missing synchronizers:

Formal CDC verification is now part of their standard verification flow, because without formal their old design review and verification methods missed all three of these failures.

Safety-Critical Design

A Triple-Mode Redundancy (TMR) design wasn’t “voting” properly, so the debug process took another four months to find the source using simulations and hardware debugging. When the team tried Questa PropCheck tool, just two properties were created and then the same bug was pinpointed in just 16 hours, what a big improvement.

Propagating X
All of the functional tests were passing, CDC analysis was run, and simulation used “x prop”, however the DUT was still failing. On closer examination their RTL simulator wasn’t propagating X correctly, as shown below when cond is X the else branch was taken:

Using the Formal X-Check app did uncover their unresolved Xs deep in the design.

Summary
Verification engineers have many tools and methods to reach coverage and verification goals, so adding formal apps that are easy to setup and run while having million gate capacity open up quicker time to market with higher confidence than other methods.

Read the complete 5 page White Paper from Mentor online.

Related Blogs

• Mentor at DVCon 2019
• Sequential Equivalency Checks in HLS
• Webinar: ASIC and FPGA Functional Verification Study

Share this post via:

• 
• 
• 
•