Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits
This addresses efficiency issues in word-level verification for arithmetic circuits, though it appears incremental as it builds on existing algebraic methods.
The paper tackles the computational overhead of verifying arithmetic circuits with large operands by introducing a hybrid algebraic verification technique based on polynomial reasoning and multimodular reasoning using homomorphic images, which avoids large-integer arithmetic and shows significant improvements on multiplier benchmarks.
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.