The VAMP Memory Unit
Hardware Design and Formal Verification
Versandkostenfrei!
Versandfertig in 6-10 Tagen
32,99 €
inkl. MwSt.
PAYBACK Punkte
16 °P sammeln!
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 mathemati...
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.
Andere Kunden interessierten sich für
