Exploring Algebraic Interpolants for Rectification of Finite Field Arithmetic Circuits with Gröbner Bases
| Autor: | Irina Ilioaea, Utkarsh Gupta, Florian Enescu, Priyank Kalla |
|---|---|
| Rok vydání: | 2019 |
| Předmět: |
050101 languages & linguistics
Polynomial Computer science 05 social sciences ComputingMethodologies_IMAGEPROCESSINGANDCOMPUTERVISION 02 engineering and technology Propositional calculus Algebra Gröbner basis Lattice (module) Finite field ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing 0501 psychology and cognitive sciences Finite field arithmetic Algebraic number Formal verification |
| Zdroj: | ETS |
| DOI: | 10.1109/ets.2019.8791541 |
| Popis: | When formal verification identifies the presence of a bug in a design, it is required to rectify the circuit at some net(s). Modern approaches formulate the rectification test as an unsatisfiability proof, and then use Craig interpolants (CI) in propositional logic to compute the corresponding rectification functions. Boolean SAT and CI engines are infeasible in rectification of finite field arithmetic circuits, where polynomial algebra is more suitable. Recently, it was shown that CI exist in polynomial algebra in finite fields. This paper presents a detailed theory and algorithms for CI in finite fields, and characterizes the lattice of all algebraic interpolants. Using the Grobner basis algorithm, we present techniques to traverse the interpolant lattice. This allows to explore various interpolants for efficient synthesis of rectification functions for finite field arithmetic circuits. Experimental results are presented that demonstrate the efficacy of our approach. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|