Abstract:

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.

Table of contents:

1. Introduction
   1.1 Motivation
   1.2 Verification of Digital Systems
   1.3 Scope of the Thesis
   1.4 Overview of the Thesis
   1.5 Publications
   

2. Preliminaries
   2.1 Ordered Binary Decision Diagrams
     2.1.1 Definitions and Properties
     2.1.2 Implementation Techniques
     2.1.3 Minimization of OBDDs

3. Extensions of OBDDs
   3.1 OBDDs - an Ideal Data Structure?
   3.2 Extensions of OBDDs
     3.2.1 Free BDDs and Read-k Decision Diagrams
     3.2.2 Functional Decision Diagrams
     3.2.3 Binary Decision Diagrams with Operator Nodes
   

4. Parity-OBDDs
   4.1 Definition
   4.2 Properties of Parity-OBDDs
   4.3 Reduction of Parity-OBDDs
   4.4 Equivalence Test
     4.4.1 Deterministic Equivalence Test
     4.4.2 Probabilistic Equivalence Test for Boolean Functions
     4.4.3 Applying the Probabilistic Equivalence Test to Parity-OBDDs
     4.4.4 Determining the Error Probability
     4.4.3 Implementation of the Probabilistic Equivalence Test
   4.5 Synthesis of Parity-OBDDs   4.5.1 Cofactor Creation
     4.5.2 The Standard Apply Algorithm
     4.5.3 The ITE+ Algorithm
     4.5.4 Extending the Synthesis Algorithm
   

5. Minimization of Parity-OBDDs
   5.1 Parity-Node Frequency
     5.1.1 Prerequisites
     5.1.2 Experimental Setup
     5.1.3 Experimental Results
   5.2 Parity-Node Placement
     5.2.1 A Simple Parity-Node Placement Heuristic
     5.2.2 Using Linear Combinations
     5.2.3 Dynamic Parity-Node Placement
     5.2.4 Meta-Parity.Nodes
     5.2.5 Jiggling - A Simple Heuristic for Parity-Node Placement
     5.2.6 Applications of Dynamic Parity-Node Placement
   5.3 Dynamically Changing the Variable Order
     5.3.1 Adapting OBDD Minimizaion Heuristics
     5.3.2 The Swap-In-Place Algorithm
     5.3.3 Adapted Sifting - A Heuristic for Parity-OBDD Minimization
     5.3.4 Conclusion
   

6. Extension of Parity-OBDDs to the Discrete Domain
   6.1 Multiple Valued Decision Diagrams
   6.2 Mod-P-Decision Diagrams
   6.3 Probabilistic Equivalence Test
     6.3.1 Definition and Properties of the Generalized A-Transform
     6.3.2 Efficient Computation of the A-Teransform
     6.3.3 Probabilistic Equivalence Test for Mod-P DDs
   6.4 Synthesis of Mod-P-DDs
     6.4.1 Cofactor Creation for Mod-P-DDs
     6.4.2 Extended Case+ Algorithm for Mod-P-DDs
   

7. Conclusions
   7.1 Key Results
   7.2 Possible Future Work

8. Experimental Results