基于对偶变量的计算机代数证明的机器检验

Machine Checking for Computer Algebraic Proofs Based on Dual Variables

摘要: 代数推理是目前验证门级整数乘法器最有效的方法之一。实用代数演算是一种涵盖了代数推理并能进行有效证明检验的证明格式。尤其是在代数编码中添加对偶变量生成统一的PAC证明。因为PAC证明文件非常大，且验证过程可能包含错误，本文介绍了一种验证检验器PACHECK2，通过对PAC证明格式进行修改，导出由一系列线性组合组成的证明。进一步识别异或门，分块进行线性组合，减少证明规则的使用，生成简洁的证明。实验表明新的检验器PACHECK2能有效检验证明，验证效率更高，同时提供详细的错误信息。为乘法器的验证提供了一个有效的检验器。

Abstract: Algebraic reasoning is one of the most effective methods to verify gate level integer multiplier at present. Practical algebraic calculus is a proof scheme that covers algebraic reasoning and can perform effective proof checking. In particular, adding dual variables to algebraic coding generates uniform PAC proofs. Because the PAC proof file is very large and the verification process may contain errors, this paper introduces a proof checker PACHECK2. By modifying the PAC proof format, a proof composed of a series of linear combinations is derived. To further identify XOR gates, the linear combination of blocks can reduce the use of proof rules and generate simple proof. The experimental results show that the new checker PACHECK2 can effectively check the proof, the verification efficiency is higher, and at the same time, provide detailed error information. It pro-vides an effective checker for the verification of the multiplier.