TUD Technische Universität Darmstadt
Hessische Landes-und Hochschulbibliothek
HLuHB

EPDA - Elektronische Publikationen Darmstadt


Autor: Ritter, Gerd
Titel:Formal Sequential Equivalence Checking of Digital Systems by Symbolic Simulation
Dissertation:TU Darmstadt, Fachbereich Elektrotechnik und Informationstechnik, 2001

Die Dokumente in PDF 1.3 (mit Adobe Acrobat Reader 4.0 zu lesen):

thesis.pdf (1302681 Byte)

Abstract auf Deutsch:


Ein neuer Ansatz zur sequentiellen Verifikation von Entwürfen auf verschiedenen Abstraktionsebenen durch symbolische Simulation wird vorgestellt. Das automatische formale Verifikationswerkzeug wurde dazu verwendet, die Äquivalenz von strukturellen Beschreibungen auf Registertransferebene und den entsprechenden Verhaltensspezifikationen nachzuweisen. Die Ergebnisse eines kommerziellen Synthesewerkzeugs auf Gatterebene konnten mit Verhaltens- bzw. Strukturbeschreibungen auf Registertransferebene verglichen werden. Es ist nicht erforderlich, daß die Spezifikation synthetisierbar oder taktäquivalent zur Implementierung ist. Ferner wird eine Anwendungsmöglichkeit der Methode zur Eigenschaftsverifikation vorgeschlagen.

Die symbolische Simulation wird entlang logisch konsistenter Pfade in den Beschreibungen durchgeführt. Eine erweiterbare Bibliothek verschiedener Techniken zur Äquivalenzerkennung erlaubt es, einen günstigen Kompromiß zwischen Genauigkeit und Geschwindigkeit zu erzielen. Auf Entscheidungsdiagrammen (OBDD) basierende Methoden erkennen seltene Fälle der Äquivalenz symbolischer Terme. Durch Einbeziehung der Resultate der anderen Techniken zur Äquivalenzerkennung gelingt es, die Größe der Graphen zu kontrollieren. Außerdem bilden die Entscheidungsdiagramme lediglich kleine Ausschnitte des Verifikationsproblems ab. Die Kooperation aller Techniken und eine effiziente Unterstützung der Fehleranalyse werden ermöglicht, indem Erkenntnisse über Termbeziehungen an Äquivalenzklassen vermerkt werden, anstatt die symbolischen Terme selbst zu manipulieren.




Abstract auf Englisch:

A new approach to sequential verification of designs at different levels of abstraction by symbolic simulation is proposed. The automatic formal verification tool has been used for equivalence checking of structural descriptions at rt-level and their corresponding behavioral specifications. Gate-level results of a commercial synthesis tool have been compared to specifications at behavioral or structural rt-level. The specification need not be synthesizable nor cycle equivalent to the implementation. In addition, a future application of the method to property verification is proposed.

Symbolic simulation is guided along logically consistent paths in the two descriptions to be compared. An open library of different equivalence detection techniques is used in order to find a good compromise between accuracy and speed. Decision diagram (OBDD) based techniques detect corner-cases of equivalence. Graph explosion is avoided by using the results of the other equivalence detection techniques and by representing only small parts of the verification problem by decision diagrams. The cooperation of all techniques as well as good debugging support are made feasible by notifying detected relationships at equivalence classes instead of manipulating symbolic terms.



Abstract auf Französisch:

Nous proposons une nouvelle méthodologie de simulation symbolique, permettant la vérification des circuits séquentiels décrits à des niveaux d'abstraction différents. Nous avons utilisé un outil automatique de vérification formelle afin de montrer l'équivalence entre une description structurelle précisant les détails de réalisation et sa spécification comportementale. Des descriptions au niveau portes logiques issues d'un outil de synthèse commercial ont été comparées à des spécifications comportementales et structurelles au niveau transfert de registres. Cependant, il n'est pas nécessaire que la spécification soit synthétisable ni qu'elle soit équivalente à la réalisation à chaque cycle d'horloge. Ultérieurement cette méthode pourra aussi s'appliquer à la vérification des propriétés.

La simulation symbolique est exécutée en suivant des chemins dont l'outil garantit la cohérence logique. Nous obtenons un bon compromis entre précision et vitesse en détectant des équivalences grâce à un ensemble extensible de techniques. Nous utilisons des diagrammes de décisions binaires (OBDD) pour détecter les équivalences dans certains cas particuliers. Nous évitons l'explosion combinatoire en utilisant les résultats des autres techniques de détection et en ne représentant qu'une petite partie du problème à vérifier par des diagrammes de décisions. La coopération de toutes les techniques, et la génération de traces permettant la correction d'erreurs, ont été rendues possibles par le fait que nous associons des relations à des classes d'équivalence, au lieu de manipuler des expressions symboliques.



Dokument aufgenommen :2001-03-30
URL:http://elib.tu-darmstadt.de/diss/000113