TensorEQC: Structure-Aware Equivalence Checking with GF(2) Algebra, Exact Tensor Networks, and Reset Analysis : a Multi-Algorithmic Study of Datapath Verification and Reset-State Dependence

Technical Summary: TensorEQC – Structure-Aware Equivalence Checking

Problem Statement
Equivalence checking (EC) is highly sensitive to the representation of a circuit. Different circuit structures—such as XOR-rich networks, carry chains, finite-field multipliers, and integer multipliers—exhibit distinct structural properties that favor different verification approaches. No single method (e.g., Boolean algebra, decision diagrams, or tensor networks) universally dominates all circuit types. Furthermore, verifying sequential circuits requires distinguishing between observable initial-state dependence and uncertainty that resolves within a specific observation boundary, particularly regarding reset states.

Methodology
The paper introduces TensorEQC, an executable research workflow designed as a multi-algorithmic portfolio rather than a single monolithic solver. Its core philosophy is that an engine should only discharge a verification obligation if it can do so according to its own exact semantics; otherwise, the obligation is passed to another engine.

The workflow consists of three primary components:

1. Combinational Portfolio: A sequential pipeline of verification engines that processes outputs until they are discharged or a resource limit is reached. The pipeline includes:
   • Structural Hashing: Establishes identity of expression DAGs under supported primitives (AND, OR, XOR, etc.) with commutative normalization.
   • Simulation: Uses packed simulation with random, all-zero, and all-one patterns to find negative witnesses (counterexamples).
   • Algebraic Normal Forms (ANF): Represents Boolean functions as multilinear polynomials over GF(2). It utilizes a specific lemma to generate exact negative witnesses from nonzero polynomials.
   • Relational Tensor Elimination: Represents gates as Boolean indicator tensors. It performs variable elimination via disjunction over the Boolean semiring (to preserve existence of satisfying assignments) rather than GF(2) summation (which computes parity).
   • ROBDD & Exhaustive Fallback: Uses Ordered Binary Decision Diagrams with node caps and small-support exhaustive enumeration as final fallbacks.
2. Tensor Train (TT) Analytics: A companion module that constructs exact TT representations from truth tables to measure algebraic rank and test for zero functions. It distinguishes between ranks over GF(2) and real numbers, noting that GF(2) ranks can be significantly smaller.
3. Reset Analysis: A synchronous module using explicit-state self-composition to check for initial-state dependence. It distinguishes between cases where reset dependence is observable immediately versus cases where it disappears after a specific number of "flushing" cycles.

Key Contributions

• Integration of Exact Engines: The work demonstrates a practical integration of structural hashing, GF(2) algebra, relational tensor networks, and ROBDDs, maintaining distinct proof contracts for each.
• Structure-Aware Strategy: It provides empirical evidence that verification efficiency is highly dependent on circuit structure and variable ordering. For instance, interleaved adder operands yield low tensor ranks (≤3), while split operands result in high ranks (129), making the latter less suitable for tensor-based approaches.
• Reset-State Diagnostics: It offers a method to explicitly distinguish between true initial-state dependence and transient uncertainty in synchronous designs.
• Reproducible Validation: The paper includes a new, self-contained supplement that validates exact GF(2) tensor train construction, rank measurements, and zero-function tests on five 16-input functions, confirming the distinction between parity cancellation and actual zero functions.

Experimental Results
The study reports on two distinct sets of evidence:

1. Historical Portfolio Campaign (v1.0.0): This dataset includes 89 case runs involving 2,048-bit ripple adders, 128-bit polynomial-basis multipliers, and affine networks.
   • Successes: The full flow successfully verified 2,048-bit ripple adders (2.87s) and 128-bit GF multipliers (0.80s), outperforming BDD-only approaches in specific cases (e.g., 2,048-bit adders where BDDs failed to resolve).
   • Limitations: The approach hit resource limits (node caps, width caps) on 1,024-bit ripple adders and 1,024-input affine networks. Integer multiplication results were limited to 10 bits due to ANF growth and tensor scope caps.
   • Observation: The full flow sometimes incurred overhead compared to selecting the optimal engine directly, highlighting the trade-off between automation and efficiency.
2. New Reproducible Supplement: A focused experiment on five 16-input functions (including parity and GF multiplication) confirmed that exact tensor train construction and rank analysis are feasible for small functions. It validated that a scalar GF(2) sum of zero does not imply a zero function (parity cancellation), a distinction correctly handled by the TT zero-test.

Significance and Claims
The paper explicitly frames its contribution as a scoped technical assessment rather than a universal solution.

• No Universal Superiority: The results do not support the claim that tensor networks are superior to all other methods. Instead, they support a "representation-sensitive strategy" where different engines are selected based on the mathematical domain (e.g., GF algebra for low-degree finite-field functions, relational elimination for carry chains).
• Integration over Replacement: The central result is the successful integration of exact algebra, relational elimination, decision diagrams, and temporal reasoning while keeping their proof contracts distinct.
• Explicit Boundaries: The author emphasizes that the current implementation is limited to binary combinational primitives and small synchronous machines. It does not yet support general SystemVerilog, power-aware semantics, asynchronous timing, or industrial-scale netlists. The paper distinguishes between "proof" (exact satisfaction of the encoded Boolean obligation) and "certification" (which requires a verified frontend and proof-checker chain, both noted as future work).

In summary, TensorEQC provides a framework for combining multiple exact verification methods to handle heterogeneous logic, demonstrating that while no single engine is universally optimal, a structured portfolio can effectively verify specific circuit classes while clearly identifying its own limitations.