Bitte benutzen Sie diese Referenz, um auf diese Ressource zu verweisen: doi:10.22028/D291-25904
Titel: Putting it all together : formal verification of the VAMP
Verfasser: Beyer, Sven
Sprache: Englisch
Erscheinungsjahr: 2005
SWD-Schlagwörter: Zweiunddreißig-Bit-Mikroprozessor
Cache-Speicher
RISC
Hardwareverifikation
Formale Methode
Freie Schlagwörter: VAMP
verification
cache memory interface
DDC-Sachgruppe: 004 Informatik
Dokumentart : Dissertation
Kurzfassung: In this thesis we describe the formal verification of a cache memory interface and its integration into a microprocessor called VAMP. The cache memory interface and the VAMP are modeled on the gate level and verified against their respective specifications, i.e., a dual-ported memory for the cache memory interface and the programmer';s model of the VAMP. The cache memory interface features separate instruction and data caches with write back policy for the data cache; the caches are connected to a unified physical memory accesses via a bus protocol with bursts. The VAMP is an out-of-order 32 bit RISC CPU with DLX instruction set, fully IEEE-compliant floating point units, and a memory unit with a cache memory interface. The VAMP also supports precise interrupts. The formal verification of the out-of-order algorithm and the floating point units of the VAMP is not subject of this thesis; we ';only'; put all the different party together to an overall correctness proof.
In dieser Arbeit beschreiben wir die formale Verifikation eines Cache Memory Interfaces und dessen Integration in einen Mikroprozessor, den VAMP. Das Cache Memory Interface und der VAMP werden auf der Gatterebene modelliert und gegen ihre Spezifikation verifiziert, also einen Speicher mit zwei Zugriffsports für das Cache Memory Interface und das Programmiermodell des VAMP. Das Cache Memory Interface besteht aus getrennten Instruktions- und Daten-Caches mit write-back Policy für den Daten-Cache. Die Caches sind mit einem vereinten physikalischen Speicher verbunden, auf den mittels eines Busprotokolls mit Bursts zugegriffen wird. Der VAMP ist eine out-of-order 32-bit RISC CPU mit DLX-Instruktionssatz, vollständig IEEE-konformen Fließkommaeinheiten und einer Speicher-Einheit mit einem Cache Memory Interface. Der VAMP unterstützt auch präzise Interrupts. Die formale Verifikation des out-of-order Algorithmus und der Fließkommaeinheiten des VAMP ist nicht Gegenstand dieser Arbeit; wir setzen lediglich die verschiedenen Teile zusammen zu einem Gesamt-Korrektheitsbeweis.
Link zu diesem Datensatz: urn:nbn:de:bsz:291-scidok-13344
hdl:20.500.11880/25960
http://dx.doi.org/10.22028/D291-25904
Erstgutachter: Paul, Wolfgang J.
Tag der mündlichen Prüfung: 18-Mär-2005
SciDok-Publikation: 16-Nov-2007
Fakultät: Fakultät 6 - Naturwissenschaftlich-Technische Fakultät I
Fachrichtung: MI - Informatik
Fakultät / Institution:MI - Fakultät für Mathematik und Informatik

Dateien zu dieser Ressource:
Datei Beschreibung GrößeFormat 
Dissertation_5315_Beye_Sven_2005.pdf1,74 MBAdobe PDFÖffnen/Anzeigen


Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.