Miter-Aware LUT Mapping: Aligning Structure and Solvability for Efficient Logic Equivalence Checking
For hardware verification engineers, this work addresses the critical bottleneck of LEC by improving solver efficiency through better problem formulation.
Logic Equivalence Checking (LEC) is bottlenecked by structural perturbations and XOR-dense regions. The authors propose a miter-aware LUT mapping framework that reduces SAT solving time by up to 92.1% across state-of-the-art solvers.
Logic Equivalence Checking (LEC), a fundamental hardware verification task, is often bottlenecked by synthesis-induced structural perturbations and XOR-dense regions that degrade SAT solver performance. We contend that the modeling of the miter is as critical as the SAT solver itself. To this end, we introduce a miter-aware mapping framework that strategically formulates the problem before solving. By constructing a LUT-based miter -- instead of a traditional, flat netlist -- our approach preserves critical structural correspondence between the two designs while making high-level logic relations explicit. Our framework uniquely integrates three techniques: equivalence-preserving mapping to structurally align the two circuits, Gaussian-guided XOR modeling to algebraically simplify dense arithmetic, and solver-oriented LUT selection to generate a representation optimized for efficient SAT reasoning. Evaluated on comprehensive datasets, our method achieves up to a \textbf{92.1\%} reduction across state-of-the-art SAT solvers. This demonstrates that a solver-aware modeling paradigm, which unifies structural mapping with SAT reasoning, can fundamentally enhance LEC efficiency.