Word-level verification of arithmetic circuits with large operands typically relies on arbitrary-precision arithmetic, which can lead to significant computational overhead as word sizes grow. In this paper, we present a hybrid algebraic verification technique based on polynomial reasoning that combines linear and nonlinear rewriting. Our approach relies on multimodular reasoning using homomorphic images, where computations are performed in parallel modulo different primes, thereby avoiding any large-integer arithmetic. We implement the proposed method in the verification tool TalisMan2.0 and evaluate it on a suite of multiplier benchmarks. Our results show that hybrid multimodular reasoning significantly improves upon existing approaches.

翻译：字级验证具有大操作数的算术电路通常依赖于任意精度算术，随着字长增长，这可能导致显著的计算开销。本文提出一种基于多项式推理的混合代数验证技术，结合线性和非线性重写。我们的方法利用同态图像进行多模推理，通过并行模不同素数进行计算，从而避免了任何大整数算术运算。我们将所提方法在验证工具TalisMan2.0中实现，并在乘法器基准套件上进行评估。结果表明，混合多模推理显著改进了现有方法。