|
Eingang zum Volltext in OPUS
Hinweis zum Urheberrecht
Dissertation zugänglich unter
URN: urn:nbn:de:hbz:385-2263
URL: http://ubt.opus.hbz-nrw.de/volltexte/2004/226/
High-level Methods for OBDD-based Sequential Verification
High-level Methoden für die OBDD-basierte sequentielle Verifikation
Stangier, Christian
 
| SWD-Schlagwörter: |
| Logischer Entwurf , Transitionssystem , Verifikation , OBDD |
| Freie Schlagwörter (Englisch): |
| formal verification , OBDDs , partitioning , reordering |
| Institut: |
| Informatik |
| Fakultät: |
| Fachbereich 4 |
| DDC-Sachgruppe: |
| Informatik |
| Dokumentart: |
| Dissertation |
| Hauptberichter: |
| Meinel, Christoph, Prof. Dr. |
| Sprache: |
| Englisch |
| Tag der mündlichen Prüfung: |
| 29.11.2002 |
| Erstellungsjahr: |
| 2002 |
| Publikationsdatum: |
| 15.06.2004 |
| Kurzfassung auf Englisch: |
| Today, usage of complex circuit designs in computers,
in multimedia applications and communication devices
is widespread and still increasing.
At the same time, due to Moore's Law we do not
expect to see an end in the growth of the complexity
of digital circuits.
The decreasing ability of common validation techniques
-- like simulation -- to assure correctness of a circuit design
enlarges the need for formal verification techniques.
Formal verification delivers a mathematical proof that
a given implementation of a design fulfills its specification.
One of the basic and during the last years widely used
data structure in formal verification are the so called
Ordered Binary Decision Diagrams (OBDDs)
introduced by R. Bryant in 1986.
The topic of this thesis is integration of structural
high-level information in the OBDD-based formal verification
of sequential systems.
This work consist of three major parts, covering different layers
of formal verification applications:
At the application layer, an assertion checking methodology,
integrated in the verification flow of the high-level design and
verification tool Protocol Compiler is presented.
At the algorithmic layer, new approaches for partitioning of
transition relations of complex finite state machines, that significantly
improve the performance of OBDD-based sequential verification are
introduced.
Finally, at the data structure level, dynamic variable reordering
techniques that drastically reduce the time required for reordering
without a trade-off in OBDD-size are described.
Overall, this work demonstrates how a tighter integration of applications
by using structural information can significantly improve the efficiency
of formal verification
applications in an industrial setting. |
| Kurzfassung auf Deutsch: |
| n.a. |
Home |
Suchen |
Veröffentlichen |
Hilfe |
Viewer
|
