Tool lets you formally verify complex datapaths

Engineers developing timing-critical applications, such as graphics, multimedia, DSP, and communications, often require advanced datapath optimization. These circuits are difficult and sometimes impossible to formally verify with synthesis. Addressing these needs, Verplex Systems has released Conformal Datapath, which automatically verifies flat-datapath modules without requiring designers to specify boundaries or architectures in the flattened netlist. Datapath synthesis uses operator-merging techniques to produce faster and smaller circuits. Conformal Datapath can handle these circuits and use equivalence checking to formally verify them.

Conformal Datapath checks for proper pipeline implementation by ensuring that the latency of the presynthesis and postsynthesis designs is identical. Datapath synthesis can introduce carry-save transformations for sequences of address, multipliers, and registers. These transformations can cause register-matching problems in traditional formal verification. Conformal Datapath recognizes carry-save circuits and properly verifies them. The product supports HP-UX, Solaris, IBM AIX, and Linux operating systems. A three-year, time-based license costs $45,000 per year.

Verplex Systems, 1-408-586-0300, www.verplex.com.