FastLEC: Parallel Datapath Equivalence Checking with Hybrid Engines

Lecture notes in computer science, pp. 89–108

Abstract

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.

Authors 4

1. Xindi Zhang

   Institute of Software · University of Chinese Academy of Sciences

   Affiliation as printed

   Key Laboratory of System Software (CAS), ISCAS, Beijing, China

   School of Computer Science and Technology, University of Chinese Academy of Science, Beijing, China

2. Furong Ye Aachen

   Leiden University

   Affiliation as printed

   LIACS, Leiden University, Leiden, The Netherlands

3. Zhihan Chen

   Institute of Software · University of Chinese Academy of Sciences

   Affiliation as printed

   Key Laboratory of System Software (CAS), ISCAS, Beijing, China

   School of Computer Science and Technology, University of Chinese Academy of Science, Beijing, China

4. Shaowei Cai corresponding

   Institute of Software · University of Chinese Academy of Sciences · Beihang University

   Affiliation as printed

   Key Laboratory of System Software (CAS), ISCAS, Beijing, China

   School of Computer Science and Technology, University of Chinese Academy of Science, Beijing, China

   School of Software, Beihang University, Beijing, 100191, China