文件名称：用布尔可满足性验证逻辑电路的等价性 (2007年)
文件大小：2.51MB
文件格式：PDF
更新时间：2024-07-08 15:12:18
工程技术 论文
提出了使用布尔可满足性来验证数字电路的等价性验证方法。这一验证方法把每个电路抽象成一个有限状态机,为两个待验证的电路构造积机,把等价性验证问题转换成了积机的断言问题。改进了Tseitin变换方法,用于把电路约束问题变换成合取范式公式。用先进的布尔可满足性求解器zChaff判定积机所生成的布尔公式的可满足性。事例电路验证说明了该方法的有效性。