SAT-based unbounded symbolic model checking

This paper describes a Boolean satisfiability checking (SAT)-based unbounded symbolic model-checking algorithm. The conjunctive normal form is used to represent sets of states and transition relation. A logical operation on state sets is implemented as an operation on conjunctive normal form formulas. A satisfy-all procedure is proposed to compute the existential quantification required in obtaining the preimage and fix point. The proposed satisfy-all procedure is implemented by modifying a SAT procedure to generate all the satisfying assignments of the input formula, which is based on new efficient techniques such as line justification to make an assignment covering more search space, excluding clause management, and two-level logic minimization to compress the set of found assignments. In addition, a cache table is introduced into the satisfy-all procedure. It is a difficult problem for a satisfy-all procedure to detect the case that a previous result can be reused. This paper shows that the case can be detected by comparing sets of undetermined variables and clauses. Experimental results show that the proposed algorithm can check more circuits than binary decision diagram-based and previous SAT-based model-checking algorithms.
Publisher
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
Issue Date
2005-02
Language
ENG
Keywords

AUTOMATIC VERIFICATION; REACHABILITY ANALYSIS; TEMPORAL LOGIC

Citation

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, v.24, no.2, pp.129 - 140

ISSN
0278-0070
DOI
10.1109/TCAD.2004.841068
URI
http://hdl.handle.net/10203/890
Appears in Collection
EE-Journal Papers(저널논문)
Files in This Item
000226478700001.pdf(551.33 kB)Download
  • Hit : 517
  • Download : 338
  • Cited 0 times in thomson ci
This item is cited by other documents in WoS
⊙ Detail Information in WoSⓡClick to seewebofscience_button
⊙ Cited 9 items in WoSClick to see citing articles inrecords_button

qr_code

  • mendeley

    citeulike


rss_1.0 rss_2.0 atom_1.0