Hinrichsen, Holger (2001)
Ein transformativer Ansatz für die Synthese und Verifikation algorithmischer Hardwarebeschreibungen.
Technische Universität Darmstadt
Dissertation, Erstveröffentlichung
Kurzbeschreibung (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.
| Typ des Eintrags: |
Dissertation
|
| Erschienen: |
2001 |
| Autor(en): |
Hinrichsen, Holger |
| Art des Eintrags: |
Erstveröffentlichung |
| Titel: |
Ein transformativer Ansatz für die Synthese und Verifikation algorithmischer Hardwarebeschreibungen |
| Sprache: |
Deutsch |
| Referenten: |
Eveking, Prof.Dr. H. ; Hoffmann, Dr. R.; Prof. |
| Berater: |
Eveking, Dr. H.; Prof. |
| Publikationsjahr: |
26 März 2001 |
| Ort: |
Darmstadt |
| Verlag: |
Technische Universität |
|
Datum der mündlichen Prüfung: |
4 Dezember 2000 |
| URL / URN: |
urn:nbn:de:tuda-tuprints-1108 |
| Kurzbeschreibung (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. |
|
Alternatives oder übersetztes Abstract: |
|
Alternatives Abstract | Sprache |
|---|
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. | Englisch |
|
| Freie Schlagworte: |
formale Synthese |
| Schlagworte: |
| Einzelne Schlagworte | Sprache |
|---|
| hardware synthesis, formal synthesis, formal verification | Englisch |
|
| Sachgruppe der Dewey Dezimalklassifikatin (DDC): |
600 Technik, Medizin, angewandte Wissenschaften > 620 Ingenieurwissenschaften und Maschinenbau |
| Fachbereich(e)/-gebiet(e): |
18 Fachbereich Elektrotechnik und Informationstechnik |
| Hinterlegungsdatum: |
17 Okt 2008 09:20 |
| Letzte Änderung: |
26 Aug 2018 21:24 |
| PPN: |
|
| Referenten: |
Eveking, Prof.Dr. H. ; Hoffmann, Dr. R.; Prof. |
|
Datum der mündlichen Prüfung / Verteidigung / mdl. Prüfung: |
4 Dezember 2000 |
| Schlagworte: |
| Einzelne Schlagworte | Sprache |
|---|
| hardware synthesis, formal synthesis, formal verification | Englisch |
|
| Export: |
|
| Suche nach Titel in: |
TUfind oder in Google |
 |
Frage zum Eintrag |
Optionen (nur für Redakteure)
 |
Redaktionelle Details anzeigen |
Drucken
Impressum