Funktionale Simulation
| Beteiligte Mitarbeiter
| Kooperationspartner
| Projektbeschreibung | Publikationen
|
Lehrstuhl für Rechnerarchitektur | |
Christoph Scholl, Prof. Dr. | |
| |
Lehrstuhl für Rechnerarchitektur | |
Andreas Brogle | |
Thomas Weis | |
Achim Brucker |
Die Aufgabe der Hardwareverifikation besteht darin, zu beweisen, daß eine gegebene Schaltungsimplementierung auch wirklich mit der Schaltungsspezifikation übereinstimmt. Eine populäre Methode zum Beweis, daß eine kombinatorische Schaltung ihrer Spezifikation entspricht, besteht darin, sowohl Spezifikation als auch Implementierung in eine Normalform zu überführen und diese dann auf Gleichheit zu testen.
Für bestimmte Schaltungsklassen wie z.B. Kontrollogik oder Addierer haben sich hierbei Binary Decision Diagrams (BDDs) als kompakte Normalform bewährt. Bei anderen Schaltungen wie z.B. Multiplizierern scheitert der BDD-basierte Ansatz jedoch, da die Darstellung von Multiplizierern mit BDDs immer exponentielle Größe hat.
Bei sequentiellen Schaltungen wird der Beweis der Äquivalenz von Spezifikation und Implementierung vielfach ebenfalls mit BDD-basierten Methoden geführt. Ist die sequentielle Schaltung allerdings zu groß, um mit den aktuellen automatischen Verifikationsmethoden behandelt zu werden, muß man sich in der Praxis nach wie vor mit Simulationen begnügen, die helfen können, Entwurfsfehler zu finden und so wenigstens eine gewisse Sicherheit liefern können, daß beim Entwurf keine Fehler unterlaufen sind. Im Projekt &laqou;Funktionale Simulation» wird an einem Verfahren gearbeitet, das die Simulation beschleunigt und so dazu beträgt, daß in einer vorgegebenen Zeit mehr Simulationsmuster getestet werden können.
Zyklus-basierte Funktionale Simulation wird zur Validierung sehr großer sequentieller Schaltungen eingesetzt. Zur Beschleunigung der Funktionalen Simulation wurden Entscheidungsdiagramme eingesetzt, um die Laufzeit für einen Simulationszyklus (die bei Event-gesteuerter Simulation oder bei Compiler-basierter Simulation im worst case proportional zu der Anzahl der Logikgatter in der Schaltung ist) zu reduzieren zu einer Laufzeit, die lediglich proportional ist zur Anzahl der Ein- und Ausgägen der Schaltung.
Dieser Vorteil wird jedoch zunichte gemacht, wenn die verwendeten Entscheidungsdiagramme und damit die Simulationsprogramme sehr groß werden, so daß Zugriffe des Programms auf den Speicher aufgrund der Speicherhierarchie langsam werden. Aus diesem Grund ist es ein zentrales Problem, den benötigten Speicher zu begrenzen.
Unser Ansatz besteht darin, große Simulationsprogramme durch spezielle Optimierungstechniken zu vermeiden, die die Entscheidungsdiagramme minimieren und zusätzlich noch die mittlere Anzahl von Operationen zur Auswertung eines Eingabevektors berücksichtigen.
Christoph Scholl, Prof. Dr., Rolf Drechsler, Prof. Dr., Bernd Becker, Prof. Dr. Functional Simulation using Binary Decision Diagrams Int'l Conf. on CAD, 1997 |