Equivalence checking using Gröbner bases
Equivalence checking using Gröbner bases
复制标题
使用 Grobner 基进行等价性检查
DOI：
--
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
R. Drechsler
中科院分区：
文献类型：
--
作者：
Amr A. R. Sayed;Daniel Große;Mathias Soeken;R. Drechsler
受最近成功的代数计算技术在大型和优化的门级乘法器的正式验证，本文提出了代数等价性检查处理电路，既包含复杂的算术组件，以及控制逻辑。这些电路对现有的证明技术提出了重大挑战。代数组合等价性检验（ACEC）的基本思想是将两个被比较的电路用Gröbner基的形式建模，然后将它们联合收割机组合成一个代数模型。它生成两个电路的内部变量之间的位和字的关系候选人，并测试它们在组合模型中的成员资格。由于成员资格测试不缩放所描述的设置，我们建议逆向工程提取算术组件，并将其抽象为规范表示。此外，我们提出了算术扫描，利用抽象的组件，找到并证明两个电路之间的内部等价。我们证明了ACEC的适用性检查的浮点乘法器（包括完整的IEEE-754舍入方案）对几个优化和多样化的实现的等效性。
Motivated by the recent success of the algebraic computation technique in formal verification of large and optimized gate-level multipliers, this paper proposes algebraic equivalence checking for handling circuits that contain both complex arithmetic components as well as control logic. These circuits pose major challenges for existing proof techniques. The basic idea of Algebraic Combinational Equivalence Checking (ACEC) is to model the two compared circuits in form of Gröbner bases and combine them into a single algebraic model. It generates bit and word relationship candidates between the internal variables of the two circuits and tests their membership in the combined model. Since the membership testing does not scale for the described setting, we propose reverse engineering to extract arithmetic components and to abstract them to canonical representations. Further we propose arithmetic sweeping which utilizes the abstracted components to find and prove internal equivalences between both circuits. We demonstrate the applicability of ACEC for checking the equivalence of a floating point multiplier (including full IEEE-754 rounding scheme) against several optimized and diversified implementations.