%0 Conference Proceedings
%T Rectification of Arithmetic Circuits with Craig Interpolants in Finite Fields
%+ University of Utah
%+ Georgia State University
%A Gupta, Utkarsh
%A Ilioaea, Irina
%A Rao, Vikas
%A Srinath, Arpitha
%A Kalla, Priyank
%A Enescu, Florian
%< avec comité de lecture
%( IFIP Advances in Information and Communication Technology
%B 26th IFIP/IEEE International Conference on Very Large Scale Integration - System on a Chip (VLSI-SoC)
%C Verona, Italy
%Y Nicola Bombieri
%Y Graziano Pravadelli
%Y Masahiro Fujita
%Y Todd Austin
%Y Ricardo Reis
%I Springer International Publishing
%3 VLSI-SoC: Design and Engineering of Electronics Systems Based on New Computing Paradigms
%V AICT-561
%P 79-106
%8 2018-10-08
%D 2018
%R 10.1007/978-3-030-23425-6_5
%K Rectification
%K Arithmetic circuits
%K Gröbner bases
%K Craig interpolants
%Z Computer Science [cs]Conference papers
%X When formal verification of arithmetic circuits identifies the presence of a bug in the design, the task of rectification needs to be performed to correct the function implemented by the circuit so that it matches the given specification. In our recent work [26], we addressed the problem of rectification of buggy finite field arithmetic circuits. The problems are formulated by means of a set of polynomials (ideals) and solutions are proposed using concepts from computational algebraic geometry. Single-fix rectification is addressed – i.e. the case where any set of bugs can be rectified at a single net (gate output). We determine if single-fix rectification is possible at a particular net, formulated as the Weak Nullstellensatz test and solved using Gröbner bases. Subsequently, we introduce the concept of Craig interpolants in polynomial algebra over finite fields and show that the rectification function can be computed using algebraic interpolants. This article serves as an extension to our previous work, provides a formal definition of Craig interpolants in finite fields using algebraic geometry and proves their existence. We also describe the computation of interpolants using elimination ideals with Gröbner bases and prove that our procedure computes the smallest interpolant. As the Gröbner basis algorithm exhibits high computational complexity, we further propose an efficient approach to compute interpolants. Experiments are conducted over a variety of finite field arithmetic circuits which demonstrate the superiority of our approach against SAT-based approaches.
%G English
%Z TC 10
%Z WG 10.5
%2 https://inria.hal.science/hal-02321766/document
%2 https://inria.hal.science/hal-02321766/file/485996_1_En_5_Chapter.pdf
%L hal-02321766
%U https://inria.hal.science/hal-02321766
%~ IFIP
%~ IFIP-AICT
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-VLSISOC
%~ IFIP-TC10
%~ IFIP-WG10-5
%~ IFIP-AICT-561