Automated Debugging of Arithmetic Circuits Using Incremental Gröbner Basis Reduction
Automated Debugging of Arithmetic Circuits Using Incremental Gröbner Basis Reduction
复制标题
使用增量GR自动调试算术电路
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
P. Mishra
中科院分区：
文献类型：
--
作者：
Farimah Farahmandi;P. Mishra
符号代数是验证大型复杂算术电路的一种有前途的方法。现有的基于代数的验证方法会生成余数来指示有错误的实现。其余部分有利于调试错误的实现，因为它可用于自动测试生成、错误定位和错误纠正。然而，现有的等价性检查方法不可扩展，并且当设计错误时会导致剩余部分的大小爆炸。更糟糕的是，错误的位置还可能导致余数项数量激增。在本文中，我们提出了一种增量等价检查方法，通过解决设计输入复杂性递增顺序的验证问题来解决可扩展性挑战。我们提出的方法有两个重要贡献。它能够为大型设计生成更小且紧凑的余数。我们提出的增量调试能够定位和纠正难以检测的错误，无论它们在设计中的位置如何。实验结果表明，当最先进的方法失败时，我们的方法可以有效地调试大型算术电路中最困难的错误。
Symbolic algebra is a promising approach to verify large and complex arithmetic circuits. Existing algebraic-based verification methods generate a remainder to indicate buggy implementation. The remainder is beneficial for debugging of the faulty implementation since it can be used for automated test generation, bug localization, and bug correction. However, existing equivalence checking approaches are not scalable and lead to explosion in size of the remainder when the design is faulty. To make the matters worse, the location of the bug can also lead to the explosion in the number of remainder terms. In this paper, we propose an incremental equivalence checking method to address the scalability challenges by solving the verification problem in the increasing order of design's input complexity. Our proposed approach makes two important contributions. It is able to generate smaller and compact remainders for large designs. Our proposed incremental debugging is capable of localizing and correcting hard-to-detect bugs irrespective of their location in the design. Experimental results demonstrate that our approach can efficiently debug most difficult bugs in large arithmetic circuits when the state-of-the-art methods fail.