| Abstract: |
Combinational Equivalence Checking (CEC) is a cornerstone of modern IC design and verification flows, with datapath circuits being among the most challenging to verify due to their dense XOR structures, which often hinder traditional SAT-sweeping methods. To overcome this, we integrate Exact Probability-based Simulation (EPS) with SAT solvers and propose a dynamic engine selection heuristic based on XOR chain density. Additionally, we parallelize both SAT and EPS engines to further accelerate verification. Experimental results on industrial benchmarks show that our approach achieves speedups of up to 100× on 40% of instances and over 1000× on 14%, with the parallel version scaling up to 70× using 64 threads. |