CSpace  > 中国科学院计算技术研究所期刊论文  > 英文
Formal verification techniques based on Boolean satisfiability problem
Li, XW; Li, GH; Shao, M
2005
发表期刊JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY
ISSN1000-9000
卷号20期号:1页码:38-47
摘要This paper exploits Boolean satisfiability problem in equivalence checking and model checking respectively. A combinational equivalence checking method based on incremental satisfiability is presented. This method chooses the candidate equivalent pairs with some new techniques, and uses incremental satisfiability algorithm to improve its performance. By substituting the internal equivalent pairs and converting the equivalence relations into conjunctive normal form (CNF) formulas, this approach can avoid the false negatives, and reduce the search space of SAT procedure. Experimental results on ISCAS'85 benchmark circuits show that, the presented approach is faster and more robust than those existed in literature. This paper also presents an algorithm for extracting of unsatisfiable core, which has an important application in abstraction and refinement for model checking to alleviate the state space explosion bottleneck. The error of approximate extraction is analyzed by means of simulation. An analysis reveals that an interesting phenomenon occurs, with the increasing density of the formula, the average error of the extraction is decreasing. An exact extraction approach for MU subformula, referred to as pre-assignment algorithm, is proposed. Both theoretical analysis and experimental results show that it is more efficient.
关键词equivalence checking incremental satisfiability minimal unsatisfiable formula model checking
收录类别SCI
语种英语
WOS研究方向Computer Science
WOS类目Computer Science, Hardware & Architecture ; Computer Science, Software Engineering
WOS记录号WOS:000227033400003
出版者SCIENCE CHINA PRESS
引用统计
被引频次:5[WOS]   [WOS记录]     [WOS相关记录]
文献类型期刊论文
条目标识符http://119.78.100.204/handle/2XEOYT63/10009
专题中国科学院计算技术研究所期刊论文_英文
通讯作者Li, XW
作者单位1.Chinese Acad Sci, Comp Technol Inst, Beijing 100080, Peoples R China
2.Zhejiang Forestry Coll, Sch Informat Engn, Hangzhou 311300, Peoples R China
3.Chinese Acad Sci, Grad Sch, Beijing 100039, Peoples R China
推荐引用方式
GB/T 7714
Li, XW,Li, GH,Shao, M. Formal verification techniques based on Boolean satisfiability problem[J]. JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY,2005,20(1):38-47.
APA Li, XW,Li, GH,&Shao, M.(2005).Formal verification techniques based on Boolean satisfiability problem.JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY,20(1),38-47.
MLA Li, XW,et al."Formal verification techniques based on Boolean satisfiability problem".JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY 20.1(2005):38-47.
条目包含的文件
条目无相关文件。
个性服务
推荐该条目
保存到收藏夹
查看访问统计
导出为Endnote文件
谷歌学术
谷歌学术中相似的文章
[Li, XW]的文章
[Li, GH]的文章
[Shao, M]的文章
百度学术
百度学术中相似的文章
[Li, XW]的文章
[Li, GH]的文章
[Shao, M]的文章
必应学术
必应学术中相似的文章
[Li, XW]的文章
[Li, GH]的文章
[Shao, M]的文章
相关权益政策
暂无数据
收藏/分享
所有评论 (0)
暂无评论
 

除非特别说明,本系统中所有内容都受版权保护,并保留所有权利。