Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs

Daniela Kaufmann, Jérémy Berthomieu

TL;DR

The paper tackles the challenge of formal circuit verification using Gröbner bases by shifting focus from rewriting the specification to rewriting the Gröbner basis itself under a degree-aware ordering. It proves that when the specification is linear, ideal membership can be decided using only the linear polynomials of the Gröbner basis, and introduces a practical subproblem strategy that builds local Gröbner bases for small sub-circuits to extract linear relations efficiently. A linearization technique is employed, introducing extension variables to replace non-linear monomials, with a soundness and completeness theorem ensuring correctness. Experimental results on multiplier benchmarks show the approach can complement existing algebraic verification methods, offering robustness in scenarios where full basis computation is infeasible. The work lays groundwork for a white-box extension and potential applications to equivalence checking by focusing on linear information extractable from Gröbner bases.

Abstract

Formal verification techniques based on computer algebra have proven highly effective for circuit verification. The circuit, given as an and-inverter graph, is encoded as a set of polynomials that automatically generates a Gröbner basis with respect to a lexicographic term ordering. Correctness of the circuit can be derived by computing the polynomial remainder of the specification. However, the main obstacle is the monomial blow-up during the rewriting of the specification, which leads to the development of dedicated heuristics to overcome this issue. In this paper, we investigate an orthogonal approach and focus the computational effort on rewriting the Gröbner basis itself. Our goal is to ensure the basis contains linear polynomials that can be effectively used to rewrite the linearized specification. We first prove the soundness and completeness of this technique and then demonstrate its practical application. Our implementation of this method shows promising results on benchmarks related to multiplier verification.

Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs

TL;DR

The paper tackles the challenge of formal circuit verification using Gröbner bases by shifting focus from rewriting the specification to rewriting the Gröbner basis itself under a degree-aware ordering. It proves that when the specification is linear, ideal membership can be decided using only the linear polynomials of the Gröbner basis, and introduces a practical subproblem strategy that builds local Gröbner bases for small sub-circuits to extract linear relations efficiently. A linearization technique is employed, introducing extension variables to replace non-linear monomials, with a soundness and completeness theorem ensuring correctness. Experimental results on multiplier benchmarks show the approach can complement existing algebraic verification methods, offering robustness in scenarios where full basis computation is infeasible. The work lays groundwork for a white-box extension and potential applications to equivalence checking by focusing on linear information extractable from Gröbner bases.

Abstract

Formal verification techniques based on computer algebra have proven highly effective for circuit verification. The circuit, given as an and-inverter graph, is encoded as a set of polynomials that automatically generates a Gröbner basis with respect to a lexicographic term ordering. Correctness of the circuit can be derived by computing the polynomial remainder of the specification. However, the main obstacle is the monomial blow-up during the rewriting of the specification, which leads to the development of dedicated heuristics to overcome this issue. In this paper, we investigate an orthogonal approach and focus the computational effort on rewriting the Gröbner basis itself. Our goal is to ensure the basis contains linear polynomials that can be effectively used to rewrite the linearized specification. We first prove the soundness and completeness of this technique and then demonstrate its practical application. Our implementation of this method shows promising results on benchmarks related to multiplier verification.

Paper Structure

This paper contains 6 sections, 2 theorems, 2 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Related Work.
  3. Our contribution.
  4. Preliminaries
  5. Gröbner Basis
  6. And-Inverter Graphs

Key Result

lemma thmcounterlemma

Every ideal $I \subseteq \mathbb{K}[X]$ has a Gröbner basis w.r.t. a fixed total order.

Figures (1)

  • Figure 1: AIG and polynomial encoding of a 2-bit multiplier in the ring $\mathbb{Q}[X]$.

Theorems & Definitions (13)

  • definition thmcounterdefinition: Term, Monomial, Polynomial, see CoxLittleOShea-Book07
  • definition thmcounterdefinition: Degree
  • definition thmcounterdefinition: Monomial Order
  • definition thmcounterdefinition: Lexicographic Order, see CoxLittleOShea-Book07
  • definition thmcounterdefinition: Degree Reverse Lexicographic Order, see CoxLittleOShea-Book07
  • definition thmcounterdefinition: Ideal
  • definition thmcounterdefinition: Remainder
  • lemma thmcounterlemma: see CoxLittleOShea-Book07
  • lemma thmcounterlemma: see CoxLittleOShea-Book07
  • definition thmcounterdefinition: AIG
  • ...and 3 more