Acceleration of SAT-Based Iterative Property Checking

  • Daniel Große
  • Rolf Drechsler
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


Formal property checking is used to check whether a circuit satisfies a temporal property or not. An important goal during the development of properties is the formulation of general proofs. Since assumptions of properties define the situations under which the commitments are checked, in order to obtain general proofs assumptions should be made as general as possible. In practice this is accomplished iteratively by generalizing the assumptions step by step. Thus, the veri.cation engineer may start with strong assumptions and weakens them gradually.

In this paper we propose a new approach to speed up SAT-based iterative property checking. This process can be exploited by reusing conflict clauses in the corresponding SAT instances of consecutive property checking problems. By this the search space is pruned, since recomputations of identical conflicts are avoided.


Symbolic Model Check Bound Model Check Model Check Problem Property Check Conflict Clause 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  2. 2.
    Große, D., Drechsler, R.: CheckSyC: An efficient property checker for RTL SystemC designs, pp. 4167–4170 (2005)Google Scholar
  3. 3.
    Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an efficient SAT solver. In: Design Automation Conf., pp. 530–535 (2001)Google Scholar
  4. 4.
    Shtrichman, O.: Pruning techniques for the SAT-based bounded model checking problem, pp. 58–70 (2001)Google Scholar
  5. 5.
    Winkelmann, K., Trylus, H.-J., Stoffel, D., Fey, G.: A cost-efficient block verification for a UMTS up-link chip-rate coprocessor. In: Design, Automation and Test in Europe, vol. 1, pp. 162–167 (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Daniel Große
    • 1
  • Rolf Drechsler
    • 1
  1. 1.Institute of Computer ScienceUniversity of BremenBremenGermany

Personalised recommendations