TU Darmstadt / ULB / tuprints

Formal Sequential Equivalence Checking of Digital Systems by Symbolic Simulation

Ritter, Gerd :
Formal Sequential Equivalence Checking of Digital Systems by Symbolic Simulation.
[Online-Edition]
TU Darmstadt
[Ph.D. Thesis], (2001)

[img]
Preview
PDF
thesis.pdf
Available under Simple publication rights for ULB.

Download (1272Kb) | Preview
Item Type: Ph.D. Thesis
Title: Formal Sequential Equivalence Checking of Digital Systems by Symbolic Simulation
Language: English
Abstract:

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.

Alternative Abstract:
Alternative AbstractLanguage
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.German
Uncontrolled Keywords: formale Verifikation, symbolische Simulation, Äquivalenzprüfung, sequentielle Verifikation, Hardwareverifikation, Gatterebene, Registertransferebene
Alternative keywords:
Alternative keywordsLanguage
formale Verifikation, symbolische Simulation, Äquivalenzprüfung, sequentielle Verifikation, Hardwareverifikation, Gatterebene, RegistertransferebeneEnglish
Classification DDC: 600 Technik, Medizin, angewandte Wissenschaften > 620 Ingenieurwissenschaften
Divisions: Fachbereich Elektrotechnik und Informationstechnik
Date Deposited: 17 Oct 2008 09:20
Last Modified: 07 Dec 2012 11:46
Official URL: http://elib.tu-darmstadt.de/diss/000113
URN: urn:nbn:de:tuda-tuprints-1131
License: Simple publication rights for ULB
Referees: Glesner, Prof. Manfred and Bakowski, Prof. Przemyslaw
Advisors: Eveking, Prof. Hans and Borrione, Prof. Dominique
Refereed: 26 March 2001
URI: http://tuprints.ulb.tu-darmstadt.de/id/eprint/113
Export:

Actions (login required)

View Item View Item