Abstract: Compositional model checking methods can be used to reduce the formal verification of a complex system to model checking problems of tractably small size. However, such techniques are difficult to apply to systems that have large data types, such as memory addresses, or large data arrays such as memories or FIFO buffers. They are also limited to the verification of systems with fixed finite resources. In this paper, a method of compositional verification is presented that uses the combination of temporal case splitting and data type reductions to reduce types of unbounded range to small finite types, and arrays of unbounded size to small fixed-size arrays. The method also supports the use of uninterpreted functions in a novel way, that allows model checking to be applied to systems with uninterpreted functions. These techniques are implemented in a proof assistant that also supports compositional reasoning and reductions via symmetry. Application of the method is illustrated by using this tool to verify an implementation of Tomasulo's algorithm. The use of temporal case splitting, data type reductions and and uninterpreted functions substantially simplifies the proof for fixed finite configurations, and also allows a generic verification for configurations of arbitrary word size, arbitrary register file size, arbitrary number of reservation stations and arbitrary number of execution units.
Abstract: Compositional proofs about systems of many components often involve apparently circular arguments. That is, correctness of component A must be assumed when verifying component B, and vice versa. The apparent circularity of such arguments can be resolved by induction over time. However, previous methods for such circular compositional reasoning apply only to safety properties. This paper presents a method of circular compositional reasoning that applies to liveness properties as well. It is based on a new circular compositional rule implemented in the SMV proof assistant. The method is illustrated using Tomasulo's algorithm for out-of-order instruction execution. An implementation is proved live for arbitrary resources using compositional model checking.
Abstract: 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.
Abstract: A method of automatic abstraction is presented that uses proofs of unsatisfiability derived from SAT-based bounded model checking as a guide to choosing an abstraction for unbounded model checking. Unlike earlier methods, this approach is not based on analysis of abstract counterexamples. The performance of this approach on benchmarks derived from microprocessor verification indicates that SAT solvers are quite effective in eliminating logic that is not relevant to a given property. Moreover, benchmark results suggest that when bounded model checking successfully terminates, and the problem is unsatisfiable, the number of state variables in the proof of unsatisfiability tends to be small. In all cases tested, when bounded model checking succeeded, unbounded model checking of the resulting abstraction also succeeded.