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.

Oral exam takes place on 24.02.2005 and 25.02.2005. We will exam two students at the same time. So, you have to decide with whom you want to go to the exam. If you can not find a partner we will do it for you ;)
To register for the exam send an e-mail to deru AT with subject "CAI exam registration" and in the body your Name, Matr. Number and the desired time for the exam. Desired time has to have the following format:
Day : Time, where Day in {24, 25} and Time in {9,10,11,14,15,16,17}

Deadline for the registration is 21.02.2005

The list of participators and time slots will be published on 22.02.2004