Publications
Sort:
Issue
Arithmetic Operand Ordering for Equivalence Checking
Tsinghua Science and Technology 2007, 12(S1): 235-239
Published: 01 July 2007
Abstract PDF (95.5 KB) Collect
Downloads:0

An information extraction-based technique is proposed for RTL-to-gate equivalence checking. Distances are calculated on directed acyclic graph (AIG). Multiplier and multiplicand are distinguished on multiplications with different coding methods, with which the operand ordering/grouping information could be extracted from a given implementation gate netlist, helping the RTL synthesis engine generate a gate netlist with great similarity. This technique has been implemented in an internal equivalence checking tool, ZD_VIS. Compared with the simple equivalence checking, the speed is accelerated by at least 40% in its application to a class of arithmetic designs, addition and multiplication trees. The method can be easily incorporated into existing RTL-to-gate equivalence checking frameworks, increasing the robustness of equivalence checking for arithmetic circuits.

Total 1