Simulation-Based Combinational Equivalence Checking With Multiple GPUs

Tianji Liu

doi:10.1109/tcad.2026.3661840

Simulation-Based Combinational Equivalence Checking With Multiple GPUs

2026-02-06

0

PRE

AI

T

Tianji Liu

E

Evangeline F. Y. Young

DOI：10.1109/tcad.2026.3661840

Original

Original request for help

Save

Abstract

En 中文

Combinational equivalence checking (CEC) is a fundamental problem in the realization flow of digital designs which is unlikely to have universally efficient algorithms due to its co-NP-completeness. Recent researches of CEC have been focusing on SAT sweeping, but novel methods are constantly needed since new and complex designs continue to emerge. This article provides a perspective other than SAT for tackling CEC, namely, exhaustive simulation, and presents a simulation-based CEC engine constructed with parallel algorithms that can be efficiently executed on multiple GPUs. The proposed multi-GPU CEC engine can solve 4 out of the 9 large cases in the experiments on its own, with up to $724.23\times $ speed-up compared with the checker in ABC. Moreover, a combination of the GPU engine and the ABC checker achieves averaged accelerations of $7.94\times $ over the standalone ABC checker and a commercial checker using a single A6000 GPU, and $15.01\times $ speed-up on average over the ABC checker with 4 A100 GPUs.

Keywords:

Combinational equivalence checking (CEC)

GPU

hardware formal verification

logic synthesis

multi-GPU algorithms

parallel computing

Simulation-Based Combinational Equivalence Checking With Multiple GPUs

Abstract

Journal

Organization

Cited Papers