基于布尔可满足性的逻辑电路等价性验证方法

• 作者: 刘歆 熊有伦
• 来源期刊: 微电子学与计算机
• 关键词: 设计验证 等价性验证 逻辑电路 布尔可满足性 合取范式
• 年，卷（期）: 2007,（11）
• 页码范围: 166-168,171
• 页数: 4页
• 分类号: TP274
• 语种: 中文
• DOI: 10.3969/j.issn.1000-7180.2007.11.048

摘要

提出了基于布尔可满足性(Boolean Satisfiability,SAT)的逻辑电路等价性验证方法.这一验证方法把每个电路抽象成一个有穷自动机(FSM),为两个待验证的电路构造积机,把等价性验证问题转换成了积机的断言判定问题.改进了Tseitin变换方法,并将其用于把电路约束问题变换成(Conjunctive Normal Form,CNF)公式.之后则用先进的CNF SAT求解器zChaff判定积机所生成的布尔公式的可满足性.事例电路验证说明了该方法的有效性.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	熊有伦		97	1709	24.0	37.0
2	刘歆	湖北工业大学电气与电子工程学院	5	5	1.0	2.0