In a Jan. 10 announcement of new Silicon Realization verification capabilities, Cadence has promised to "extend metric-driven verification from digital simulation to formal model checking." Here's some more detailed information about what that means and how it can help design and verification engineers meet their verification goals.
Many IC design teams use metric-driven verification (MDV) for simulation. The concept is simple; you capture your verification intent in an executable verification plan (vPlan), and as verification progresses you track coverage metrics, most notably code coverage and functional coverage. The plan can also track assertions, checks, and time-based data points. This makes it possible to determine when high-quality verification closure has been achieved, answering the toughest of all verification questions, "am I done yet?"
The four stages of MDV - plan, execute, measure, and react - are depicted in the diagram below. A recent Cadence whitepaper provides more information about MDV.
Speaking Different Languages
To date, however, MDV has generally been limited to simulation. Separate teams typically tackle formal verification, and if they achieve a partial or complete proof on a block, this may not be reflected in the verification plan. The end result may be a lot of unnecessary or redundant simulation. Avoiding that extra work is a key motivation for extending metric-driven verification to formal model checking.
In a recent Q&A interview Alok Jain, who directs Cadence's R&D efforts in formal verification, noted that formal coverage metrics and simulation coverage metrics are very different. With formal coverage, you are trying to understand how good your constraints are or how complete your proof is. The "metrics" used for these purposes are often fairly crude or ad-hoc, and have seen limited use.
In the simulation world, code coverage and functional coverage are widely used. There is no clear connection to formal coverage. Alok noted that "formal and simulation speak two different languages as they describe different aspects of the verification intent." One goal of the new Cadence verification announcement is to get formal and simulation technologies to speak the same language.
Speaking One Language
How can this be done? The new Cadence verification solution uses formal analysis in the Incisive Enterprise Verifier to generate simulation metrics. Formal analysis generates a witness trace for coverage points in the design. A witness trace is a sequence of values that ensures a coverage point can be hit. This witness trace can then be replayed in the Incisive Enterprise Simulator. This approach generates stimulus that can activate coverage points, and determines whether coverage points are reachable.
"So to put it another way," Alok said, "Incisive Enterprise Verifier has become a smart testbench generator. You generate testbenches that can hit all your functional coverage points. You replay these testbenches in the simulator and get simulation-oriented metrics."
With this connection, the verification plan can add two elements: the reachability of coverage points, and the proofs provided by formal analysis. As Alok noted, simulation alone can't exhaustively prove an assertion -- it can only track whether it passes or fails. Formal analysis can provide a complete proof by ensuring that there is no possible counter-example.
In support of the new capabilities, the vPlan provided by Incisive Enterprise Manager can track coverage point hits from both simulation and formal engines, and has added a column that shows whether coverage points are reachable.
Another Step Toward Silicon Realization
So what does all this have to do with Silicon Realization? Recall that the EDA360 vision of Silicon Realization calls for holistic solutions based on three requirements -- unified intent, abstraction, and convergence. "Intent" applies to verification as well as design, and metric-driven verification provides a way to represent verification intent and then monitor progress towards it. Now that capability has been extended into the formal realm. The end result will be greater convergence on that perennial question, "am I done yet?"