• search hit 1 of 1
Back to Result List

Improving the Power of Ordered Binary Decision Diagrams by Integrating Parity Nodes

Verbesserung der Berechnungskraft von geordneten Binaeren Entscheidungsdiagrammen durch Integration von Parity-Knoten

  • Hardware bugs can be extremely expensive, financially. Because microprocessors and integrated circuits have become omnipresent in our daily live and also because of their continously growing complexity, research is driven towards methods and tools that are supposed to provide higher reliability of hardware designs and their implementations. Over the last decade Ordered Binary Decision Diagrams (OBDDs) have been well proven to serve as a data structure for the representation of combinatorial or sequential circuits. Their conciseness and their efficient algorithmic properties are responsible for their huge success in formal verification. But, due to Shannon's counting argument, OBDDs can not always guarantee the concise representation of a given design. In this thesis, Parity Ordered Binary Decision Diagrams are presented, which are a true extension of OBDDs. In addition to the regular branching nodes of an OBDD, functional nodes representing a parity operation are integrated into the data structure, thus resulting in Parity-OBDDs. Parity-OBDDs are more powerful than OBDDs are, but, they are no longer a canonical representation. Besides theoretical aspects of Parity-OBDDs, algorithms for their efficient manipulation are the main focus of this thesis. Furthermore, an analysis on the factors that influence the Parity-OBDD representation size gives way for the development of heuristic algorithms for their minimization. The results of these analyses as well as the efficiency of the data structure are also supported by experiments. Finally, the algorithmic concept of Parity-OBDDs is extended to Mod-p-Decision Diagrams (Mod-p-DDs) for the representation of functions that are defined over an arbitrary finite domain.
  • n.a.

Download full text files

Export metadata

Additional Services

Share in Twitter Search Google Scholar
Metadaten
Author:Harald Sack
URN:urn:nbn:de:hbz:385-2148
Advisor:Christoph Meinel, Prof. Dr. sc.
Document Type:Doctoral Thesis
Language:English
Date of completion:2004/06/15
Publishing institution:Universit├Ąt Trier
Granting institution:Universit├Ąt Trier, Fachbereich 4
Date of final exam:2002/01/11
Release Date:2004/06/15
Tag:Formal Verification; Integrated Circuits; OBDDs; Ordered Binary Decision Diagrams; XOR Parity
GND Keyword:Algorithmus; Datenstruktur; Erweiterung; OBDD
Institutes:Fachbereich 4 / Informatik
Dewey Decimal Classification:0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme / 004 Datenverarbeitung; Informatik

$Rev: 13581 $