用布尔可满足性验证逻辑电路的等价性

摘要：

提出了使用布尔可满足性来验证数字电路的等价性验证方法.这一验证方法把每个电路抽象成一个有限状态机,为两个待验证的电路构造积机,把等价性验证问题转换成了积机的断言问题.改进了Tseitin变换方法,用于把电路约束问题变换成合取范式公式.用先进的布尔可满足性求解器zChaff判定积机所生成的布尔公式的可满足性.事例电路验证说明了该方法的有效性.

关键词： 数字电路 等价性验证 布尔可满足性 合取范式

作者: 刘歆 颜萍

作者单位: 湖北工业大学电气与电子工程学院,湖北,武汉,430068

会议类型: 国内会议

会议名称: 湖北省机械工程学会机械设计与传动专业委员会第十五届学术年会

会议地点: 武汉

会议语种:中文

页码: 1-4

在线出版日期: 2007-06-02（万方平台首次上网日期，不代表论文的发表时间）