Hardware description with timing requirements

Abstract

Hardware Designs die für sicherheitskritische Anwendungen entwickelt werden müssen unter allen Umständen korrekt funktionieren.<br />Eine Möglichkeit dies sicherzustellen ist durch (i) Beschreiben der Spezifikation in einem formalen Framework und (ii) Beweisen des korrekten Verhaltens der Designs auf der Abstraktionsebene dieses Frameworks. Bei diesem Ansatz bleibt immer noch eine Beweislücke zwischen der Darstellung des Designs im Framework und dessen Codierung in einer für die Fertigung verwendeten Hardware Beschreibungssprache.<br />In dieser Arbeit wird die neue Hardware Beschreibungssprache Dhdl vorgestellt. Dhdl erweitert das Formal Modeling and Analysis Framework von Függer (siehe Matthias Fuegger, Analysis of On-Chip Fault-Tolerant Distributed Algorithms, PhD thesis, Vienna University of Technology, 2010). Dadurch wird die Beweislücke zwischen der formalen Analyse und der Hardware Implementierung geschlos-sen. Mit dem Dhdl spezifischen, semantischen Zeitmodell können auch Simulationsergebnisse von Dhdl in das Formale Framework rückgeführt werden. Die Möglichkeit Zusicherungen über das Zeitverhalten direkt im Dhdl Design selbst zu spezifizieren ist ein großer Vorteil gegenüber aktuell verwendeten Beschreibungssprachen wie VHDL. Um die breite Anwendbarkeit von Dhdl zu zeigen wurden zwei Designs implementiert und deren Zeitverhalten analysiert: ein synchrones, am Beispiel einer einfachen Kaffeemaschine, und ein asynchrones, am Beispiel des DARTS Pulse Generation Algorithmus.<br />

Hardware designs intended for use in high reliability missions are required to behave correctly under all circumstances. One way of establishing their validity is by (i) stating a specification in terms of a formal framework and (ii) proving them correct within the framework.<br />However, a proof gap between the formally stated design and the actual specification in terms of a hardware description language remains.<br />In this thesis, a novel hardware description language, called Dhdl, is introduced. Dhdl is tailored to the formal modeling and analysis framework defined by Függer (see Matthias Fuegger, Analysis of On-Chip Fault-Tolerant Distributed Algorithms, PhD thesis, Vienna University of Technology, 2010). Thereby, it closes the gap between formal proof methods and hardware implementation. With its semantically defined timing model it is even possible to translate traces back to the modeling and analysis framework. The ability to specify timing properties within the design itself is a major advantage of Dhdl to currently popular hardware description languages like VHDL. To demonstrate the wide applicability of Dhdl, both a synchronous (a simple coffee machine) and an asynchronous hardware design, namely the pulse generation algorithm of DARTS, have been implemented and their timing constraints have been analyzed.