Datapath Combinational Equivalence Checking With Hybrid Sweeping Engines and Parallelization

TL;DR

This paper introduces a hybrid and parallelized approach for combinational equivalence checking in datapath circuits, combining SAT and EPS methods with dynamic engine selection and regularity detection, significantly improving speed and efficiency.

Contribution

The paper presents a novel hybrid engine that dynamically combines SAT and EPS techniques with parallelization and regularity detection for faster CEC in datapath circuits.

Findings

Significantly faster than state-of-the-art tools on industrial benchmarks.

Over 100x speedup on 30% of instances.

77x speedup with 64-thread parallelization.

Abstract

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. Furthermore, we parallelized the SAT and EPS engines of HybridCEC, leading to the parallel CEC prover. 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 100x faster on 30% of the instances, 1000x faster on 12% of the instances. In addition, the 64 threads version of our method achieved 77x speedup.