TU Darmstadt / ULB / tuprints

Ein transformativer Ansatz für die Synthese und Verifikation algorithmischer Hardwarebeschreibungen

Hinrichsen, Holger :
Ein transformativer Ansatz für die Synthese und Verifikation algorithmischer Hardwarebeschreibungen.
[Online-Edition]
TU Darmstadt
[Ph.D. Thesis], (2001)

[img]
Preview
PDF
hinrichsen.pdf
Available under Simple publication rights for ULB.

Download (1173Kb) | Preview
Item Type: Ph.D. Thesis
Title: Ein transformativer Ansatz für die Synthese und Verifikation algorithmischer Hardwarebeschreibungen
Language: German
Abstract:

In dieser Arbeit wird ein Verfahren der formal korrekten Synthese vorgestellt, mit Hilfe dessen ein automatisierter Entwurf von Prozessoren mit Pipelining möglich ist. Das Verfahren basiert auf einer kleinen Menge korrektheitserhaltender Transformationen, deren Anwendung effizient durch eine unabhängige Post-Synthese-Verifikation überprüft wird. Zur Spezifikation dient eine im Rahmen dieser Arbeit entwickelte, experimentelle Hardwarebeschreibungssprache LLS (Language of Labelled Segments). Der transformale Ansatz kann neben der Synthese auch zur Verifikation genutzt werden. Ein automatisches Verfahren wird vorgestellt, daß die Äquivalenz eines Entwurfs vor und nach dem Einplanungsschritt der High-Level-Synthese nachweist. Durch Anwenden von Transformationen kann die Äquivalenz zweier Beschreibungen gezeigt werden. Die Äquivalenz ist gegeben, wenn eine Folge korrektheitserhaltender Transformationen existiert, die die eine in die andere Beschreibung umwandelt. Insbesondere Ergebnisse moderner Einplanungsverfahren wie z.B. AFAP und DLS können mit dem vorgestellten Verfahren, das sowohl auf zyklischen Kontrollflußgraphen als auch für Pipeline-Systeme arbeitet, verifiziert werden.

Alternative Abstract:
Alternative AbstractLanguage
A method of formally correct synthesis is presented and applied to the automatic construction of pipelined processors. The approach is based on a small set of correctness-preserving transformations that are efficiently cross-checked by an independent formal verification tool. For specification an experimental hardware description language LLS (Language of Labelled Segments) is used. The transformational technique can also be used for verification. A method for the fully automatic equivalence verification of a design before and after the scheduling step of high-level synthesis is presented. The equivalence of two descriptions is given if a sequence of transformations exists which turns the first description into the second. The technique is applicable to the results of advanced scheduling methods like AFAP and DLS, which work on cyclic control flows, as well as to pipelined designs.English
Uncontrolled Keywords: formale Synthese
Alternative keywords:
Alternative keywordsLanguage
formale SyntheseGerman
hardware synthesis, formal synthesis, formal verificationEnglish
Classification DDC: 600 Technik, Medizin, angewandte Wissenschaften > 620 Ingenieurwissenschaften
Divisions: Fachbereich Elektrotechnik und Informationstechnik
Date Deposited: 17 Oct 2008 09:20
Last Modified: 07 Dec 2012 11:46
Official URL: http://elib.tu-darmstadt.de/diss/000110
URN: urn:nbn:de:tuda-tuprints-1108
License: Simple publication rights for ULB
Referees: Eveking, Prof.Dr. H. and Hoffmann, Dr. R.; Prof.
Advisors: Eveking, Dr. H.; Prof.
Refereed: 4 December 2000
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/110
Export:

Actions (login required)

View Item View Item