TU Darmstadt / ULB / TUprints

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

Hinrichsen, Holger (2001)
Ein transformativer Ansatz für die Synthese und Verifikation algorithmischer Hardwarebeschreibungen.
Technische Universität
Ph.D. Thesis, Primary publication

[img]
Preview
PDF
hinrichsen.pdf
Copyright Information: In Copyright.

Download (1MB) | Preview
Item Type: Ph.D. Thesis
Type of entry: Primary publication
Title: Ein transformativer Ansatz für die Synthese und Verifikation algorithmischer Hardwarebeschreibungen
Language: German
Referees: Eveking, Prof.Dr. H. ; Hoffmann, Prof. R.
Advisors: Eveking, Dr. H.; Prof.
Date: 26 March 2001
Place of Publication: Darmstadt
Date of oral examination: 4 December 2000
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
URN: urn:nbn:de:tuda-tuprints-1108
Classification DDC: 600 Technology, medicine, applied sciences > 620 Engineering and machine engineering
Divisions: 18 Department of Electrical Engineering and Information Technology
Date Deposited: 17 Oct 2008 09:20
Last Modified: 21 Mar 2016 10:56
URI: https://tuprints.ulb.tu-darmstadt.de/id/eprint/110
PPN:
Export:
Actions (login required)
View Item View Item