Acceleration of SAT-Based Iterative Property Checking

Today, verification is becoming the dominating factor for successful circuit designs. In this context formal verification techniques allow to prove the correctness of a circuit and meanwhile are standard in many design flows. Formal property checking is used to check whether a circuit satisfies a temporal property. 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 verification 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 ...

• Type: Conference
• Year: 2005
• Where: CHARME
• Authors: Daniel Große, Rolf Drechsler
• Keywords: CHARME 2005, Formal Property Checking, General Proofs, Hardware, Property Checking