Automatic generation of invariants in formal verification of microprocessors and memory systems.

摘要

Formal verification of complex hardware designs is a very challenging process especially for designs such as microprocessors due to their sheer complexity. The main difficulty in verifying such systems is in finding and strengthening invariants. In this thesis, we introduced several techniques to alleviate the problem of finding and strengthening invariants for such systems.; First, we propose a formulation of hardware correctness based on the idea of functional equivalence. We show how functional equivalence can be used to prove the correctness of microprocessors and memory systems and other kinds of hardware. Functional equivalence makes verifying systems such as microprocessors much easier than other approaches in the literature. Moreover, it is applicable to a much larger class of systems.; Then, we introduce a method we call symbolic consistency testing that reduces the effort needed to generate inductive invariants. The method uses k-step induction to strengthen the property (functional equivalence) and relies on the user to find symbolic test vectors . These test vectors are used to eliminate existential quantifiers in the k-step induction using a technique we call predicate instantiation. We show how this method works successfully on a number of examples of cached memory systems.; To further reduce the manual effort needed to verify such systems, we introduce a refinement heuristic that tries to automatically find the symbolic test vectors. The heuristic finds the required test vectors for all the examples we consider very quickly.; We also introduced a semi-formal method that can be used with systems that are too complex for symbolic consistency testing. This is a debugging method that uses structural constraints within the system to remove incoherent states from the state space. This method is able to find all bugs in our examples and it is in general more efficient than symbolic consistency testing.; Finally, we introduce a sound and complete abstraction method that maps an infinite system to a finite system that can be verified with model checking techniques. This abstraction technique applies only to a certain class of systems what we characterize.