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

技术摘要：TensorEQC – 结构感知型等价检查

问题陈述
等价检查（EC）对电路的表示形式高度敏感。不同的电路结构——例如富含 XOR 的网络、进位链、有限域乘法器和整数乘法器——展现出各异的结构特性，这些特性更倾向于不同的验证方法。没有任何单一方法（如布尔代数、决策图或张量网络）能够普遍主导所有类型的电路。此外，验证时序电路需要区分观测到的初始状态依赖性，以及在特定观测边界内消除的不确定性，特别是在涉及复位状态的情况下。

方法论
本文介绍了一种名为 TensorEQC 的可执行研究工作流，其设计理念是一个多算法组合集（portfolio），而非单一的单体求解器。其核心哲学是：一个引擎只有在其自身的精确语义范围内能够完成验证义务时，才应承担该义务；否则，该义务应移交给另一个引擎。

该工作流由三个主要部分组成：

1. 组合逻辑组合集（Combinational Portfolio）： 一个顺序流水线式的验证引擎，负责处理输出，直到义务被解除或达到资源限制。该流水线包括：
   • 结构哈希（Structural Hashing）： 在支持的基元（AND、OR、XOR 等）下建立表达式有向无环图（DAG）的恒等性，并进行交换律归一化。
   • 仿真（Simulation）： 使用包含随机模式、全零模式和全一模式的打包仿真，以寻找负向证物（反例）。
   • 代数正规型（ANF）： 将布尔函数表示为 GF(2) 上的多项式。它利用特定的引理，从非零多项式中生成精确的负向证物。
   • 关系张量消除（Relational Tensor Elimination）： 将逻辑门表示为布尔指示张量。它通过布尔半环上的析取（以保留满足赋值的存在性）而非 GF(2) 求和（计算奇偶校验）来进行变量消除。
   • ROBDD 与穷举回退（ROBDD & Exhaustive Fallback）： 使用带有节点容量限制的排序二叉决策图（ROBDD）以及小规模支持的穷举枚举作为最终回退手段。
2. 张量列阵（Tensor Train, TT）分析： 一个伴随模块，通过构建来自真值表的精确 TT 表示，来测量代数秩并测试零函数。它区分了 GF(2) 上的秩与实数上的秩，指出 GF(2) 秩可能显著更小。
3. 复位分析（Reset Analysis）： 一个使用显式状态自组合（self-composition）的同步模块，用于检查初始状态依赖性。它区分了复位依赖性是立即被观测到，还是在特定数量的“刷新”周期后消失的情况。

核心贡献

• 精确引擎的集成： 本研究展示了结构哈希、GF(2) 代数、关系张量网络和 ROBDD 的实际集成，并为每种方法保持了独立的证明契约。
• 结构感知策略： 研究提供了经验证据，表明验证效率高度依赖于电路结构和变量排序。例如，交错的加法器操作数产生低张量秩（≤3），而分离的操作数则产生高秩（129），后者较不适合基于张量的方法。
• 复位状态诊断： 提供了一种方法，用于明确区分真实的初始状态依赖性与同步设计中的瞬态不确定性。
• 可复现的验证： 本文包含一个新的、自包含的补充材料，该材料验证了精确 GF(2) 张量列阵构建、秩测量以及零函数测试在五个 16 输入函数上的表现，确认了奇偶抵消与实际零函数之间的区别。

实验结果
研究报告了两组不同的证据：

1. 历史组合集战役 (v1.0.0)： 该数据集包括 89 次运行案例，涉及 2,048 位进位加法器、128 位多项式基乘法器和仿射网络。
   • 成功案例： 全流程成功验证了 2,048 位进位加法器（2.87s）和 128 位 GF 乘法器（0.80s），在特定情况下（如 BDD 无法解决的 2,048 位加法器）优于仅使用 BDD 的方法。
   • 局限性： 该方法在 1,024 位进位加法器和 1,024 输入的仿射网络上达到了资源限制（节点容量限制、宽度限制）。整数乘法的结果由于 ANF 增长和张量作用域限制，仅限于 10 位。
   • 观察： 全流程有时会比直接选择最优引擎产生更高的开销，这凸显了自动化与效率之间的权衡。
2. 新的可复现补充材料： 对五个 16 输入函数（包括奇偶校验和 GF 乘法）进行的针对性实验证实，精确张量列阵构建和秩分析对于小型函数是可行的。它验证了标量 GF(2) 之和为零并不意味着零函数（奇偶抵消），而 TT 零测试正确处理了这一区别。

意义与主张
论文明确将其贡献界定为范围限定的技术评估，而非通用解决方案。

• 不存在普遍优越性： 结果并不支持“张量网络优于所有其他方法”的说法。相反，它们支持一种“表示敏感型策略”，即根据数学领域（例如，针对低阶有限域函数使用 GF 代数，针对进位链使用关系消除）来选择不同的引擎。
• 集成而非替代： 核心成果是成功地将精确代数、关系消除、决策图和时序推理集成在一起，同时保持了各自独立的证明契约。
• 明确的边界： 作者强调，目前的实现仅限于二进制组合基元和小型同步机。它尚不支持通用的 SystemVerilog、功耗感知语义、异步时序或工业级网表。论文区分了“证明”（对编码后的布尔义务的精确满足）与“认证”（这需要经过验证的前端和证明检查链，两者均被列为未来工作）。

总之，TensorEQC 提供了一个结合多种精确验证方法以处理异构逻辑的框架，证明了虽然没有哪种引擎是普遍最优的，但一个结构化的组合集可以有效地验证特定类别的电路，同时清晰地识别自身的局限性。