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
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;
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
DOI :
10.1109/ASICON.2009.5351339