
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.
FOS: Computer and information sciences, Logic in Computer Science, F.4.1; F.3.1; B.6.3; I.2.2; I.2.8; D.2.4, Logic in Computer Science (cs.LO)
FOS: Computer and information sciences, Logic in Computer Science, F.4.1; F.3.1; B.6.3; I.2.2; I.2.8; D.2.4, Logic in Computer Science (cs.LO)
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 0 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
