[ main page ] [ back ]

2011 : Hardware Description with Timing Requirements

Author(s)
Stefan Resch
Abstract
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. However, a proof gap between the formally stated design and the actual specification in terms of a hardware description language remains. 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 in [9]. 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 [21], have been successfully implemented and their timing constraints have been verified.
Bibtex
@mastersthesis{ resch:2011,
  author =      "Stefan Resch",
  title =       "Hardware Description with Timing Requirements",
  address =     "Treitlstr. 3/3/182-1, 1040 Vienna, Austria",
  school =      "Technische Universit{\"a}t Wien, Institut f{\"u}r Technische Informatik",
  year =        "2011"
}
Download


[ main page ] [ back ]