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 pr oof 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 a re then discharged by model checking. The proof strategy uses proof techniq ues for design refinement, temporal case splitting, data-type reduction and the exploitation of symmetry. Uninterpreted functions can be used to abstr act operations on data. A proof system supporting this approach generates v erification subgoals to be discharged by the SMV symbolic model checker. Ap plication of the methodology is illustrated using an implementation of Toma sulo's algorithm, a packet buffering device and a cache coherence protocol as examples. (C) 2000 Published by Elsevier Science B.V. All rights reserve d.