Verifikation von Arithmetik-Schaltungen mit Word-Level Decision Diagrams

| Beteiligte Mitarbeiter | Kooperationspartner | Projektbeschreibung | Publikationen |

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 exponentielle Größe hat.

Um diesem Problem zu begegnen, wurden sogenannte Word-level DDs wie z.B. *BMDs, HDDs oder K*BMDs eingeführt, die z.B. Multiplizierer in polynomieller Größe darstellen können. Word-level DDs stellen im Gegensatz zu BDDs Funktionen mit ganzzahligem (oder rationalem) Wertebereich dar. Die Frage, ob auch Dividierer in polynomiellem Platz mit Word-level DDs darstellbar sind, war über längere Zeit offen und konnte im Rahmen dieses Projektes beantwortet werden.

Nachdem es sich herausgestellt hatte, daß bestimmte Word-level DDs zur Verifikation von Multiplizierern hervorragend geeignet sind, da es möglich ist, für die Multipliziererfunktion diese Word-level DDs mit polynomiellem Platz und in polynomieller Zeit zu konstruieren, wurde die Betrachtung auf Dividierer ausgeweitet. Hierbei konnte die schon längere Zeit offene Frage, ob auch Dividierer in polynomiellem Platz mit Word-level DDs darstellbar sind, beantwortet werden. Mit Methoden der linearen Algebra wurde eine exponentielle untere Schranke für die Darstellungsgröße von Word-level DDs für die Divisionsfunktion angegeben. Der Beweis beruht auf der Konstruktion eines "generischen" Word-level DDs, für das die Schranke gezeigt wird und das weiterhin die Einbettung aller gängigen Word-level DD-Typen erlaubt. Im Gegensatz zu sonst üblichen Techniken bei DDs wurde hier der Beweis direkt für eine ganze Klasse von DDs geführt.

Erste weiterführende Untersuchungen lassen jedoch erhoffen, daß es dennoch möglich ist, Dividierer unter Zuhilfenahme von Word-level DDs zu verifizieren. Der von uns beabsichtigte Ansatz versucht, anstatt der Divisionsfunktion selbst eine transformierte Funktion zu verifizieren. Die Transformation ergibt sich durch einen Zusatzschaltkreis, der hinter den Dividierer gesetzt wird und die Division durch Multiplikation mit dem Divisor und Addition des Divisionsrestes rückgängig macht. Man überlegt sich, daß der Dividierer korrekt ist, genau dann, wenn der Gesamtschaltkreis die Identität berechnet. Man beginnt nun die Berechnung des Word-level DDs für den Gesamtschaltkreis zunächst durch den (einfachen) Aufbau des Word-level DDs für den Zusatzschaltkreis. Kommt man dann zu dem Teil des Schaltkreises, der zum eigentlichen Dividierer korrespondiert, so arbeitet man auf einer Darstellung, die es nicht erfordert den Dividierer selbst durch Rückwärtseinsetzen aufzubauen, sondern eine durch den Zusatzschaltkreis gegebene Transformation. Es ist Gegenstand momentaner Untersuchungen, ob diese Transformation (und in welchen Fällen sie) zu einer polynomiell beschränkten Darstellung führt. Es sollen für verschiedene gebräuchliche Dividiererentwürfe - u.a. den Pentium-Dividierer - Betrachtungen durchgeführt werden. Ziel ist ein Verfahren, das im Gegensatz zu bisher bekannten Methoden eine vollautomatische Verifikation durchführt, ohne interaktiv auf Wissen des Entwicklers über die vorliegende Realisierung zurückgreifen zu müssen.