• search hit 13 of 19
Back to Result List

High-level Methods for OBDD-based Sequential Verification

High-level Methoden für die OBDD-basierte sequentielle Verifikation

  • 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.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Author:Christian Stangier
Advisor:Christoph Meinel
Document Type:Doctoral Thesis
Date of completion:2004/06/15
Publishing institution:Universität Trier
Granting institution:Universität Trier, Fachbereich 4
Date of final exam:2002/11/29
Release Date:2004/06/15
Tag:OBDDs; formal verification; partitioning; reordering
GND Keyword:Logischer Entwurf; OBDD; Transitionssystem; Verifikation
Institutes:Fachbereich 4 / Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik

$Rev: 13581 $