{"ID":6138158,"CreatedAt":"2026-07-09T01:07:32.349475501Z","UpdatedAt":"2026-07-11T08:45:50.451512195Z","DeletedAt":null,"paper_url":"https://arxiv.org/abs/2607.07164","arxiv_id":"2607.07164","title":"Miter-Aware LUT Mapping: Aligning Structure and Solvability for Efficient Logic Equivalence Checking","abstract":"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.","short_abstract":"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-...","url_abs":"https://arxiv.org/abs/2607.07164","url_pdf":"https://arxiv.org/pdf/2607.07164v1","authors":"[\"Jiaying Zhu\",\"Zhengyuan Shi\",\"Mengxia Tao\",\"Kezhi Li\",\"Min Li\",\"Qiang Xu\"]","published":"2026-07-08T08:56:24Z","proceeding":"cs.AR","tasks":"[\"cs.AR\",\"cs.LO\"]","methods":"[]","has_code":false}