The VAMP Memory Unit - Dalinger, Iakov;Alekhin, Artem
32,99 €
inkl. MwSt.
Versandkostenfrei*
Versandfertig in 6-10 Tagen
  • Broschiertes Buch

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…mehr

Andere Kunden interessierten sich auch für
Produktbeschreibung
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.
Autorenporträt
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.