Search papers, labs, and topics across Lattice.
This paper introduces a miter-aware mapping framework for Logic Equivalence Checking (LEC) that addresses performance bottlenecks caused by structural perturbations and XOR-dense regions. By utilizing a LUT-based miter formulation, the approach maintains critical structural correspondence and clarifies high-level logic relations, leading to significant improvements in SAT solver efficiency. The proposed method achieves up to a 92.1% reduction in solving time compared to state-of-the-art SAT solvers, highlighting the importance of integrating structural mapping with SAT reasoning for enhanced LEC performance.
A miter-aware mapping framework can slash SAT solving times by over 92% by aligning circuit structures with solver needs.
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.
