FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines

TL;DR

FastLEC is a hybrid formal verification tool that combines multiple engines and strategies to significantly improve the efficiency and scalability of combinational equivalence checking for complex datapath circuits.

Contribution

It introduces a hybrid prover unifying SAT, BDD, and simulation engines with novel heuristics and strategies, achieving superior performance over existing tools.

Findings

Proves 5.07x more circuits than ABC &cec using 32 CPU cores.

Outperforms existing serial and parallel CEC provers by 3.33x and 2.67x in PAR-2 time.

Achieves an additional 4.07x speedup with GPU acceleration.

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.07x 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.33x and 2.67x in PAR-2 time, demonstrating an improvement of 74 newly solved circuits. With the addition of a single GPU, it achieves a further 4.07x improvement. The prover also demonstrates excellent scalability.