The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Miter-Aware LUT Mapping: Aligning Structure and Solvability for Efficient Logic Equivalence Checking
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 92.1 percent 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.
A copy is held
pdf, 1.7 MB. Not published — it may be under
copyright. The facts and links here are.
@misc{zhu2026miteraware,
title = {Miter-Aware LUT Mapping: Aligning Structure and Solvability for Efficient Logic Equivalence Checking},
author = {Jiaying Zhu and Zhengyuan Shi and Mengxia Tao and Kezhi Li and Min Li and Qiang Xu},
year = {2026},
}