An XMG Based Equivalence Checking Algorithm for Large Bit-Width Multiplier Circuits

Combinational equivalence checking is an essential part of electronic design automation (EDA). Modern computers have an increasing proportion of arithmetic logic circuits, which poses challenges for traditional equivalence checking algorithms, especially when checking multi-bit logic circuits. An equivalence checking method based on XOR-majority graph (XMG) is proposed to address this issue. Firstly, a miter circuit is constructed using an XMG representation of the referenced design and the design to be verified. Secondly, a functional rewrite is performed on the XMG of the miter, in which the logic level and number of nodes are optimized. Finally, the Boolean satisfiability (SAT) solver and simulator are used to verify the final equivalence verification result. As compared to tools such as ABC and Lingeling, the algorithm performs 489 times CPU time speedup on average, and a maximum acceleration of 1472 times in validation time.