Refinement verification is methodology of verifying that the
functionality of an abstract system model is correctly implemented by
a low-level implementation. It can be used, for example, to verify
that a packet router or bus protocol, modeled at the clock-cycle
level, correctly implements a given abstract model of end-to-end data transfer.
Similarly one can verify that a clock-accurate model of a pipelined,
out-of-order processor correctly implements a given instruct-set
architecture (*i.e.*, a programmer's model of a machine).

By breaking a large verification problem into small, manageable
parts, the refinement methodology makes it possible to verify designs
that are much too large to be handled directly by model checking.
This decomposition of the verification problem is enabled by specifying
*refinement maps* that translate the behavior of the abstract model
into the behavior of given interfaces and structures in the low-level
design. This makes it possible to verify small parts of the low-level
design in the context of the abstract model. Thus, the proof obligations
can be reduced to a small enough scale to be verified by model checking.

SMV supports this methodology by allowing one to specify many abstract
definitions for the same signal. A new construct called a ``layer'' is
introduced for this purpose. A layer is a collection of abstract signal definitions. A
layer can, for example, define low-level implementation signals as a
function of abstract model signals, and thus provide a refinement map
(*i.e.*, a translation between abstraction levels). The low-level
implementation of a signal must be simultaneously consistent with all of
its abstract definitions. Thus, each abstract definition entails a
verification task - to show that every implementation behavior is
allowed by this definition. For the purpose of this verification task,
one may use whichever abstract definition is most convenient for
defining of the other signals. Suppose, for example, that we have
abstract definitions of both the inputs and outputs of a given
low-level block as a function of a high-level model, as depicted in
figure 1. We can use the abstract definitions of the
inputs to drive the inputs of the block from the high-level model when
verifying that the outputs are consistent with their abstract
definitions. Thus, the abstract model provides the context (or environment)
for verifying the block, and we do not need to consider the remainder
of the low-level model.

SMV also supports design by a successive refinement. One can define a sequence of layers, each of which is more detailed than the previous layer. The implementation of each signal is given by the lowest-level definition in the hierarchy.

- Layers
- Refinement maps

- Decomposing large data structures
- Exploiting Symmetry
- Decomposing large structures in the implementation
- Case analysis

- Data type reductions

- Proof by induction

- Instruction processors
- A very simple example
- Uninterpreted functions
- Plugging in interpretations for function symbols
- What about outputs?

- An out-of-order instruction processor
- Tomasulo's algorithm
- The abstract model
- Implementation
- Refinement maps
- Case splitting
- The proof
- Abstract counterexamples
- Multiple execution units
- Proving non-interference
- Adding a reorder buffer
- Proving liveness

- Bit vectors as scalarsets
- Propagation of unknown values
- Conditional proof statements, and course-of-values induction