The VAMP Memory Unit : Hardware Design and Formal Verification

ISBN-13: 9783639088793 / Angielski / Miękka / 2009 / 116 str.

Iakov Dalinger; Artem Alekhin

Opis

This work is devoted to the formal verification ofthe VAMP memory unit (MU) and based on the workcarried out in [Dal06]. The new design of the MU,developed here, contains translation look-asidebuffers (TLB) for fast virtual address translationinside the memory management units (MMU) and supportsaccesses to external devices.A computer-aided verification tool used throughoutthe whole work is an interactive theorem proverIsabelle/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. Thework is described formally and paper-and-pencilproofs are provided.

O autorze

I.Dalinger: Born in 1979. He received PhD degree from Saarland
University in 2006. Now, he is deputy vice-president for science
of Saint-Petersburg State University of Civil Aviation.
A.Alekhin: Born in 1983. He received MSc degree in computer
science from Saarland University in 2009. Now, he works as a
scientific researcher in Saarland University.