Please use this identifier to cite or link to this item: doi:10.22028/D291-25849
Title: Formal verification of a processor with memory management units
Other Titles: Formale Verifikation eines Prozessors mit Memory Management Units
Author(s): Dalinger, Iakov
Language: English
Year of Publication: 2006
OPUS Scource: 
SWD key words: Prozessor
Verifikation
Speicherverwaltung
Free key words: memory management unit
formal verification
VAMP
processor
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
Abstract: In this thesis we present formal verification of a memory management unit which operates under specific conditions. We also present formal verification of a complex processor VAMP with support of address translation by means of a memory management unit. The is an out-of-order 32 bit RISC CPU with DLX instruction set, fully IEEE-compliant floating point units, and a memory unit. The VAMP also supports precise internal and external interrupts. It is modeled on the gate level and verified with respect to its specification. Subject of this thesis is based on the formal proof of the VAMP without address translation [Bey05] and on paper and pencil specification, implementation, and correctness proof of a memory management unit.
In dieser Dissertation stellen wir die formale Verifikation einer Memory Management Unit vor, welche nur unter bestimmten Operationsbedingungen korrekt arbeitet. Wir stellen auch die formale Verifikation des VAMP vor, eines komplexen Prozessors, der Adressübersetzung unterstützt. Der VAMP ist eine out-of-order 32-Bit RISC CPU mit DLX Instruktionssatz, vollständig IEEE-konformen Fließkommaeinheiten und einer Speichereinheit. Der VAMP unterstützt präzise interne und externe Interrupts. Er ist auf der Gatterebene modelliert und bezüglich einer formalen Spezifikation verifiziert. Diese Arbeit basiert auf dem formalen Beweis des VAMP ohne Adressübersetzung [Bey05] und auf der Papier-und-Bleistift Spezifikation, Implementierung, und dem Korrektheitsbeweis einer Memory Management Unit aus [Hil05].
Link to this record: urn:nbn:de:bsz:291-scidok-6339
hdl:20.500.11880/25905
http://dx.doi.org/10.22028/D291-25849
Advisor: Paul, Wolfgang J.
Date of oral examination: 5-Jun-2006
Date of registration: 11-Jul-2006
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
Dissertation_9032_Dali_Iako_2006.pdf1,35 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.