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

This lecture will be in English!

second date for examen: wednesday april 23rd


Time We 30.04. Mo 05.05.
14:45 Mohammed Ali Assoudeh Safura Raisi
15:30 Venkaia Krishna Taiwicheria Subramanyam Nadavala Viktor Steiz
16:15 Hermann Prediger Andrej Rioumin