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 int 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 probelm 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 issuues, 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 respct 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.