DC FieldValueLanguage
dc.contributor.advisorSteininger, Andreas-
dc.contributor.authorResch, Stefan-
dc.date.accessioned2020-06-30T05:19:47Z-
dc.date.issued2011-
dc.date.submitted2011-11-
dc.identifier.urihttps://resolver.obvsg.at/urn:nbn:at:at-ubtuw:1-48081-
dc.identifier.urihttp://hdl.handle.net/20.500.12708/10654-
dc.descriptionZsfassung in dt. Sprache-
dc.description.abstractHardware 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 />de
dc.description.abstractHardware 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.en
dc.formatviii, 114 Bl.-
dc.languageEnglish-
dc.language.isoen-
dc.subjectHardware Designde
dc.subjectHardware nahe Programmiersprachede
dc.subjectVHDLde
dc.subjectVLSIde
dc.subjectasynchrones Designde
dc.subjectDARTSde
dc.subjectZeitzusicherungde
dc.subjecthardware designen
dc.subjecthardware descriptionen
dc.subjectVHDLen
dc.subjectVLSIen
dc.subjectasynchronous designen
dc.subjectDARTSen
dc.subjecttiming requirementen
dc.titleHardware description with timing requirementsen
dc.typeThesisen
dc.typeHochschulschriftde
tuw.publication.orgunitE182 - Institut für Technische Informatik-
dc.type.qualificationlevelDiploma-
dc.identifier.libraryidAC07812034-
dc.description.numberOfPages114-
dc.identifier.urnurn:nbn:at:at-ubtuw:1-48081-
dc.thesistypeDiplomarbeitde
dc.thesistypeDiploma Thesisen
item.fulltextwith Fulltext-
item.openairetypeThesis-
item.openairetypeHochschulschrift-
item.cerifentitytypePublications-
item.cerifentitytypePublications-
item.languageiso639-1en-
item.grantfulltextopen-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
item.openairecristypehttp://purl.org/coar/resource_type/c_18cf-
Appears in Collections:Thesis

Files in this item:

Show simple item record

Page view(s)

9
checked on Apr 9, 2021

Download(s)

63
checked on Apr 9, 2021

Google ScholarTM

Check


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