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!