DocumentCode :
1835700
Title :
Learning from BDDs in SAT-based bounded model checking
Author :
Gupta, Aarti ; Ganai, Malay ; Wang, Chao ; Yang, Zijiang ; Ashar, Pranav
Author_Institution :
NEC Labs America, Princeton, NJ, USA
fYear :
2003
fDate :
2-6 June 2003
Firstpage :
824
Lastpage :
829
Abstract :
Bounded Model Checking (BMC) based on Boolean Satisfiability (SAT) procedures has recently gained popularity as an alternative to BDD-based model checking techniques for finding bugs in large designs. In this paper, we explore the use of learning from BDDs, where learned clauses generated by BDD-based analysis are added to the SAT solver, to supplement its other learning mechanisms. We propose several heuristics for guiding this process, aimed at increasing the usefulness of the learned clauses, while reducing the overheads. We demonstrate the effectiveness of our approach on several industrial designs, where BMC performance is improved and the design can be searched up to a greater depth by use of BDD-based learning.
Keywords :
Boolean functions; binary decision diagrams; computability; formal verification; integrated circuit design; learning (artificial intelligence); logic CAD; BDD; BDD-based analysis; BDD-based learning; BMC; Boolean satisfiability; SAT solver; binary decision diagram; bounded model checking; industrial design; learned clauses; learning mechanism; overhead reduction; property checking; Binary decision diagrams; Boolean functions; Chaos; Circuits; Computer bugs; Data structures; Hardware; Learning systems; National electric code; Permission;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Design Automation Conference, 2003. Proceedings
Print_ISBN :
1-58113-688-9
Type :
conf
DOI :
10.1109/DAC.2003.1219133
Filename :
1219133
Link To Document :
بازگشت