Skip to main content
main-content

Über dieses Buch

One of the main problems in chip design is the huge number of possible combinations of individual chip elements, leading to a combinatorial explosion as chips become more complex. New key results in theoretical computer science and in the design of data structures and efficient algorithms, can be applied fruitfully here. The application of ordered binary decision diagrams (OBDDs) has led to dramatic performance improvements in many computer-aided design projects. This textbook provides an introduction to the foundations of this interdisciplinary research area with an emphasis on applications in computer-aided circuit design and formal verification.

Inhaltsverzeichnis

Frontmatter

Introduction

1. Introduction

Abstract
A wide variety of problems in discrete mathematics, computer science, or the design of integrated circuits involve the task of manipulating objects over finite domains. The dependencies and relations among the objects are modeled by means of discrete functions. By introducing a binary encoding for the elements of the underlying domain, each finite problem can be fully expressed by means of switching functions, i.e., functions mapping bit vectors to single bits. Consequently, manipulations over finite domains can be entirely reduced to the treatment of switching functions.
Christoph Meinel, Thorsten Theobald

Basics

2. Basics

Abstract
Propositional logic. The theme of propositional calculus is to investigate simple logical connections among elementary statements. Such elementary statements are for example
  • “Paris is the capital of France.”
  • “6 is a prime number.”
Christoph Meinel, Thorsten Theobald

Data Structures for Switching Functions

Frontmatter

3. Boolean Functions

Abstract
The basic components of computers and other digital systems are circuits. Circuits consist of wires connecting one or several voltage input ports with one or several output ports. The simplified model for describing the relation between input and output voltage merely starts from two well-distinguished signals: either there is a voltage, indicated by the value 1, or there is none, indicated by the value 0. Of course, in a technical realization, there will be deviations from these nominal values. However, as long as these deviations do not exceed certain limits, they do not affect the basic functionality of the circuit. Hence, in fact, the statement that a signal is two-valued or binary simply means that the value of this signal is within one of two non-overlapping continuous ranges.
Christoph Meinel, Thorsten Theobald

4. Classical Representations

Abstract
To be able to work with concrete switching functions, a description of these functions is required. Of course, there is a very broad spectrum of possible description types. Basically, the representation has to describe the function adequately and thoroughly, i.e., it must be completely clear from the representation which switching function is considered. Besides this fundamental condition, which has always to be satisfied, a series of further properties are desirable. For example, the description of a function should
  • be rather short and efficient
  • support the evaluation and manipulation of the function
  • make particular properties of the function visible
  • suggest ideas for a technical realization
and much more.
Christoph Meinel, Thorsten Theobald

5. Requirements on Data Structures in Formal Circuit Verification

Abstract
In the previous chapter, we have introduced several representation types for switching functions. In particular, we have described the switching functions under consideration based on the following ideas:
  • by systematically tabulating the function values (e.g., truth tables)
  • by providing a method for computing the function (e.g., disjunctive or conjunctive normal forms, Boolean formulas or circuits)
  • by describing a scheme for evaluating the function (e.g., decision trees, branching programs).
Christoph Meinel, Thorsten Theobald

OBDDs: An Efficient Data Structure

Frontmatter

6. OBDDs — Ordered Binary Decision Diagrams

Abstract
In this chapter, we introduce the representation type of ordered binary decision diagrams, called OBDDs for short. Although the underlying model of decision diagrams (or synonymously branching programs) was already studied by Lee and Akers in the 1950s and 1970s, these representations have not been used in serious applications for a long time. In 1986, by adding some ingenious ordering restrictions to these models and providing a sophisticated reduction mechanism, R. Bryant substantially improved the model. Since this time, the improved representation, denoted as OBDD, has invaded nearly all areas of computer-aided VLSI design.
Christoph Meinel, Thorsten Theobald

7. Efficient Implementation of OBDDs

Abstract
So far, we have mainly considered structural properties of ordered binary decision diagrams. Several of these properties, like the linear-time equivalence test, already indicate the suitability of OBDDs in the context of Boolean manipulation. However, as the efficiency of all OBDD-based applications depends almost exclusively on the efficiency of the basic OBDD operations, the demands on the performance of these operations are very high. Hence, much research effort has been spent on transforming the basic OBDD concept into fast and memory-efficient implementations.
Christoph Meinel, Thorsten Theobald

8. Influence of the Variable Order on the Complexity of OBDDs

Abstract
In this chapter we analyze the influence of the variable order on the complexity of OBDDs. The following two theorems, which immediately follow from the Theorems and Corollaries 6.9 to 6.12, are applied several times.
Christoph Meinel, Thorsten Theobald

9. Optimizing the Variable Order

Abstract
Before representing and manipulating switching functions in terms of OBDDs, an order on the set of variables has to be fixed. In the previous chapter, we have seen that the construction of the optimal variable order is a very critical venture — as it is related to exploding running times. A good order can lead to a very compact representation and hence to small running times, whereas a bad representation may exceed the physically ex-isting memory and hence causes the whole computation to abort. Even in the cases where bad variable orders do not cause a memory overflow, they lead to unacceptably large running times.
Christoph Meinel, Thorsten Theobald

Applications and Extensions

Frontmatter

10. Analysis of Sequential Systems

Abstract
The design of increasingly complex electronic systems makes it more and more difficult to verify their correct behavior. At the same time it becomes more and more important that the systems work correctly, as nowadays human lives seriously depend on them, e.g., in traffic or in medicine.
Christoph Meinel, Thorsten Theobald

11. Symbolic Model Checking

Abstract
In the verification methods presented in Chapter 10, the model of finite state machine was the center of attention. Based on this, we now consider the more general verification concept of model checking. This concept is not strictly tied to the model of finite state machine, but is capable in addition of handling logic-based specifications.
Christoph Meinel, Thorsten Theobald

12. Variants and Extensions of OBDDs

Abstract
To further improve the efficiency of the data structure of OBDDs, several variants and extensions have been proposed. For the requirements in specific application fields, these refined models are better suited than the “classic” OBDDs. We would like to present some particularly interesting and important developments in this area, although the relevant research efforts have not been completed yet. The search for more compact representations of switching functions, which preserve the valuable properties of OBDDs, is still ongoing.
Christoph Meinel, Thorsten Theobald

13. Transformation Techniques for Optimization

Abstract
In this chapter, we introduce transformation techniques which serve to further optimize OBDD representations. The optimization space in this framework goes far beyond the optimization space established by the optimization of the variable order.
Christoph Meinel, Thorsten Theobald

Backmatter

Weitere Informationen