1 Introduction↩︎

Logic Equivalence Checking (LEC) [1] proves that a golden design and its implementation compute identical Boolean functions. The de facto LEC pipeline builds a miter by connecting the outputs of two designs through XOR gates and checks whether the miter can ever evaluate to \(1\). This turns equivalence checking into a single Boolean satisfiability (SAT) problem [2], and the approach has scaled thanks to modern SAT solvers [3]–[5] and solver heuristics [6]–[9].

However, two challenges limit the robustness of such pipeline on complex designs. First, logic synthesis (e.g. rewriting [10], resubstitution [11] and decomposition [12]) can significantly perturb logic cones and obscure matchable points between the miter’s two sides. The resulting lack of recognizable internal equivalences inhibits functional merging, a key simplification step shrinking the SAT instance within solvers [13], [14]. Second, many real-world designs contain XOR-dense modules, such as arithmetic units and cryptographic units. Unfortunately, modern SAT solvers relying on the search-backtracking algorithm [15] poorly handle constraints derived from XOR chains, deducing a literal typically requires almost all inputs fixed and terminating searching branch after verbose decisions [16]–[18].

Although prior efforts attempt to simplify the SAT instances before solving [19]–[21], operating solely on the flattened miters remains insufficient. We attribute that LEC efficiency is determined largely by how the miter is modeled before solving. Rather than simply constructing a conventional miter and hoping the solver compensates, we advocate a modeling strategy that preserves structural correspondence and exposes strong implications prior to SAT.

In this work, we propose a novel mapping-based LEC formulation that constructs a simplified Look-up Table (LUT)-based miter (see Figure 1) instead of directly linking the two netlists at the bit level. By mapping both designs to LUT abstraction, our approach preserves more internal identical cones, makes XOR structure explicit, and reduces solving complexity. We realize this agenda through three contributions:

• An equivalence-preserving LUT mapping algorithm that actively aligns corresponding subgraphs across the two designs, forming more internal equivalent logic between implementation and golden designs.

• A Gaussian-guided XOR modeling mechanism that detects XOR-dense area, implements with the LUTs representing XOR logic, and leverages Gaussian elimination [22], [23] to extract explicit affine relations.

• A solver-oriented LUT selection criterion within the mapping algorithm that quantifies the solver-friendliness to minimize overall SAT solving difficulty.

We implement the proposed framework on top of a standard miter-based LEC flow and evaluate it using both structurally optimized and arithmetic-heavy benchmarks. Experimental results demonstrate that our complete framework achieves up to 92.1% reduction across solvers, with an 83.3% average improvement over the baseline under the PAR2 metric. Ablation results further show that the miter-aware mapping alone reduces runtime by 62.5%, while the Gaussian-guided XOR modeling mechanism alone yields a 36.8% reduction. Overall, our method can systematically reshape the problem representation—bridging LUT-mapping and SAT reasoning into a unified framework that delivers more compact CNFs and scalable equivalence checking performance.

In summary, this work introduces a solver-aware modeling paradigm for LEC that unifies miter-aware mapping, algebraic simplification, and solver-oriented LUT selection. Rather than introducing a new mapping framework, we embed SAT/LEC-specific insights into standard LUT mapping so the resulting abstraction is solver-friendly rather than merely structurally compact. This approach marks a significant departure from recent works [20], [21] that apply LUT mapping to single-circuit SAT problems. While their methods optimize an individual netlist, our core contribution is the joint mapping of both golden and implementation circuits. This strategy is designed to explicitly preserve and rediscover the internal equivalences often obscured by synthesis—a challenge unique to equivalence checking. Consequently, the proposed framework not only improves practical verification efficiency but also forges a conceptual bridge between circuit optimization and SAT solving.

2 Related Work↩︎

2.1 Logic Equivalence Checking↩︎

Logic Equivalence Checking (LEC) is a cornerstone of formal verification in EDA, aiming to ensure that two circuits, typically before and after synthesis, implement the same Boolean function [24]. The standard approach is to build a miter circuit by XORing corresponding outputs and ORing all XOR results together. Unsatisfiability of the resulting miter indicates functional equivalence.

Typically, when two designs share a high degree of structural correspondence, equivalence points (i.e., functionally identical node pairs) can often be detected, making the miter instance of LEC easy to solve. However, aggressive logic synthesis disrupts the structural similarity [10]–[12], [25] but retain the hard-to-solve regions (i.e., XOR-dense regions) [16]–[18]. Recent efforts apply preprocessing to the flattened miter to simplify the SAT instance prior to solving [20], [21], yet overlooking the inherent cross-design correlations between the golden and implementation sides. Another line of research combines multiple engines, such as simulation-guided engine [26], [27] or non-SAT alternatives [28], to solve the miter instance. While effective on certain classes of designs, these methods still rely heavily on favorable problem features and initial decisions. In contrast to operating solely on a flattened miter, our work targets the initial modeling stage of LEC, reconstructing similar structure and neutralizing hard-to-solve regions before SAT solving.

2.2 Look-up Table (LUT) Mapping↩︎

Look-up Table (LUT) mapping is a fundamental step in logic synthesis, where a Boolean network is decomposed into a network of \(k\)-input LUTs for FPGA [29]. In a typical mapping procedure, the circuit is traversed in an output-to-input direction. For each node, multiple candidate LUTs are enumerated based on feasible input cuts and their corresponding Boolean functions, and the most suitable one is selected to optimize delay and latency. Recently, it has also attracted attention as a structure-preserving abstraction for SAT solving, where multiple logic gates are packed into solver-friendly LUTs to reduce CNF size and improve clause locality [20], [21]. Each LUT encapsulates a small truth table, offering flexibility for customized encoding strategies and fine-grained control over structural granularity.

The SAT-solving advantage of LUT-based abstraction arises from its ability to preserve local functional coherence [14], [21]. By grouping strongly related logic signals into a single LUT, the circuit representation becomes more compact and semantically cohesive, which helps remove redundant variables and clauses in the resulting CNF. Moreover, each LUT inherently defines a deterministic mapping between its inputs and output, enabling stronger inferences once partial assignments are known. This leads to more concentrated propagation, shorter implication chains, and overall improvement in solver efficiency.

However, existing approaches primarily target single-circuit optimization and overlook miter-specific structural patterns that arise in equivalence checking. Our work extends this line of research by performing miter-aware, solver-friendly LUT mapping, jointly considering structural alignment, XOR reasoning, and CNF-level propagation properties.

3 Methodology↩︎

3.1 Overview↩︎

Given the golden design (G) and implementation design (Imple. Design, I) in an LEC problem, our framework formulates it into an easy-to-solve SAT instance. As shown in Figure 1, our framework targets three objectives:

1. Preserve structural correspondence across the two sides of the miter, facilitating equivalence identification and functionally reduction.

2. Gaussian-guided XOR modeling to uncover the underlying affine relations among XOR variables and inject into the final CNF.

3. Select solver-friendly LUTs guided by multi-dimensional metrics that correlate with efficient branching, propagation, and conflict analysis.

3.2 Equivalence-preserving LUT Mapping↩︎

To mitigate the synthesis-induced structural perturbations, we introduce a miter-aware LUT mapping scheme (Figure 2) that explicitly reconstructs structural correspondence between the two sides of the miter. In a typical mapping procedure, the circuit is traversed in an output-to-input direction; for each node, multiple candidate LUTs are enumerated from feasible input cuts and their corresponding Boolean functions, and the most suitable one is selected to optimize delay. Building upon this standard process, our mapping identifies XOR/XNOR structures near the primary outputs as natural comparison anchors between the golden and implementation circuits. The two fan-in nodes of these XOR gates serve as the respective boundaries of the two sides, providing an approximate yet practical alignment even after aggressive synthesis.

Starting from these boundary anchors, our mapper proceeds recursively to generate and match LUT candidates on both sides. At each level, we create paired LUTs from nodes exhibiting structural similarity. This similarity is measured using a heuristic that combines topological depth, fan-in/fan-out counts, and the functional hash of the immediate logic cone. Such matched mapping preserves functional equivalences that would otherwise be obscured by synthesis transformations. While SAT-sweeping [26], [27] detects equivalences via repeated SAT queries, our alignment provides a lightweight, orthogonal structural matching that complements such solver-based techniques without their computational cost.

It is worth noting that LUT mapping inherently absorbs a group of primitive gates into each LUT, leaving only the LUT’s input and output variables exposed in the final CNF. Consequently, variables corresponding to internal gates disappear once absorbed. When mapping is guided to preserve equivalence points as LUT input or output boundaries, these equivalence variables remain explicit in the CNF and can be more effectively exploited by the solver’s redundancy elimination mechanisms [2]. Moreover, equivalence points located closer to the primary outputs enable earlier clause subsumption and stronger pruning within the search space, amplifying solver efficiency.

If no direct correspondence can be found for a node pair—e.g., due to heavy resubstitution or decomposition—we independently select LUTs on each side according to the solver-friendliness metric introduced in Sec 3.4, maintaining comparable structural granularity across designs. The resulting LUT network thus achieves improved symmetry, enhanced clause reuse, and stronger implication propagation, effectively bridging structural matching and solver-oriented optimization.

3.3 Gaussian-guided XOR Modeling↩︎

XOR-dominated circuits—such as arithmetic and cryptographic designs—pose major challenges to CDCL-based SAT solving, since their CNF encodings often require a large number of clauses and provide weak unit propagation.

To this end, we first detect XOR relations within the AIG network and perform Gaussian elimination (GE) over the finite field GF (2) within XOR-dense regions. Each XOR gate represents an equation among variables. To construct equations with constant right-hand sides, we leverage simple transformations:

• \(x_1 \oplus x_2 = x_3 \;\Rightarrow\; x_1 \oplus x_2 \oplus x_3 = 0\)

• \(x_1 \odot x_2 = x_3 \;\Rightarrow\; x_1 \oplus x_2 \oplus x_3 = 1\)

where \(\oplus\) denotes XOR, \(\odot\) denotes XNOR.

For example, given the XOR relations:

\[\begin{align} x_1 \oplus x_2 \oplus x_3 \oplus x_5 &= 1,\\[-3pt] x_1 \oplus x_2 \oplus x_4 &= 1,\\[-3pt] x_2 \oplus x_3 \oplus x_5 &= 1,\\[-3pt] x_1 \oplus x_4 \oplus x_5 &= 0,\\[-3pt] \end{align}\]

performing elementary row transformations yields: \[\begin{align} x_1 \oplus x_2 \oplus x_5 &= 1,\\[-3pt] x_1 \oplus x_3 &= 0,\\[-3pt] x_2 \oplus x_4 &= 1,\\[-3pt] x_4 \oplus x_5 &= 0. \end{align}\]

Unlike conventional elimination that substitutes away variables, we selectively retain XOR-related LUTs whose variables participate in nontrivial affine relations discovered by Gaussian elimination. These LUTs are explicitly reconstructed as standalone XORs rather than merged into larger logic cones, ensuring that their participating variables remain visible and semantically linked in the final representation. Concretely, each affine relation derived from GE is directly instantiated as an XOR LUT connecting the involved variables, thereby materializing the linear dependency within the mapped circuit itself.

For circuit-based solvers, this explicit construction enables early identification of XOR structures and reduces intermediate branching and propagation effort. For CNF-based solvers, the preserved XOR LUTs naturally translate into small XOR substructures during CNF conversion, allowing the solver to recognize and leverage these dependencies for stronger propagation and redundancy elimination  [14]. Overall, our approach integrates Gaussian-derived affine relations into the circuit as explicit XOR logic, ensuring their visibility across abstraction levels and improving both propagation and clause-level simplification.

3.4 Solver-oriented LUT Selection↩︎

For regions not dominated by XOR structures, we perform LUT implementations guided by a solver-friendliness metric.

1) Branching efficiency: These metrics capture how easily the solver can explore and prune the search space around \(L\).

1. Branch count: We measure how compactly \(L\) partitions the input space into regions with fixed output. Formally, a branch is a pattern \(p\in\{0,1,x\}^{|I|}\) (where \(x\) denotes “don’t care”) such that every assignment covered by \(p\) produces the same output. Let \(\mathrm{bc}(L)\) be the minimum number of such patterns needed to cover all satisfying assignments of \(L\). We normalize by the input space size: \[f_{\text{branch}}(L)=\frac{\mathrm{bc}(L)}{2^{|I|}}.\] Intuitively, a smaller branch count indicates that the function can be characterized by fewer consistent input regions, implying that decisions on input literals more rapidly constrain the search space. From the SAT-solving perspective, such functions yield simpler decision trees, shorter BCP chains, and fewer case splits during clause learning, thus improving solver convergence. For example, a 2-input AND can be covered by three branches (see Table ¿tbl:tab:and-branches?), while XOR requires four fully specified minterms, hence AND yields a lower \(f_{\text{branch}}\) and is considered more solver-friendly.

   

   

2. Sensitivity: Sensitivity reflects how reactive \(L\) is to single-bit flips. For each input assignment \(a\in\{0,1\}^{|I|}\) and each input bit \(i\), we flip bit \(i\) to obtain \(a\oplus e_i\) and check whether the output changes. Let \(T_L(\cdot)\) be the Boolean function implemented by \(L\). We define \[\mathrm{SensCount}(L)= \sum_{a\in\{0,1\}^{|I|}}\sum_{i=1}^{|I|} 1_{(T_L(a)\neq T_L(a\oplus e_i))},\] and normalize by the total number of flip trials: \[f_{\text{sensitivity}}(L)= \frac{\mathrm{SensCount}(L)}{|I|\cdot 2^{|I|}}.\] Lower \(f_{\text{sensitivity}}\) indicates locally stable behavior and typically leads to a narrower effective branching space for CDCL-based solvers.

2) Propagation strength. CDCL relies on Boolean Constraint Propagation (BCP)-partial assignments should force additional literals quickly.

1. Determinacy: Let \(V=\{x_1,\dots,x_{|I|},O\}\) be LUT inputs and output. For each non-empty subset \(S\subseteq V\), enumerate partial assignments \(a_S\) on \(S\) and test whether remaining variables \(V\setminus S\) become uniquely determined. Let \(1_{\text{det}}(S,a_S)\) be 1 if so and 0 otherwise. We define \[\mathrm{DetCount}(L)= \sum_{\substack{S\subset V\\ S\neq\emptyset}} \sum_{a_S\in\{0,1\}^{|S|}} 1_{\text{det}}(S,a_S),\] \[f_{\text{det}}(L)= \frac{\mathrm{DetCount}(L)}{\sum_{S\subset V,\,S\neq\emptyset} 2^{|S|}}.\] Higher \(f_{\text{det}}\) means partial assignments tend to collapse the remaining degrees of freedom, enabling stronger BCP.

2. Monotonicity: \(T_L\) is monotone if for any \(a,b\in\{0,1\}^{|I|}\) with \(a_i\le b_i\) for all \(i\), we have \(T_L(a)\le T_L(b)\). Monotone functions typically translate into Horn-like CNFs with few negative literals, which in turn yield shorter propagation chains and more localized learned clauses, improving solver efficiency [30], [31]. Non-monotone functions (e.g., XOR) tend to generate balanced positive/negative clauses that weaken unit propagation.

3) Conflict interpretability. We also favor LUTs whose conflicts are easy to explain locally. For any non-empty \(S\subseteq V\) and partial assignment \(a_S\), we ask whether \(a_S\) is infeasible, i.e., no full assignment extending \(a_S\) is consistent with \(T_L\). Let \(1_{\text{conf}}(S,a_S)=1\) if \(a_S\) is infeasible and \(0\) otherwise. We compute \[\mathrm{InterpCount}(L)= \sum_{\substack{S\subset V\\ S\neq\emptyset}} \sum_{a_S\in\{0,1\}^{|S|}} 1_{\text{conf}}(S,a_S),\] \[f_{\text{interp}}(L)= \frac{\mathrm{InterpCount}(L)}{\sum_{S\subset V,\,S\neq\emptyset} 2^{|S|}}.\] A higher \(f_{\text{interp}}\) means conflicts emerge from small local contexts, which leads to shorter learned clauses and faster convergence.

4) Structural compactness. Finally, we estimate how much internal logic a LUT absorbs from its fan-in cone, i.e., how many primitive logic gates (AIG nodes) are required to realize the Boolean function implemented by a \(L\). We approximate this count by performing a sum-of-products–based minimization that derives prime implicants from the truth table [32], [33]. A larger gate count implies that the LUT encapsulates more local logic and thus eliminates more intermediate signals during mapping. To ensure comparability across different input sizes, the score is normalized as \[f_{\text{compact}}(L)=\frac{|I|}{\mathrm{GateCount}(L)},\] where a smaller value indicates stronger logic absorption and fewer CNF variables introduced.

Complexity and reusability. Although metrics like \(\text{DetCount}(L)\) and \(\text{InterpCount}(L)\) require enumerating variable subsets and partial assignments, the cost is negligible since only 2/3/4-input LUTs are used. All scores are precomputed offline (in five seconds) and cached for reuse, introducing no overhead in synthesis or solving.

Cost aggregation and weight learning. The overall LUT cost combines each metric \(f_i(L)\) with Bayesian-optimized [34] weight \(w_i\), tuned on a small validation set to minimize solving time: \[\text{Cost}(L)=\sum_i w_i f_i(L).\] While the weight \(w_i\) is tuned on a subset, the results are robust across all validation sets. Propagation (\(f_{\textit{det}}\)) and branching (\(f_{\textit{branch}}\)) metrics dominate, confirming that strong BCP and effective search partitioning are key to solver efficiency. Their relative emphasis (higher \(f_{\textit{det}}\) for SAT, higher \(f_{\textit{branch}}\) for UNSAT) aligns with the distinct behaviors of satisfaction and proof-oriented solvers.

4 Experiments↩︎

4.1 Experiment Setting↩︎

We construct a comprehensive benchmark suite to evaluate the efficiency of our proposed LEC formulation framework. This suite includes the circuit pairs derived from industrial LEC problem and the instances built from public sources: ForgeEDA [35], ITC99 [36], EPFL [37], and Opencore [38]. To build the equivalent circuit pairs, each circuit is synthesized and conjunctive with the original one to form a miter. To build the inequivalent circuit pairs, we introduce small functional perturbations by randomly modifying a few nodes in the synthesized AIGERs before miter construction.

All circuits are synthesized with ABC [29], and LUT networks are generated using a customized cost-driven mapper built on Mockturtle [39], restricted to 2-, 3-, and 4-input LUTs, since larger LUTs (i.e., \(\ge\)​5 inputs) would produce exponentially more complex CNF encodings (\(2^n\) clauses) and thus hinder subsequent SAT solving. Each instance runs on a single Intel(R) Xeon(R) Platinum 8375C core with a 3,600 seconds timeout.

4.2 Main results↩︎

To validate the effectiveness of our proposed framework, we compare the solving time of LEC instances formulated by our framework (Ours) and the baseline flow (Baseline). The performance is measured using average PAR2 score, where any instance failing the 3,600s timeout is penalized with 7,200s. The PAR2 score for “Ours” includes both solving time and LUT mapping runtime, where the formulation overhead accounts for \(< 10\%\). Besides, we also record the number of solved instance within 3,600s time limit as #Solved.

After formulating SAT instance of the given LEC problem, we employ two state-of-the-art CNF-based SAT solvers (Kissat [3] and CaDiCaL [4]), two circuit-based SAT solvers (X-SAT [21] and CSAT [5]) and an advanced LEC engine (command cec in ABC [29], denoted as CEC in Table 1), respectively. It should be noted that the LEC engine performs functional reduction (e.g., SAT-sweeping [26]) and invokes CNF-based modern solver for final checking. Since CEC constructs the miter and translates it to CNF before calling solver, our approach is seamlessly inserted as a plugin-like pre-CNF optimization layer.

The results are summarized in Table 1, from which three key observations emerge. First, our framework consistently achieves significant positive gains across all solvers and engines. This is most dramatic with the CaDiCaL solver, where our approach reduces the PAR2 score by nearly an order of magnitude (from 856.6 to 67.4). Second, the improvement is particularly pronounced for the CNF-based SAT solvers, delivering reductions of 91.4% for Kissat and 92.1% for CaDiCaL. We attribute this to our framework’s ability to leverage circuit-based methods for effective elimination—optimizations that CNF-based solvers cannot perform on their own. Third, our framework still provides a 66.49% PAR2 reduction when used with the advanced CEC engine. Therefore, our approach is fully compatible with existing LEC tools, acting as a powerful pre-processing step that provides additional simplification, logic packing, and solver-friendly reformulation.

4.3 Ablation Studies↩︎

We further perform ablation studies to assess the effectiveness of the three key components in our framework using Kissat, the strongest solver among those tested.

4.3.1 Effectiveness of Equivalence-Preserving LUT Mapping↩︎

To assess the impact of our equivalence-preserving LUT mapping, we conduct an ablation study comparing the configurations with (Ours.) or without (Ours.w/o Equiv) the proposed method. Besides, we also evaluate the configurations with (w CCC) or without (w/o CCC) Clausal Congruence Closure (CCC) [14]. CCC is a powerful CNF-level circuit simplification technique, which detects AND, XOR, and ITE gate structures directly from CNF formulas and performs congruence closure to merge equivalent literals. We include such comparison to demonstrate our LUT mapping provides benefits that are complementary to the subsequent CNF-based optimizations.

Therefore, we have four settings in this experiments:

• Ours.w CCC: our proposed equivalence-preserving mapping algorithm combined with the redundancy elimination in Clausal Congruence Closure (denoted as CCC).

• Ours.w/o CCC: our mapping method without CCC.

• Ours.w/o Equiv w CCC: the variant without our equivalence-preserving mapping but still using CCC.

• Ours.w/o Equiv w/o CCC: the variant that disables the equivalence-preserving mapping and also removing CCC.

Here, Clausal Congruence Closure serves as a CNF-level circuit simplification technique, which detects AND, XOR, and ITE gate structures directly from CNF formulas and performs congruence closure to merge equivalent literals, thereby reducing structural redundancy and improving SAT solving efficiency. In contrast, our equivalence-preserving mapping operates at the circuit level during LUT decomposition, maintaining structural correspondence between the golden and implementation sides of the miter. We include both with and without CCC settings to demonstrate that our method is complementary to CNF-level simplification—our mapping enhances structural regularity before CNF translation, while CCC further eliminates redundancy after translation.

Table  2 presents the cumulative solving performance for all four variants on the entire dataset. Comparing Ours.w/o Equiv w/o CCC and Ours.w/o Equiv w CCC shows that CCC alone contributes a noticeable performance gain by simplifying redundant CNF structures. However, when our equivalence-preserving mapping is enabled (Ours.w/o CCC), an even larger improvement is observed, indicating that preserving equivalence alignment early at the circuit level leads to substantially better clause reuse and stronger implication propagation during solving.

4.3.2 Gaussian-guided XOR Modeling↩︎

To assess the contribution of the proposed Gaussian-guided XOR modeling, we compare the solver performance with (Ours.) and without (Ours.w/o Gauss) this component. While we observe an average 5.3% PAR2 reduction across the entire dataset by using Gaussian-guided XOR modeling, the gain is especially significant on XOR-dense datapath circuits.

Therefore, we perform a deeper analysis on 20 circuits constructed from 32\(\times\)​32 multipliers implemented with diverse architectures [40], [41]. These multipliers pose one of the most challenging verification tasks [42] due to their deep and XOR-dense structures. To maintain a consistent comparison and demonstrate complementarity with CNF-level simplifications as Section 4.3.1, we again compare the configurations with (w CCC) or without CCC (w/o CCC).

The results are shown in Figure 3. First, a large improvement on solving efficiency is seen when our method is applied (Ours.w/o Gauss w CCC v.s. Ours. w CCC). With our method, all 20 XOR-dense instances are solved within 2,000 seconds. In contrast, the configuration without our Gaussian modeling solves only 7 instances by the 2,000s mark and 19 instances by 3,600s. Second, the two techniques are not conflicting, as they operate at different stages of the flow and can be applied simultaneously—Ours.w CCC achieves the best overall performance, yielding an average speedup of 36.8% over Ours.w/o Gauss w CCC.

4.3.3 Solver-Oriented LUT Selection Criterion↩︎

To evaluate the effectiveness of our proposed solver-friendliness metric, we isolate it from the other two components and activate only the metric-guided LUT selection module (denoted as Ours.metric). Two baselines are included for comparison:

• Comp.1, from prior work [20], which employs a branching-based LUT cost function emphasizing structural complexity.

• Comp.2, from prior work [19], which uses area-oriented cost functions based on CNF clause counts during mapping.

As shown in Figure 4, Ours.metric consistently outperforms both Comp.1 and Comp.2 across the runtime range. Compared with Comp.1, it solves 5.5% more instances within 3,600 seconds and yields an overall 34.1% average speedup. These results demonstrate that our metric effectively captures solver-oriented behaviors beyond structural complexity, leading to a more solver-efficient formulation.

5 Conclusion↩︎

This paper presented a mapping-based modeling framework for Logic Equivalence Checking. By integrating equivalence-preserving LUT mapping, Gaussian-guided XOR modeling, and solver-oriented LUT selection into a unified flow, our method formulates the miter into a structurally symmetric, algebraically simplified, and solver-efficient form. Experiments on comprehensive benchmarks confirm substantial and consistent improvements across multiple solver paradigms, demonstrating that modeling formulation can markedly enhance LEC efficiency and bridge the gap between logic synthesis and SAT-based formal verification.

Acknowledgments↩︎

This work was supported in part by the Hong Kong Research Grants Council (RGC) under Grant No. N_CUHK451/25, 14202824, C6003-24Y, and T46-415/25-R.

References↩︎