数据路径组合等价性检查：混合扫描引擎与并行化
Datapath Combinational Equivalence Checking With Hybrid Sweeping Engines and Parallelization
AI总结：
针对数据路径电路组合等价性检查，提出混合SAT与EPS扫描引擎并动态选择，通过并行化实现显著加速，比现有工具快百倍以上。
摘要：
在微处理器IC设计中，经常需要优化执行各种算术运算的数据路径电路实现。组合等价性检查（CEC）在确保设计优化的正确性方面起着至关重要的作用。最流行的CEC算法基于SAT扫描，该算法利用SAT按拓扑顺序证明内部节点对的等价性，并合并等价节点。数据路径电路通常包含等价对，其传递扇入锥较小但XOR链密度较高，证明此类节点对对于SAT求解器来说非常困难。精确基于概率的模拟（EPS）适用于验证此类对，但由于内存成本，该方法不适用于具有许多主输入的对。我们首先降低了EPS的内存成本，并将其集成以改进SAT扫描方法。考虑到SAT和EPS的互补能力，我们设计了一种引擎选择启发式方法，根据XOR链密度在扫描过程中动态选择SAT或EPS。我们通过检测规律性减少不必要的引擎调用来进一步改进我们的方法。此外，我们并行化了HybridCEC的SAT和EPS引擎，从而产生了并行CEC证明器。在工业数据路径电路基准套件上的实验表明，我们的方法在几乎所有实例上都比最先进的CEC工具（即ABC &cec）快得多，在30%的实例上快100倍以上，在12%的实例上快1000倍以上。此外，我们方法的64线程版本实现了77倍加速。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
