A methodology for hardware verification using compositional model checking

A methodology for system-level hardware verification based on compositional model checking is described. This methodology relies on a simple set of proof techniques, and a domain specific strategy for applying them. The goal of this strategy is to reduce the verification of a large system to finite state subgoals that are tractable in both size and number. These subgoals are then discharged by model checking. The proof strategy uses proof techniques for design refinement, temporal case splitting, data-type reduction and the exploitation of symmetry. Uninterpreted functions can be used to abstract operations on data. A proof system supporting this approach generates verification subgoals to be discharged by the SMV symbolic model checker. Application of the methodology is illustrated using an implementation of Tomasuloʹs algorithm, a packet buffering device and a cache coherence protocol as examples.