-
题名基于对偶变量的计算机代数证明的机器检验
- 1
-
-
作者
魏峰玉
黄怡桐
刘帅
江建国
-
机构
辽宁师范大学数学学院
-
出处
《应用数学进展》
2022年第11期8191-8199,共9页
-
文摘
代数推理是目前验证门级整数乘法器最有效的方法之一。实用代数演算是一种涵盖了代数推理并能进行有效证明检验的证明格式。尤其是在代数编码中添加对偶变量生成统一的PAC证明。因为PAC证明文件非常大,且验证过程可能包含错误,本文介绍了一种验证检验器PACHECK2,通过对PAC证明格式进行修改,导出由一系列线性组合组成的证明。进一步识别异或门,分块进行线性组合,减少证明规则的使用,生成简洁的证明。实验表明新的检验器PACHECK2能有效检验证明,验证效率更高,同时提供详细的错误信息。为乘法器的验证提供了一个有效的检验器。
-
关键词
代数推理
对偶变量
乘法器验证
实用代数演算
-
分类号
O15
[理学—数学]
-
-
题名k-归纳模型检测结果的认证器
- 2
-
-
作者
刘帅
魏峰玉
黄怡桐
江建国
-
机构
辽宁师范大学数学学院
-
出处
《应用数学进展》
2022年第11期7729-7737,共9页
-
文摘
基于k-归纳的模型检测可以验证许多重要的系统,但在具体的实现过程中仍可能存在缺陷,所以对其结果进行认证是非常必要的。目前最有效的方法是利用k-证据电路的概念扩展给定的模型检测问题,然后使用认证器进行判定,但是在部分情况下,QBF的验证大大增加了认证时间。为了解决这一问题,本文提出对复位检测的算法进行优化,创建了一个新的复位条件并添加了带映射的原始电路来减小QBF。并且本文还使用C语言实现了认证器。实验结果表明:利用优化算法生成的QBF有效减少了认证时间,利用C语言实现的认证器也为之后的研究提供了有力工具。
-
关键词
k-归纳
模型检测
认证器
k-证据电路
-
分类号
TP311
[自动化与计算机技术—计算机软件与理论]
-
-
题名基于散列表的加法器重写优化算法
- 3
-
-
作者
黄怡桐
刘帅
魏峰玉
江建国
-
机构
辽宁师范大学数学学院
-
出处
《应用数学进展》
2022年第11期8265-8273,共9页
-
文摘
在大规模算术集成电路设计领域中,乘法器电路的验证是一重大难题。当前主流的方法是Gröbner基法。在此基础上,研究者们提出了加法器重写等优化方法,但重写过程依赖进位变量且需遍历全部变量,导致验证效率降低。为此,本文利用散列表对该方法进行优化,使用散列表存储所有和位输出变量,遍历表中元素进行扩充,再结合加法器的结构特性去识别加法器,从而不再依赖进位变量并且减少了需要遍历的变量数目。由实验结果可知,优化算法提高了Gröbner基的生成效率,也提高了乘法器的验证效率。
-
关键词
乘法器电路验证
Gr?bner基
加法器重写方法
散列表
-
分类号
O29
[理学—应用数学]
-
