Putting it all together : formal verification of the VAMP

Abstract

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.