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中实现了所提出的方法，并在多个乘法器基准测试上进行了评估。结果表明，混合多模推理显著优于现有方法。