Formal verification of multiplier circuits using computer algebra
Formal verification of multiplier circuits using computer algebra
复制标题
DOI：
10.1515/itit-2022-0039
复制
发表时间：
2022-06
期刊：
影响因子：
--
通讯作者：
Daniela Kaufmann
中科院分区：
文献类型：
--
作者：
Daniela Kaufmann
数字电路在计算机中得到了广泛的应用，因为它们为各种数字元件和算术运算提供了模型。算术电路是用于执行布尔代数的数字电路的一个子类。为了避免像臭名昭著的奔腾FDIV错误这样的问题，确保算术电路正确是至关重要的。形式验证可用于确定电路相对于某个规范的正确性。然而，算术电路，特别是整数乘法器，代表了对当前验证方法的挑战，并且实际上仍然需要大量的手工劳动。在我的论文中，我们研究和开发基于计算机代数的自动推理方法，其中的字级规格，建模为多项式，减少了Gröbner基础推断的门级表示的电路。我们提供了一个精确的形式化的推理过程，其中包括健全性和完整性参数，并增加了在这一领域的数学背景。在实践方面，我们提出了一个独特的增量列式验证算法和预处理方法的基础上变量消除，简化了推断Gröbner基础。此外，我们在这篇论文中提供了一个代数证明演算，允许获得证书作为电路验证的副产品，以提高自动推理工具的结果的信心。这些证书可以通过独立的证明检查工具进行有效验证。
Abstract Digital circuits are widely utilized in computers, because they provide models for various digital components and arithmetic operations. Arithmetic circuits are a subclass of digital circuits that are used to execute Boolean algebra. To avoid problems like the infamous Pentium FDIV bug, it is critical to ensure that arithmetic circuits are correct. Formal verification can be used to determine the correctness of a circuit with respect to a certain specification. However, arithmetic circuits, particularly integer multipliers, represent a challenge to current verification methodologies and, in reality, still necessitate a significant amount of manual labor. In my dissertation we examine and develop automated reasoning approaches based on computer algebra, where the word-level specification, modeled as a polynomial, is reduced by a Gröbner basis inferred by the gate-level representation of the circuit. We provide a precise formalization of this reasoning process, which includes soundness and completeness arguments and adds to the mathematical background in this field. On the practical side we present an unique incremental column-wise verification algorithm and preprocessing approaches based on variable elimination that simplify the inferred Gröbner basis. Furthermore, we provide an algebraic proof calculus in this thesis that allows obtaining certificates as a by-product of circuit verification in order to boost confidence in the outcomes of automated reasoning tools. These certificates can be efficiently verified with independent proof checking tools.