The abstract interpretation framework used to analyze worst case cache behavior for real-time system works well for caches with least-recently-used (LRU) replacement. We give insights into why LRU is amenable to analysis and contrast this with a cache using FIFO (first-in, first-out) replacement, where no tight and at the same time safe upper bound on cache misses can be given.

The current approach evaluates each memory access in a program to decide its cache behavior. Another approach to cache analysis is to bound the total number of misses that can occur in parts of a given program. We outline research issues that will hopefully lead to better bounds on cache behavior in the future.

Several processor features hinder precise prediction of program execution times on real-time systems. We show some examples where the processor behavior is hard to model for analysis due peculiarities in the processor's design. Upon that, we formulate principles that a processor designed for predictability must meet. Based on these principles, we give a design of a hard real-time processor with predictable timing, which is simultaneously capable of reaching respectable performance levels.

Hardware zur Behandlung von Gleitkommazahlen ist sehr komplex und Korrektheit kann nicht alleine durch Tests sichergestellt werden. Mittels formaler Verifikation wird die Übereinstimmung der Hardware mit einer Spezifikation bewiesen.

Ich stelle das VAMP-Projekt vor, in dem am Lehrstuhl Paul der RISC-Prozessor VAMP (Verified Architecture MicroProcessor) verifiziert wird. Die Floating Point Unit (FPU) des VAMP unterstützt die Operationen Addition/Subtraktion, Multiplikation/Division, Vergleiche und Konversionen. Denormale Zahlen und Exceptions werden in Hardware behandelt.

Die Schaltkreise der VAMP-FPU werden auf Gatterebene (d.h. mit UND/ODER/NICHT-Gattern) in der Sprache des Theorembeweisers PVS implementiert. Gleichzeitig wird der IEEE Standard 754, in dem Gleitkomma-Arithmetik definiert wird, in PVS formalisiert. Die Spezifikation der FPU sagt nun aus, daß die von der FPU ausgeführten Rechnungen dem IEEE-Standard entsprechen. Die Übereinstimmung der Implementierung mit der Spezifikation wird mittels PVS bewiesen.

Der Vortrag gibt einen Überblick über das Verifikations-Projekt und skizziert den Beweisansatz. Als Ausblick wird auf die Implementierung des VAMP auf einem FPGA eingegangen.

We describe the results and status of a project aiming to provide a provably correct library of basic circuits. We use the theorem proving system PVS in order to prove circuits such as incrementers, adders, arithmetic units, multipliers, leading zero counters, shifters, and decoders. All specifications and proofs are available on the web.