Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits

TL;DR

This paper introduces a hybrid multimodular algebraic verification method for arithmetic circuits that avoids large-integer computations by parallel modular reasoning, improving efficiency.

Contribution

It presents a novel parallel multimodular verification technique combining linear and nonlinear rewriting, implemented in TalisMan2.0, to enhance circuit verification performance.

Findings

Significantly reduces computational overhead for large-word arithmetic circuit verification.

Demonstrates improved performance over existing methods on multiplier benchmarks.

Effectively avoids large-integer arithmetic through parallel modular computations.

Abstract

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.