Rechnergestützter Entwurf von Prozessoren auf der Register-Transfer-Ebene

Register-Transfer-Synthese

Unter Register-Transfer-Synthese versteht man die Übersetzung eines vom zu entwerfenden Spezialprozessor zu bearbeitenden parallelen Algorithmus in eine maßgeschneiderte Register-Transfer-Struktur, die den vorgegebenen Algorithmus mit einer beschränkten Anzahl von Wertespeichern (Registern), Berechnungs- und Transfereinheiten besonders effizient ausführen kann. In den vergangenen Jahren ist weltweit sehr viel Forschungsarbeit geleistet worden, um diesen Vorgang zumindest teilweise zu automatisieren. Mehrere Entwurfssysteme sind zwischenzeitlich entwickelt worden, die sich hinsichtlich des vorgesehenen Anwendungsgebietes, hinsichtlich der Zerlegung in Teilprobleme bzw. der Reihenfolge, in der diese Teilprobleme bearbeitet werden und schließlich in den verwendeten Entwurfsalgorithmen unterscheiden. Das wesentliche Ziel ist die Optimierung eines auf Chipfläche und Performanz beruhenden Qualitätsmaßes. Register-Transfer-Synthese-Systeme verwenden unterschiedliche Modelle für die Vielzahl von Randbedingungen, die bei einem praktischen Entwurf zu berücksichtigen sind, sie setzen die Korrektheit der Verhaltensbeschreibung der zu verwendenden RT-Module voraus und benutzen eine Vielzahl von komplexen Algorithmen zur Optimierung des oben genannten Qualitätsmaßes. Es ist daher fraglich, ob das Entwurfsergebnis in allen Fällen tatsächlich eine Realisierung des vorgegebenen Systemverhaltens darstellt. Entwurfskorrektheit ist daher ein zweites, fast noch wesentlicheres Qualitätsmaß, das bei bisherigen Systemen aber nur unzureichend berücksichtigt wurde.

In unserem System führen wir formale Modellierungen ein, die eine Überprüfung von Entwurfsschritten auf Korrektheit erlauben und entwickeln Entwurfsalgorithmen für bisher ungelöste Teilprobleme.

Systemübersicht

Abb. 2.4 zeigt eine Übersicht über die einzelnen Systemmodule. Dabei handelt es sich um ein Experimentiersystem, bei dem verschiedene Sprachen und Theorien eingesetzt werden, die teilweise nur intern benutzt werden und daher für den Benutzer nicht in Erscheinung treten. Benutzersprachen sind die Hardwarebeschreibungssprache VHDL, Zeitdiagramme, Blockdiagramme und derzeit noch eine spezielle für die Verifikation entwickelte Sprache VIOLA mit formaler, in Higher Order Logik definierter Semantik. Eine Ersetzung durch VHDL ist geplant. Für Programmgraphen gibt es außerdem eine graphische Ausgabe, um die einzelnen Entwurfsschritte anhand von transformierten Programmgraphen zu verdeutlichen.

Die wesentlichen eigenen Forschungsergebnisse fließen in die Interfacesynthese, die Datenpfadsynthese und den Modulverifizierer.

Zielarchitektur

Der Entwurf von Hardwareprozessoren gliedert sich in mehrere Teilaufgaben. Diese leiten sich aus der heutzutage üblichen Modellierung eines Hardwaresystems als Komposition kommunizierender Prozessoren ab. Entsprechend ist ein Prozessor in eine Verarbeitungseinheit und eine Kommunikationseinheit zu unterteilen. Die Verarbeitungseinheit wiederum zerfällt in Datenpfad und Controller.

Diese Unterteilung macht Sinn, weil nicht nur die zweckmäßigste Art der Verhaltensbeschreibung sondern auch der gesamte Entwurfsprozeß für Kommunikationseinheiten und Verarbeitungseinheiten unterschiedlich sein sollte. Kommunikationseinheiten interagieren laufend mit ihrer Umgebung und beschaffen sich dabei Aufträge, Anfangswerte zur Bearbeitung der Aufträge und liefern die vom Verarbeitungsprozessor erzeugten Ergebnisse an die Umgebung zurück. Hierbei sind quantitative Zeitbedingungen zu beachten.

Kommunikationseinheiten sind gekennzeichnet durch einen eingeschränkten Datenpfad und einen dominanten Controllerteil, der in der Regel ebenfalls taktsynchron arbeiten wird, in besonders zeitkritischen Anwendungen aber auch self-timed Systeme enthalten kann. Der Controller kann als Einheit oder auch als Komposition kommunizierender Teilsysteme entworfen werden.

Zur Bewältigung dieser Entwurfsaufgabe gibt es heutzutage nur wenige CAD-Systeme.

Verabeitungseinheiten verknüpfen die ihnen als Anfangswert übermittelten Daten in verschiedenster Weise. Ihre Interaktion mit der Umgebung über den Kommunikationsprozessor erfolgt nur zu Beginn und am Ende des Verarbeitungsauftrags. Dies ist die typische Situation wie sie von fast allen Register-Transfer- Synthese-Systemen angenommen wird.

Derzeit entsprechen auch die unterstützten Hardware-Grundstrukturen denjenigen, die in allen Register- Transfer-Synthese-Systemen verwendet werden. Der Datenpfad ist also multiplexer- oder busorientiert, wobei die Kommunikationspfade bedarfsorientiert gelegt werden und nicht in ihrer Grundstruktur vorgegeben werden. Auch der zugehörige Controller wird derzeit als Ganzes entworfen. Der gewählte Ansatz der Formalisierung auf der Basis von Prozeßalgebren erlaubt allerdings auch, den Controller als Komposition von interagierenden Controllern zu implementieren und die Korrektheit dieses Systems von Controllern nachzuweisen.

Die erlaubten Strukturelemente (Module) der Hardwarearchitektur sind in einer Modulbasis auf unterschiedlichen Abstraktionsebenen beschrieben.

VERENA: Modulverifikation

Da Module auf unterschiedlichen Abstraktionsebenen beschrieben werden, stellt sich das Problem der Beschreibungskonsistenz. Der Modulverifizierer VERENA kann die ErfŸüllung einer VIOLA Spezifikation und einer VIOLA Implementierungsbeschreibung auf der Logikebene durch Transformationen auf VIOLA Termen automatisch nachweisen. Abb. 2.5 zeigt als typisches Beispiel einer Verifikationsaufgabe die Implementierung einer multifunktionalen Pipeline auf der Logikebene und die Spezifikation.

Durch folgende Strategie soll der Umgang mit unserem Verifikationssystem VERENA praktikabel werden:

1. Der zugrundegelegte Formalismus wird vor dem Entwerfer verborgen. Der Entwerfer spezifiziert Verhalten und Implementierung in einer Hardwarebeschreibungssprache VIOLA (geplant: subset von VHDL) und wählt Beweisstrategien aus.

2. Beweise der Äquivalenz zwischen Verhalten und Implementierung erfolgen automatisch auf der Ebene von VIOLA durch Anwendung von Transformationsregeln. Im Falle der Nichtäquivalenz werden Gegenbeispiele ausgegeben.

3. Die Korrektheit der Vorgehensweise des bisher implementierten Systems liegt in der Verantwortung des Systementwicklers. Er hat hierzu die formale Semantik von VIOLA auf der Basis der Logik höherer Ordnung definiert und die VIOLA Transformationsregeln unter Verwendung des HOL-Systems verifiziert.

4. Das System ist offen sowohl bezüglich einer Spracherweiterung als auch bezüglich der Transformationsregeln und der Methode zu deren Anwendung. Die Korrektheit bezüglich eines formalen Modells liegt dann in der Verantwortung eines Systembetreuers. Er benötigt Erfahrung im Umgang mit der Beweismethodik.

Das Verfahren kann auf unterschiedliche Schaltungstypen angewendet werden. Für jeden Schaltungstyp führt das Verfahren den Nachweis der Korrektheit bzw. die Ableitung von Gegenbeispielen automatisch durch. Der automatische Nachweis der Korrektheit der Pipelinestufe aus Abb. 2.5 erfolgt beispielsweise in 4 Minuten. Dabei müssen graphische Darstellungen von Logikfunktionen mit ca. 1,5 Millionen Knoten bearbeitet werden.

SUSAN: Datenpfadsynthese

VHDL-Programme werden intern in einen Datenflußgraphen gewandelt. Er repräsentiert alle zulässigen Reihenfolgen, in denen die Anweisungen ausgeführt werden können. Die Aufgabe des Schedulings ist es, eine erlaubte Ausführungsreihenfolge zu wählen, so daß Beschränkungen hinsichtlich der Ausführungszeit und des Ressourceneinsatzes erfüllt werden.

Eine elegante Formulierung des Schedulingproblems basiert auf einem ILP- Modell. Es erlaubt vielfältige Nebenbedingungen zu modellieren, wie beispielsweise die Ausführung mehrerer Operationen in einem Verarbeitungsschritt, die Verwendung von Operationen, die mehr als einen Verarbeitungsschritt benötigen, die Berücksichtigung von funktionaler Fließbandverarbeitung, das Falten von Schleifen und Verzweigungen im Datenflußgraph.

Der ursprüngliche Ansatz benötigte allerdings lange Bearbeitungszeiten, die nun durch verschiedene Maßnahmen drastisch reduziert werden konnten, so daß die Größenordnungen heuristischer Verfahren für dieses exakte Optimierungsverfahren erreicht wurden. Darüberhinaus konnten weitere praktisch wichtige Randbedingungen modelliert werden, nämlich der Einsatz multifunktionaler Verarbeitungseinheiten und die Betrachtung unterschiedlicher Verarbeitungszeiten für einen Typ von Operationen.

Aufgrund der Erfolge mit dem ILP-Ansatz für das Scheduling soll nun ein entsprechender Ansatz für die Lösung des Allokationsproblems erstellt und untersucht werden.

SABINA: Interfacesynthese

Die Synthese von Kommunikationseinheiten beginnt mit einer aus Impulsdiagrammen abgeleiteten prozeßalgebraischen Spezifikation in T-LOTOS (einer Erweiterung der standardisierten formalen Beschreibungstechnik LOTOS), die sowohl Wertübergabe als auch quantitative Zeitbehandlung erlaubt.

Die zentrale Aufgabe besteht nun in der Unterstützung eines interaktiven Entwurfsvorgangs, in dem die Schaltung Stück für Stück aus Modulen zusammengesetzt wird. Beispielsweise kann der Anwender Berechnungseinheiten, Zeitgeber, Zähler u.ä. als Komponenten des zu entwerfenden Systems auswählen. Das System begleitet den Entwurfsprozeß durch

1. Überprüfung, ob das jeweils erzeugte Teilsystem wirklich ein Teil des gültigen Gesamtsystems sein kann;

2. automatische Erzeugung einer Spezifikation des jeweiligen Rest-Teilsystems , das benötigt wird, um das vom Anwender bereits entworfene Teilsystem zu einem gültigen Gesamtsystem zu ergänzen;

3. automatische Umsetzung der Spezifikation eines Rest-Teilsystems in einen endlichen Automaten.

Diese Systemleistungen arbeiten ausschließlich auf D T-LOTOS-Darstellungen. In Zusammenarbeit mit der Universität Madrid entsteht im Rahmen des ESPRIT-Projektes FORMAT auch eine Übersetzung von LOTOS- Darstellungen in VHDL. Hierdurch wird ein durchgängiger Entwurfsfluß von Zeitdiagrammen zu VHDL gewährleistet.