TUD Technische Universität Darmstadt
Hessische Landes-und Hochschulbibliothek
HLuHB

EPDA - Elektronische Publikationen Darmstadt


Autor: Hinrichsen, Holger
Titel:Ein transformativer Ansatz für die Synthese und Verifikation algorithmischer Hardwarebeschreibungen
Dissertation:TU Darmstadt, Fachbereich Elektrotechnik und Informationstechnik, 2000

Die Dokumente in PDF 1.3 (mit Adobe Acrobat Reader 4.0 zu lesen):

hinrichsen.pdf (1201937 Byte)

Abstract auf Deutsch:


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.



Abstract auf Englisch:

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.


Dokument aufgenommen :2001-03-26
URL:http://elib.tu-darmstadt.de/diss/000110