The struggle for timing closure has grabbed most of the headlines lately, but achieving functional closure has always been at least as difficult. From 1999 Electronic Design Automation (EDA) Consortium reports, nearly a half-billion dollars was spent on software primarily used to verify functionality, making it the single biggest market segment within EDA. This segment surpasses both logic synthesis, ASIC and IC implementation tools.
Timing closure is achieved when the whole chip meets the timing specification or constraints. Analogously, functional closure occurs when the whole chip meets the intended functional specification, usually expressed in a behavioral or register-transfer level (RTL) description. Just as static timing analysis is the tool of choice for verifying timing closure, formal verification is essential in verifying functional closure. It is faster than simulation, requires no vectors and is exhaustive so more bugs are caught earlier when they take less time to fix.
Timing-closure verification is enabled by the full-chip capacity of static timing analysis tools. For example, it is not helpful to know that 90 percent of a chip's timing has been verified but the remaining 10 percent is undetermined. In that respect, full-chip capacity of formal tools is also important to functional closure. Without it, a percentage of logic remains unverified that might not correctly interface with the rest of the chip.
The effort to achieve functional closure happens in two stages: design-intent validation and implementation verification. Design-intent validation occurs when the designer is checking to ensure that the design will work correctly for its intended purpose. Today, simulation-based technology predominates for that purpose but, as design complexities continue to increase, adequate coverage is not possible and run-times grow long.
Model checkers are a powerful supplement to simulation for design validation, using exhaustive mathematical techniques to determine whether a design is exhibiting the correct functional behavior. Early model checkers were limited to impractical blocks of a few thousand gates, however. That is changing.
Later in the cycle, during implementation, the goal is to create a final netlist functionally identical to the original "golden" RTL design. Today, most design starts exceeding half a million gates are using equivalence checking for implementation verification.
The best equivalence checkers today provide full-chip capacity from RTL to the gate level, even when all these structural dissimilarities are present.
The next great movement in formal verification will be toward design-intent validation.
Dino Caporossi is Director of Marketing for Verplex Systems Inc. (Milpitas, Calif.).
RSS
RSS| 
Digital| 
Mobile
