Up to now, when discussing refinement verification, we've considered only the transfer of data from one place to another, without actually operating on the data. Now we'll have a look at how to verify instruction set processors, that is, machines that input a sequence of operations to be performed on some data structure, such as a register file or a memory. In this case, our abstract model is usually an ``instruction set architecture'' (ISA). This is represented by a simple sequential machine the processes instructions on at a time, in the order they are received. The implementation is usually a more complex machine that works on more than one instruction at a time. This can be done, for example, by pipelining, or out-of-order execution techniques.

The key to verification of such designs in SMV is to break the problem
up into individual instructions. Usually, we break an instruction up
into two parts, which correspond to two lemmas in the proof. The
first lemma is that all the operands fed to the function unit(s) are
correct, according to the abstract model. The second is that all
results produced by the functional unit(s) are correct (again, with
respect to the abstract model). Needless to say, we use lemma 1 to
prove lemma 2, and *vice versa*. The reason for breaking the
problem into two lemmas is that the operand fetching operation and the
functional unit operation are somewhat different in nature, so it's
convenient to separate the two issues, so we can apply a different
proof approach to each (much as we separated the issues of data
correctness and ordering in the circular buffer).

Now, in order to specify that the operands and results are correct with respect to the abstract model, we usually have to add some auxiliary information to the implementation (see the previous section). In this case, we add to each instruction moving through the implementation a few extra fields to store the correct operands and results for that instruction, as computed by the abstract model.

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