Formal verification techniques based on Boolean satisfiability problem

	Formal verification techniques based on Boolean satisfiability problem
	Li, XW ; Li, GH ; Shao, M
	2005
发表期刊	JOURNAL OF COMPUTER SCIENCE AND TECHNOLOGY
ISSN	1000-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.