Formale Spezifikation und Synthese digitaler Schaltungen auf höheren Abstraktionsebenen

Christian Blumenröhr

ISBN 978-3-89722-360-8
204 Seiten, Erscheinungsjahr: 2000
Preis: 40.50 €
Formale Spezifikation und Synthese digitaler Schaltungen auf höheren Abstraktionsebenen

Das Problem, eine abstrakte Schaltungsbeschreibung in eine konkrete Hardwareimplementierung umzusetzen, wirft zwei grundlegende und zueinander orthogonale Fragestellungen auf:

1.Korrektheit: Realisiert die Hardwareimplementierung den vorgegebenen funktionalen Zusammenhang in der Weise, wie er in der Spezifikation beschrieben wurde?

2.Kosten: Wie kann die Synthese durchgeführt werden, sodass die physikalischen Eigenschaften der resultierenden Implementierung wie Flächenbedarf, Zeitverhalten, etc. bezüglich einer vorgegebenen Kostenfunktion optimiert werden?

In der konventionellen Synthese kann eine Optimierung der Kosten erreicht werden, eine explizite Gewährleistung der Korrektheit der Hardwareimplementierung findet während des Syntheseprozesses aber nicht statt. Es werden zwar in manchen Ansätzen auf dem Papier Korrektheitsbeweise für die zugrunde liegenden Transformationen erbracht, es wird dann aber stillschweigend davon ausgegangen, dass die Softwareimplementierung des Syntheseprogramms, das diese Transformationen realisiert, fehlerfrei ist. Vielmehr wird nach der Synthese eine Simulation oder formale Verifikation nachgeschaltet, was einen erheblichen Aufwand mit sich bringt, bzw. meist gar nicht vollständig möglich ist.

In Anbetracht dieser Situation wurde in dieser Arbeit eine andere Methode entwickelt, um zu erwiesenermaßen korrekten Syntheseergebnissen zu kommen. Statt die Synthese in konventioneller Weise durchzuführen und eine Simulation oder Verifikation nachzuschalten, wird das Syntheseergebnis innerhalb des Logikkalküls eines Theorembeweisers durch Anwendung elementarer mathematischer Regeln abgeleitet. Dieser Synthesevorgang wird mit dem Begriff "Formale Schaltungssynthese" bezeichnet.

Im Bereich der Formalen Schaltungssynthese existieren bislang lediglich Arbeiten für eine Synthese auf unteren Abstraktionsebenen (RT- und Gatterebene) sowie für reine Datenpfade auf algorithmischer Ebene. In dieser Arbeit wurde ein Verfahren für die Synthese allgemeiner berechenbarer Funktionen auf algorithmischer Ebene und für eine Synthese auf Systemebene entwickelt. Auf algorithmischer Ebene werden Einprozessbeschreibungen behandelt, während auf Systemebene Strukturen nebenläufiger Prozesse betrachtet werden. Die Schaltungssynthese basiert auf einer neuentwickelten funktionalen Hardwarebeschreibungssprache namens Gropius. Im Gegensatz zu herkömmlichen Hardwarebeschreibungssprachen wie etwa VHDL hat Gropius eine mathematisch exakte Semantik, da alle Konstrukte in der Prädikatenlogik höherer Ordnung definiert wurden.

Im Verlaufe der Synthese wird eine Eingangsschaltungsbeschreibung durch Instantiierung vorbewiesener Theoreme in eine transformierte Beschreibung überführt. Die Tatsache, dass die Transformation im Theorembeweiser stattfindet, garantiert die Korrektheit des Syntheseschritts. Die Entscheidung, welche Transformationstheoreme wann und an welcher Stelle eingesetzt werden sollen, ist wesentlich für die Implementierungskosten des Syntheseergebnisses. Sie kann einerseits interaktiv getroffen werden, andererseits ist es aber auch möglich, eine automatische Entwurfsraumuntersuchung außerhalb des Theorembeweisers durchzuführen, aufgrund deren Ergebnis die Transformation im Theorembeweiser dann ebenfalls automatisch ausgeführt wird. Als Methoden für eine Entwurfsraumuntersuchung können dabei Verfahren der konventionellen Hardware-Synthese eingesetzt werden.

Aufgrund dieser strikten Trennung zwischen Entwurfsraumuntersuchung und Transformation wird es möglich, nicht nur zu garantiert korrekten, sondern auch zu kostengünstigen Hardwareimplementierungen zu gelangen. Da die Formale Schaltungssynthese die Korrektheit konstruktiv ableitet und nicht wie die Verifikationsverfahren im nachhinein überprüft, ist der zeitliche Mehraufwand für eine Formale Synthese gegenüber einer konventionellen Synthese geringer als der für eine nachträgliche Verifikation oder Simulation. Experimentelle Ergebnisse zeigen, dass insbesondere im Hinblick auf komplexere Entwurfsraumuntersuchungsmethoden der zusätzliche Aufwand für die formale Ableitung im Theorembeweiser keinen entscheidenden Performanzfaktor darstellt.