With Today's Designs, Timing and Function Matter

Timing closure has been the clarion call of the electronics industry for several years. If a design achieves timing closure, it is considered silicon-ready. The Electronic Design Automation (EDA) industry has jumped on this concept and met the demand by developing products designed to efficiently reach timing closure.

Timing closure is reached when the whole chip meets the timing specification or constraints. While timing closure is an important design consideration, it isn't the final consideration. Meeting timing closure often creates structural changes within a design, leading to functional problems. These problems are often introduced late in the design cycle, after creation of the original RTL specification and after larger portions of the netlist have been flattened.

Full-chip functional closure occurs when the whole chip meets the intended functional specification, usually expressed in a behavioral or 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.

Incorporating a formal-verification methodology into the design flow will ensure functional closure. Equivalence checking, part of a formal-verification methodology, automatically detects functional inconsistencies, providing a reliable way to ensure that the final design implementation does what the RTL code specifies. It uses mathematical techniques to determine whether one design representation is functionally equivalent to another. In essence, it verifies that the final netlist is correct.

Today's highest capacity equivalence checkers all operate in a similar manner. They first compile the designs, typically represented in either a netlist or RTL form, into a database representation of their functionality (a few tools on the market can actually read a transistor-level netlist). The checkers then find all of the inputs and outputs of the two designs and attempt to match them. The next step is to identify and attempt to correlate the state bits, or storage elements, of the two designs. Finally, they use a combination of arithmetic and automatic test-pattern-generation (ATPG) algorithms to exhaustively compare the combinatorial logic that resides between the state bits of the two designs. If functional differences are detected using these algorithms, counterexamples are generated to help debug the design.

The best equivalence checkers on the market have the most sophisticated algorithms. State-bit correlation algorithms must be fully automatic so that there is no need for user intervention. Combinatorial-logic comparison algorithms must handle major architectural differences, such as those faced when making RTL-to-netlist comparisons of multipliers. Algorithms must be fast and use minimal memory so that they can handle full-chip, multi-million-gate designs. Algorithms must be robust so that all blocks of a design can be verified reliably, even when faced with a broad variety of complex embedded structures. Finally, diagnosis algorithms must help the designer to quickly identify functional differences.

The equivalence checking capability fills a void in most verification flows—to ensure that the design's functionality has not been altered due to timing-closure optimizations. Equivalence checking can functionally verify an entire chip design from RTL to GDSII.

Previously, functional closure could be reached with gate-level simulation. That is no longer possible due to slow performance and inadequate coverage. Instead, equivalence checking offers a practical solution. By automatically detecting functional differences, with 100% coverage that requires no test vectors, equivalence checking enables design teams to achieve functional closure quickly and exhaustively.

Equivalence checking reduces or eliminates the need for lengthy gate-level simulation. If gate-level simulation is eliminated, designers must depend entirely on the results of RTL simulation to ensure their designs are correct. Without an exhaustive equivalence check to ensure that the RTL description matches silicon, the veracity of the RTL simulation results is in question.

Back-end netlist changes and manipulations performed today to reach timing closure have created a market for equivalence checkers that can verify these changes. Equivalence checkers that can reliably compare designs at the back-end stage to their respective original RTL specifications will gain acceptance. The use of both timing closure tools and equivalence checking ensures that both the timing and the function of a design have been thoroughly verified, achieving complete design closure.

Dino Caporossi is director of marketing at Verplex. Prior to joining Verplex, Caporossi held formal-verification marketing positions at Cadence Design Systems and Compass Design Automation. He has eight years of sales and marketing experience within the EDA industry and eight years of electronics design experience. Caporossi holds a Master's degree in Electrical Engineering from Johns Hopkins University and a Bachelor's degree in Electronics Engineering from the University of Maryland.