@article{WENG2007, 
author = {Yanling WENG and Haitong GE and Xiaolang YAN and Kun Ren},
title = {Arithmetic Operand Ordering for Equivalence Checking},
year = {2007},
journal = {Tsinghua Science and Technology},
volume = {12},
number = {S1},
pages = {235-239},
keywords = {synthesis, equivalence checking, arithmetic circuit},
url = {https://www.sciopen.com/article/10.1016/S1007-0214(07)70116-5},
doi = {10.1016/S1007-0214(07)70116-5},
abstract = {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.}
}