Formal Tool Verifies Complex Datapaths

May 26, 2003
A tool's ability to verify compiled datapath blocks with equivalence checking ends the reliance on simulation as a stopgap measure.

Until now, verification of complex datapath blocks has been left to simulation, a strategy fraught with drawbacks. Debugging is difficult, and the overall quality of verification is lower than that seen by other parts of the design. In the end, there's increased risk of costly silicon respins due to missed bugs.

With the release of Conformal Datapath (DP), Verplex Systems changes that by bringing formal equivalence checking to bear on compiled datapath circuitry. With Conformal DP, designers of graphics, multimedia, DSP, and communications chips can exhaustively verify such circuits. It does so independently of "side files" passed clandestinely from the synthesis tool, ensuring that the formal-verification process doesn't rely on assumptions made during synthesis.

The tool handles a wide variety of datapath structures found in high-end designs. It can verify flat datapath structures without specifying boundaries or architectures in the flattened netlist. It also overcomes difficulties associated with automatic verification of merged operators, which in the past have prevented equivalence checking from working well on synthesized datapath circuits.

Conformal DP checks for proper pipeline implementation by ensuring the latency of the compiled design is correct. It can also verify circuits containing carrysave transformations, which have posed register-matching problems for equivalence checkers in the past.

Conformal DP is sold as an add-on to Verplex's Conformal Logic Equivalence Checker (LEC). A three-year, time-based license costs $45,600/year. Support is offered for HP Unix, Sun Solaris, IBM AIX, and Linux platforms.

Verplex Systems

See associated figure

Sponsored Recommendations


To join the conversation, and become an exclusive member of Electronic Design, create an account today!