We develop at the gate level most of the schematics of a processor
with superpipelining, delayed branch, forwarding, hardware interlock,
speculative execution, caches, nested precise interrupts and out of order
execution.
We prove the correctness of most constructions.
The foremost motivation for presenting mathematical correctness proofs is
efficiency of teaching: computer architecture is complicated (unless one ignores crucial details) and the proper use of mathematics permits even the explanation of complicated things at a relaxed pace.
The second motivation is formal verification: our correctness proofs can be
entered into and verified by interactive theorem provers.