We develop at the gate level a complete floating point execution unit (including division/multiplication), a tomasulo out-of-order scheduler, and a memory management unit for the DLX processor from computer architecture I.
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.
This lecture will be in English!