Main Page
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!

Schedule for exams:

Thursday November 4th:
14:00 Stilian Stanev Rostislav Rusev
14:45 Anna Marchenkova Mario Manchino

Friday November 5th:
09:00 Yury Chebiryak Sabine Fischer
09:45 Steffen Knapp Verena Kremer
10:30 Li Wang Dieter Brunotte
11:30 Peter Böhm Hristo Tzigarov
14:00 Stephen Kemmerling Christian Michalk
14:45 Sebastian Altmeyer Christian Hümbert
15:30 Andrey Shadrin Vladimir Boyarinov