Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs - Sorbonne Université
Preprints, Working Papers, ... Year : 2024

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

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.
Fichier principal
Vignette du fichier
main.pdf (598.77 Ko) Télécharger le fichier
Origin Files produced by the author(s)
Licence

Dates and versions

hal-04804486 , version 1 (26-11-2024)

Licence

Identifiers

Cite

Daniela Kaufmann, Jérémy Berthomieu. Extracting Linear Relations from Gröbner Bases for Formal Verification of And-Inverter Graphs. 2024. ⟨hal-04804486⟩
0 View
0 Download

Altmetric

Share

More