位置:成果数据库 > 期刊 > 期刊详情页
用布尔可满足性验证逻辑电路的等价性
  • ISSN号:1004-132X
  • 期刊名称:《中国机械工程》
  • 时间:0
  • 分类:TP274[自动化与计算机技术—控制科学与工程;自动化与计算机技术—检测技术与自动化装置]
  • 作者机构:[1]湖北工业大学电气与电子工程学院,湖北武汉430068
  • 相关基金:国家自然科学基金(50390060,50335020).
中文摘要:

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

英文摘要:

This paper presents the equivalence verification method of digital circuits by means of Boolean Satisfiability (SAT). It first extracts the circuit under test into a finite state machine (FSM), and then builds a product machine of two finite state machines, which transforms the problem of equivalence of two circuits into the one of the asserted product machine. The Tseitin's transformation method is improved and is used for converting the circuit constrained problems to CNF (Conjunctive Normal Form) formulas. Its satisfiability is then handed over to the state-of-the-art solver Chaff to check. The testing of example circuits demonstrates the effectiveness of this approach.

同期刊论文项目
期刊论文 339 会议论文 107 著作 6
期刊论文 119 会议论文 27 获奖 9 著作 3
同项目期刊论文
期刊信息
  • 《中国机械工程》
  • 中国科技核心期刊
  • 主管单位:中国科学技术协会
  • 主办单位:中国机械工程学会
  • 主编:董仕节
  • 地址:湖北工业大学772信箱
  • 邮编:430068
  • 邮箱:paper@cmemo.org.cn
  • 电话:027-87646802
  • 国际标准刊号:ISSN:1004-132X
  • 国内统一刊号:ISSN:42-1294/TH
  • 邮发代号:38-10
  • 获奖情况:
  • 1997年获中国科协期刊一等奖,第二届全国优秀科技...,机械行业优秀期刊一等奖,1999年获首届国家期刊奖,2001年获首届湖北十大名刊,中国期刊方阵“双高”期刊,2003第二届国家期刊奖提名奖,百种中国杰出学术期刊
  • 国内外数据库收录:
  • 俄罗斯文摘杂志,美国化学文摘(网络版),荷兰文摘与引文数据库,美国剑桥科学文摘,英国科学文摘数据库,日本日本科学技术振兴机构数据库,中国中国科技核心期刊,中国北大核心期刊(2004版),中国北大核心期刊(2008版),中国北大核心期刊(2011版),中国北大核心期刊(2014版),中国北大核心期刊(2000版)
  • 被引量:50788