A Basic Sequential MIPS Machine
We define the basic MIPS instruction set architecture (ISA) without delayed branch, interrupt mechanism and devices. The first Sect. 6.1 of this chapter is very short. It contains a very compact summary of the instruction set architecture (and the assembly language) in the form of tables, which define the ISA if one knows how to interpret them. In Sect. 6.2 we provide a succinct and completely precise interpretation of the tables, leaving out only the coprocessor instructions and the system call instruction. From this we derive in Sect. 6.3 the hardware of a sequential, i.e., not pipelined, MIPS processor and provide a proof that this processor construction is correct.
The ISA is MIPS instead of DLX. Most of the resulting modifications are already handled in the control logic of the ALU and the shift unit.
The machine implements each instruction in one very long hardware cycle and uses only precomputed control. It is not meant to be an efficient sequential implementation and serves later only as a reference machine. This turns most portions of the correctness proof into straightforward bookkeeping exercises, which would be terribly boring if presented in the classroom. We included this bookkeeping only as a help for readers, who want to use this book as a blueprint for formal proofs.
Because the byte addressable memory of the ISA is embedded in the implementation into a 64-bit wide hardware memory, shifters have to be used both for the load and store operations of words, half words, and bytes. In  the memory is 32 bits wide, the shifters for loads and stores are present; they must be used for accesses of half words or bytes. However,  provides no proof that with the help of these shifters loads and stores of half words or bytes work correctly. Subsequent formal correctness proofs for hardware from  as presented in [1, 3, 6] restricted loads and stores to word accesses, and thus, did not provide these proofs either. We present these proofs here; they hinge on the software condition that accesses are aligned and turn out to be not completely trivial.