On the Rectifiability of Arithmetic Circuits using Craig Interpolants in Finite Fields
On the Rectifiability of Arithmetic Circuits using Craig Interpolants in Finite Fields
复制标题
有限域中使用克雷格插值的算术电路的可整流性
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Florian Enescu
中科院分区：
文献类型：
--
作者：
Utkarsh Gupta;Irina Ilioaea;V. Rao;Arpitha Srinath;P. Kalla;Florian Enescu
当算术电路的正式验证发现设计中存在错误时，需要执行纠正任务，以纠正电路实现的功能，使其符合给定的规范。本文研究了有缺陷的有限域运算电路的纠错问题。这些问题是通过一组多项式(理想)来表示的，并使用计算代数几何中的概念来提出解决方案。解决了单修复纠正-即任何(一组)错误可以在单个网络(门输出)上纠正的情况。我们确定在一个特定的位置是否有可能进行单一修正，即弱Nullstellensatz检验。随后，我们在有限域上的多项式代数中引入了Craig插值法的概念，并证明了利用代数插值法可以计算校正函数。实验结果表明，与基于SAT的方法相比，该方法具有更好的性能。
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. This paper addresses 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 location, formulated as the Weak Nullstellensatz test. 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. Experimental results demonstrate the superiority of our approach against SAT-based approaches.