Arithmetic Operand Ordering for Equivalence Checking
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.
synthesis equivalence checking arithmetic circuit
WENG Yanling GE Haitong YAN Xiaolang Ren Kun
Institute of Very Large Scale Integrated Circuits Design,Zhejiang University,Hangzhou 310027,China
国内会议
北京
英文
235-239
2007-07-15（万方平台首次上网日期，不代表论文的发表时间）