| Because of the difficulty of adequately simulating large digital designs, there has been a recent surge of interest in formal verification, in which a mathematical model of the design is proved to satisfy a precise specification. Model checking is one formal verification technique. It consists of checking that a finite-state model of the design satisfies a specification given in temporal logic, which is a logic that can express properties involving the sequencing of events in time. One of the main drawbacks of model checking is the state explosion problem. This problem occurs in systems composed of multiple processes executing in parallel; the size of the state space generally grows exponentially with the number of components. This thesis considers two methods for avoiding the state explosion problem in the context of model checking: compositional verification and abstraction.; In compositional verification, our goal is to check local properties of the components in the design, deduce that these hold in the global system, and then use them to prove the overall specification. With abstraction, we can hide internal state, replace complex data types with simpler abstract ones, or simplify some of the timing behavior of the components. Using a connection between the abstracted and unabstracted systems, we deduce that whatever properties we prove at the abstract level also hold in the original system. We develop the necessary framework for using these two techniques with model checking, and demonstrate via a number of examples how they can be applied to realistic systems. Our largest example is the cache coherence protocol described in the IEEE Futurebus+ standard. In the course of the verification, we found errors in the standard, and proposed fixes for the protocol. |
