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:

Friday July 25th:
11:30 Oleg Parshin Gennady Shmonin
12:00 Alexandra Tsyban Pawel Klepkin
13:45 Vasily Tsyba Alexey Podgaev

Thursday September 11th:
09:00Rupali MukherjeeSafura Raisi
09:45Ralisa AngeloveRuzica Piskac
10:45Jan DörrenbächerStefan Maus
11:30Kara QadarWaqar Saleem
14:00Christian HennrichRalf Tschuncky
14:45Herve PeuengueuDominik Rester