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.

The second exam is on Friday 23th. If you wiil participate, send an e-mail to the assistant.

The list of topics for the exam is available.