Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits

Clemens Hofstadler, Daniela Kaufmann, Chen Chen

TL;DR

A hybrid algebraic verification technique based on polynomial reasoning that combines linear and nonlinear rewriting that relies on multimodular reasoning using homomorphic images, where computations are performed in parallel modulo different primes, thereby avoiding any large-integer arithmetic.

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.

Avoiding Big Integers: Parallel Multimodular Algebraic Verification of Arithmetic Circuits

TL;DR

A hybrid algebraic verification technique based on polynomial reasoning that combines linear and nonlinear rewriting that relies on multimodular reasoning using homomorphic images, where computations are performed in parallel modulo different primes, thereby avoiding any large-integer arithmetic.

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.
Paper Structure (15 sections, 2 theorems, 3 equations, 4 figures, 1 table)

This paper contains 15 sections, 2 theorems, 3 equations, 4 figures, 1 table.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Algebra
  4. And-Inverter Graphs and their Polynomial Encodings
  5. Related Work
  6. Multimodular Verification via Homomorphic Images
  7. Hybrid Algebraic Circuit Verification
  8. Linear Rewriting
  9. Nonlinear Rewriting
  10. Experiments
  11. Conclusion & Future Work
  14. Benchmark Details
  15. Experimental Data

Key Result

lemma 1

Let $C$ be an AIG and $m \geq 2$ be a positive integer. An assignment $\varphi$ is a model of $G(C)$ over $\mathbb{Z}$ if and only if it is a model of $G(C)$ over $\mathbb{Z}_m$.

Figures (4)

  • Figure 1: AIG and polynomial encoding of a 2-bit multiplier.
  • Figure 2: Overview of the TalisMan2.0 workflow. Double-edged boxes are computations that are run in parallel in TalisMan2.0.
  • Figure 3: Comparison of TalisMan2.0 and related work. For each tool the number of solved instances is added in parentheses.
  • Figure 4: Comparing the default setting when either uniform input sampling (left), only linear rewriting (middle), or only nonlinear rewriting is used (right).

Theorems & Definitions (6)

  • definition 1
  • definition 2
  • lemma 1
  • proof
  • theorem 1
  • proof