Abstract Combinational equivalence checking (CEC) remains a challenge EDA task in the formal verification of datapath circuits due to their complex arithmetic structures and the limited capability or scalability of SAT, BDD, and exact-simulation (ES) based techniques when used independently. This work presents FastLEC , a hybrid prover that unifies these three formal reasoning engines and introduces three strategies that substantially enhance verification efficiency. First, a regression-based engine-scheduling heuristic predicts solver effectiveness, enabling more accurate and balanced allocation of computational resources. Second, datapath-structure-aware partitioning strategies, along with a dynamic divide-and-conquer SAT prover, exploit the regularity of arithmetic designs while preserving completeness. Third, the memory overhead of ES is significantly reduced through address-reference-count tracking, and simulation is further accelerated through a GPU-enabled backend. FastLEC is evaluated across 368 datapath circuits. Using 32 CPU cores, it proves 5.07 $$\times $$ × more circuits than the widely used ABC &cec tool. Compared with the latest best datapath-oriented serial and parallel CEC provers, FastLEC outperforms them by 3.33 $$\times $$ × and 2.67 $$\times $$ × in PAR-2 time, demonstrating an improvement of 74 newly solved circuits. With the addition of a single GPU, it achieves a further 4.07 $$\times $$ × improvement. The prover also demonstrates excellent scalability.

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.

In modern digital circuit design, verifying the equivalence of arithmetic circuits is a significant and challenging task. This paper introduces a new circuit solver based on the Conflict-Driven Clause Learning (CDCL) algorithm, which integrates structural elimination techniques to reduce the number of variables and clauses while maintaining the circuit structure. Additionally, branching heuristics have been enhanced specifically for the structure of arithmetic circuits. Experimental results demonstrate that X-SAT significantly outperforms best previous circuit solver could be found on all benchmarks. Further, X-SAT performs better than the state-of-the-art CNF-based SAT solvers on complex arithmetic circuits, underscoring its significant potential in the field of circuit design verification.

In the application of IC design for microprocessors, there are often demands for optimizing the implementation of datapath circuits, on which various arithmetic operations are performed. Combinational equivalence checking (CEC) plays an essential role in ensuring the correctness of design optimization. The most prevalent CEC algorithms are based on SAT sweeping, which utilizes SAT to prove the equivalence of the internal node pairs in topological order, and the equivalent nodes are merged. Datapath circuits usually contain equivalent pairs for which the transitive fan-in cones are small but have a high XOR chain density, and proving such node pairs is very difficult for SAT solvers. An exact probability-based simulation (EPS) is suitable for verifying such pairs, while this method is not suitable for pairs with many primary inputs due to the memory cost. We first reduce the memory cost of EPS and integrate it to improve the SAT sweeping method. Considering the complementary abilities of SAT and EPS, we design an engine selection heuristic to dynamically choose SAT or EPS in the sweeping process, according to XOR chain density. Our method is further improved by reducing unnecessary engine calls by detecting regularity. Experiments on a benchmark suite from industrial datapath circuits show that our method is much faster than the state-of-the-art CEC tool namely ABC ‘&cec’ on nearly all instances, and is more than 100× faster on 30% of the instances, 1000× faster on 12% of the instances.