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