Datapath Combinational Equivalence Checking With Hybrid Sweeping Engines and Parallelization
Zhihan Chen, Xindi Zhang, Yuhang Qian, Shaowei Cai · ACM Transactions on Design Automation of Electronic Systems · 2025
Synthesizing circuits to achieve better PPA is crucial, particularly in datapath netlists with various arithmetic operators. The verification relies on the Combinational Equivalence Checking (CEC) techniques, checking the equivalence of two combinational circuits. Contemporary CEC tools commonly utilize SAT as the principal reasoning engine, employing a SAT-sweeping algorithm, which sequentially confirms the equivalence of internal pairs in topological order, merging verified equivalents to reduce the netlist’s scale. Nonetheless, datapath circuits frequently comprise pairs of nodes characterized by relatively limited transitive fan-in cones, yet these nodes display a pronounced density of XOR chains. This particular arrangement presents considerable obstacles for SAT solvers. To address this, exact probability-based simulation (EPS) provides an effective solution, but its high memory requirements limit its applicability. This article proposes a hybrid CEC prover, hybridCEC , and its parallel version, paraHCEC . Firstly, we decrease the memory requirements of the EPS method and integrate it into the SAT-sweeping framework. Secondly, we propose a dynamic engine selection heuristic for SAT and EPS, based on XOR chain density. Thirdly, we improve efficiency by identifying and reducing redundant engine calls by detecting regularity in the circuits. Finally, we parallelize the internal SAT and EPS engines, resulting in a highly efficient parallel CEC prover. Extensive experiments on industrial datapath circuit benchmarks demonstrate that our method significantly outperforms the state-of-the-art prover ABC “&cec”, achieving up to 100× speedups on 40% of instances and over 1000× speedups on 14%. Moreover, our 64-thread parallel version achieved an impressive 70× speedup, highlighting its scalability and effectiveness.