Acceleration of SAT-Based Iterative Property Checking
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.
KeywordsSymbolic Model Check Bound Model Check Model Check Problem Property Check Conflict Clause
- 2.Große, D., Drechsler, R.: CheckSyC: An efficient property checker for RTL SystemC designs, pp. 4167–4170 (2005)Google Scholar
- 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.Shtrichman, O.: Pruning techniques for the SAT-based bounded model checking problem, pp. 58–70 (2001)Google Scholar
- 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