Functional verification is already "the" major design-phase bottleneck, and it will only get worse unless improvements in methodology and tools close the gap. The RTL synthesis revolution enabled the separation of function from timing within the verification domain. This allowed static timing tools and the attendant methodology to emerge and dominate.

Today, we are at the brink of another such separation. More "static" analysis methods and tools will be needed to close the verification gap that we will see with 200 million gate designs. Assertion-based verification (ABV) is an emerging set of technologies that holds the promise of partially closing this gap. ABV can be used for both static (formal) and dynamic (simulation) verification. ABV boosts productivity by increasing observability, improving coverage metrics, reducing debug time, and identifying more errors.

One form of static analysis, equivalence checking, combines the advantages of ABV with high performance and near 100 percent coverage. Whereas dynamic simulation covers nothing other than what the test suite asks for, equivalence checking is exhaustive by definition, because it is a static methodology based on mathematical proofs.

For the same reason, equivalence checking provides the level of performance needed for fast regression testing. For example, a leader in broadband networking equipment recently ran regressions of a 9.6 million-gate ASIC on a standard 32-bit Linux workstation implemented in a physical design flow. It took about an hour and a half to perform a gate-to-gate, first-to-final netlist verification of the entire system-on-chip implementation.

The same design would have been impossible to verify exhaustively using a dynamic simulator. It is simply impractical to run gate-level regressions even on a moderate size design using dynamic simulation. The speed and accuracy of equivalence checkers give designers the time and confidence to make last minute changes that improve the overall quality of their designs.

Equivalence checking is a key technology to closing the verification gap. But to fulfill its technological promise, equivalence checking tools must be enhanced to analyze, verify, and debug complex, multimillion-gate ASICs in their entirety.

Due to capacity limitations, most equivalence checking tools are not able to handle large designs without partitioning them. These first-generation tools must break up designs according to their hierarchical structure. In many situations, this is not acceptable because critical information is ignored.

This weakness of purely hierarchical equivalence checking methodologies is exacerbated as gate count grows. With increased design complexity, the verification distance — defined by the number of design transformations that occur between RTL synthesis and final sign off — becomes even more challenging in terms of tool capacity and performance. The verification distances associated with multimillion-gate designs require innovative solutions.

A new generation of tools must take advantage not only of advanced tool architectures and algorithms, but also of cutting-edge technologies, such as parallel computing. Architectural innovations that support parallel processing include:

• Minimum memory usage, limited only by the speed and capacity of the resident disk system.
• Multi-engine solve architecture that increases capacity and performance.
• Support for CPU servers and workstation networks for maximum throughput.
• Checkpoint/restart for flexible integration in regression farms.

The ability to distribute verification across a design-appropriate number of workstations will be essential to verify and debug these capacious designs with a meaningful level of accuracy. In fact, parallel computing eliminates the need to make the classic tradeoff between performance and capacity, even for gate counts in the tens of millions.

Robert Hum is vice president and general manager of the Design Verification and Test division for Mentor Graphics.