Arithmetic Circuit Correction by Adding Optimized Correctors Based on Groebner Basis Computation
Arithmetic Circuit Correction by Adding Optimized Correctors Based on Groebner Basis Computation
复制标题
基于 Groebner 基计算添加优化校正器的算术电路校正
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
B. Alizadeh
中科院分区：
文献类型：
--
作者：
Negar Aghapour Sabbagh;B. Alizadeh
虽然符号计算机代数(SCA)是一种很有前途的验证大型算术电路的方法，但由于单项式爆炸，基于SCA的这类电路的自动校正仍然是一个巨大的挑战。基于SCA的验证方法将电路和规范转换为一组多项式。验证问题被认为是对给定规范多项式的理想成员测试，其中理想是由电路的多项式生成的。验证算法返回一个称为余数的多项式，其值表示电路的正确性。我们自动纠正故障电路的主要思想是构造一个称为校正器的子电路，实现余数的补码，该余数被添加到故障电路中。我们的方法适用于各种乘法器电路，具有不同的大小(8到256位)和错误数量(1到5个错误)。与通过在电路中插入元件以实现零余数来消除每一步中一项余数的方法进行了比较。结果表明，用该方法生成校正子电路的速度平均提高了20.03倍。
Although Symbolic Computer Algebra (SCA) is a promising approach to verify large arithmetic circuits, automatic correction of such circuits based on SCA remains a significant challenge due to the monomial explosion. SCA-based verification methods translate the circuit and the specification into a set of polynomials. The verification problem is considered as an ideal membership test for the given specification polynomial where the ideal is generated by the polynomials of the circuit. A polynomial, called the remainder, is returned by the verification algorithm whose value shows the correctness of the circuit. Our main idea to automatically correct the buggy circuit is to construct a sub-circuit called the corrector, implementing the complement of the remainder, which is added to the buggy circuit. Our method is applied to various multiplier circuits, with different sizes (8 to 256 bits) and the number of bugs (1 to 5 bugs). The proposed method is compared with a method, which eliminates one term of the remainder in each step by inserting elements to the circuit to achieve a zero remainder. The results show that generating the corrector sub-circuit is done, on average, 20.03× faster than before applying our method.