Dalinger, I: The VAMP Memory Unit Hardware Design and Formal Verification
-
- Englisch ausgewählt
Fr. 76.90
inkl. gesetzl. MwSt.,
Beschreibung
Produktdetails
Einband
Taschenbuch
Erscheinungsdatum
01.02.2009
Verlag
VDMSeitenzahl
116
Maße (L/B/H)
22/15/0.7 cm
Gewicht
189 g
Sprache
Englisch
ISBN
978-3-639-08879-3
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.
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.
Kundinnen und Kunden meinen
Verfassen Sie die erste Bewertung zu diesem Artikel
Helfen Sie anderen Kund*innen durch Ihre Meinung