DocumentCode :
2650448
Title :
Enhance SAT conflict analysis for model checking
Author :
Ming-e Jing ; Chen, Gengshen ; Yin, Wenbo ; Zhou, Dian
Author_Institution :
State Key Lab. of ASIC & Syst., Fudan Univ., Shanghai, China
fYear :
2009
fDate :
20-23 Oct. 2009
Firstpage :
686
Lastpage :
689
Abstract :
Bounded model checking shows that satisfiability (SAT) problem can be widely used for model checking. The performance of SAT solver depends heavily on the quality of the learnt clauses in the conflict analysis process. Combining with the characters of model checking, we propose to add efficient implied clauses to the clause database to enhance the conflict analysis. Experimental results show that the average running time of our algorithm is reduced by 35% compared with the traditional FUIP algorithm.
Keywords :
circuit analysis computing; computability; directed graphs; formal verification; integrated circuit design; FUIP algorithm; IC design process; SAT conflict analysis; SAT solver; conflict analysis process; directed acyclic graph; model checking; satisfiability problem; Business continuity; Databases; Design methodology; Formal verification; Interpolation; Laboratories; Large-scale systems; Performance analysis; Process design; Testing; Conflict analysis; Implication graph; Model checking; Satisfiability problem;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
ASIC, 2009. ASICON '09. IEEE 8th International Conference on
Conference_Location :
Changsha, Hunan
Print_ISBN :
978-1-4244-3868-6
Electronic_ISBN :
978-1-4244-3870-9
Type :
conf
DOI :
10.1109/ASICON.2009.5351339
Filename :
5351339
Link To Document :
بازگشت