| Model checking is a widely used automatic formal verification technique. Despite the recent advances in model checking technology, its application is still limited by the state explosion problem. For model checking large techniques for the efficient verification of hardware designs with thousands of registers.; A technique, called SAT conflict dependency analysis, If a CNF formula is unsatisfiable, this technique can extract a proof of unsatisfiability by analyzing conflict; clauses and conflict graphs generated by the SAT procedure.; In this thesis, we propose two new algorithms to improve the efficiency of traditional localization reduction based methods. The first algorithm combines multiple verification engines including BDD, ATPG, refinement. When the SAT solver determines that there are no concrete counterexamples proof using the SAT conflict dependency analysis. The second algorithm identifies a set of registers for refinement based on the extracted proof.; for verifying infinite state systems. They become inefficient when applied to the verification of large scale hardware designs. We improve the existing model is refined by adding compact predicates and general transition constraints identified by unsatisfiability proofs. Third, existing refinement algorithms can add unnecessary predicates, called redundant predicates. We propose algorithms to identify and remove the redundant predicates. Fourth, to exploit high level information from Verilog designs, a method is developed to extract relevant branch conditions that can be used as predicates during refinement. Finally, successfully applied to the verification of industrial hardware designs with up to six thousand registers and 250 thousand gates. |
