Extracting Linear Relations from Gr\"obner Bases for Formal Verification of And-Inverter Graphs

TL;DR

This paper introduces a novel approach for circuit verification using Gr"obner bases, focusing on extracting linear relations to improve efficiency and overcome monomial blow-up issues in algebraic methods.

Contribution

The paper proposes a new technique to extract linear polynomials from Gr"obner bases, enhancing formal verification of circuits with improved computational efficiency.

Findings

Effective extraction of linear relations from Gr"obner bases

Reduction in monomial blow-up during polynomial rewriting

Successful application to multiplier verification benchmarks

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\"obner 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\"obner 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.