Formal verification of a processor with memory management units
Iakov Dalinger · MPG.PuRe (Max Planck Society) · 2006
In this thesis we present formal verification of a memory management unit which operates under specific conditions. We also present formal verification of a complex processor VAMP with support of address translation by means of a memory management unit. The VAMP is an out-of-order 32 bit RISC CPU with DLX instruction set, fully IEEE-compliant floating point units, and a memory unit. The VAMP also supports precise internal and external interrupts. It is modeled on the gate level and verified with respect to its specification. Subject of this thesis is based on the formal proof of the VAMP without address translation [Bey05] and on paper and pencil specification, implementation, and correctness proof of a memory management unit [Hil05].