The VAMP Memory Unit

This work is devoted to the formal verification of the VAMP memory unit (MU) and based on the work carried out in [Dal06]. The new design of the MU developed here contains translation look-aside buffers (TLB) for fast virtual address translation inside the memory management units (MMU) and supports accesses to external devices. A computer-aided verification tool used throughout the whole work is an interactive theorem prover Isabelle/HOL bound [Tve05] with the NuSMV [CCG+02] and SMV [McM99] model checkers. The results (correctness proofs and models of hardware blocks) are presented as Isabelle mathematical theories. The work is described formally and paper-and-pencil proofs are provided.