Link to the main class page - Link to the BDD resources page

Topics:

Why BDDs?

Overview of the class material

Possibilities to adjust material to students' needs

Student projects and project requirements

Reading:

1) H.R.Andersen. Introduction to BDDs (Lecture Notes)

2) R.E.Bryant. Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams,ACM Computing Surveys, Vol. 24, No. 3 (September, 1992), pp. 293-318. Available from Randy Bryant's Home.

The BDD package (with manual and source code examples):

BuDDy from Jorn Lind-Nielsen, Computer Systems Section at the Department of Information Technology, Technical University of Denmark

Topics:

Canonical and non-canonical forms of boolean functions

Decision trees and reduction rules

Standard BDDs vs. Zero-Suppresed BDDs

BDDs with and without complementary edges

Building already reduced diagrams recursively

Tradeoffs between implicit and explicit methods

Reading:ITE operator and complement edges:G. Hachtel, F. Somenzi, Logic Synthesis and Verification Algorithms, Kluwer, 1996. Chapter 6, pp. 233-243.Zero-suppressed BDDs:S.Minato, Binary Decision Diagrams and Applications for VLSI CAD. Kluwer, 1996. Chapter 6, pp. 61-70.

Topics:

The ITE operator and its properties

Algorithms for APPLY, RESTRICT, REPLACE, COMPOSE

Quantification (existential, universal, unique)

Complexity of BDD operators

Estimation of complexity of BDD representation of boolean functions using cross sections

What is common to these and other efficient procedures?

Generic recursive algorithm

Topics:

BDD-based representation of sets, cubes, partitions, graphs, matrices, state machines

What is common to all successful BDD-based applications?

Selecting representation for your problem

Topics:

Connection between variable ordering and BDD size

The size of decision diagrams for symmetric functions

Exact minimization of BDDs is NP-complete

The fan-in based heuristic to find good static variable ordering for BDDs representing outputs of logic networks

Dynamic reordering based on variable swap

Reordering algorithms: window permutation, sifting, block sifring, symmetric sifting

Reading:

Ch. Meinel, Th. Theobald. Algorithms and Data Structures in VLSI Design: Foundations of OBDD Applications, Springer, 1998, Chapter 9, pp. 145-170.

Topics:

Downloading and compiling the BDD package

Starting the package and defining variables

Building BDDs from elementary BDD representing variables in positive and negative polarity

Most often used operations on BDDs

Typical structure of an efficient BDD-based procedure

Examples: 1) Counting the number of true assignments of a function. 2) Getting one true assignment of a function

The importance of hashing

Homework problem

Reading:

BuDDy Manual.

Topics:

BDDs for symmetric functions

Characteristic functions of sets and sets of sets

Building BDD for Tuples “k out of n”

Constraint satisfaction problems

Example: N-queen Problem

Binate Covering Problem

Solution of BCP using Shortest Path on BDDs

Topics:

Relations as a fundamental representation of discrete phenomena

Image computation for relations

Representing FSMs using relations

Reachability analysis as an exploration of the state space of FSMs using the transition relation

Applications of reachability analysis

(1) Computing the transitive closure of relations

(2) Equivalence checking of FSMs

Topics:

Mapping elementary BDD variables

Building transition/output relation from STG

BDD operators for image computation

Programming reachability analysis procedures

Programming error trace generation

Topics:

Variable ordering for reachability analysis

(1) Extension of Malik’s heuristics for static ordering

(2) Combination of static and dynamic reordering

The generalized cofactor and its flavors: constraint and restrict

Improvements to image computation

(1) Interleaved variable ordering

(2) Iterative squaring

(3) Transition relation clustering

(4) Recursive image computation

Topics:

Equivalence for FSMs and FSM states

Product machine (PM)

Solving the problem of FSM equivalence

- Derive transition and output relation of the PM

- Perform reachability on the PM and verify property PM_Output = 1

- Generate an error trace if the equivalence check has failed

Solving the problem of FSM state minimization

- Derive transition and output relation of the PM

- Perform reachability on the PM and derive the state equivalence relation

- Transform the initial FSM’s transition and output relations

Compatible projection operator

Topics:

Compatible projection operator

- Background

- Recursive algorithm

- Applications (FSM state minimization, FSM decomposition, functional decomposition, checking non-determinism, etc.)

Representations of Boolean networks

- functional

- structural

Problems in Boolean networks

- test pattern generation

- fault localization

- optimization (for the number of nodes, area, delay, testability)

- eliminating combinational loops, etc

Topics:

Covering problems

- Unate and binate covering problems

- Branch-and-bound procedure

- Explicit vs. implicit reduction of the covering table

Two-level sum-of-products minimization

- Irredundant cover computation (Minato/Morreale)

- Explicit Quine-McCluskey procedure

- Implicit Quine-McCluskey procedure based on formulas with quantifiers

- Implicit minimization procedure based on transposing functions (Coudert/Madre)

Topics:

The concept of functional decomposition

Two uses of BDDs for decomposition

- as a computation engine to implement algorithms

- as a representation that helps finding decompositions

Two ways to direct decomposition using BDDs

- bound set on top (Lai/Pedram/Vardhula, DAC’93)

- free set on top (Stanion/Sechen, DAC’95)

- other approaches

Disjoint and non-disjoint decomposition

Implicit support minimization

Topics:

Other approaches to functional decomposition

- Recursive decomposition (Bertacco/Damiani, ICCAD’97)

- Bi-decomposition using 1-, 0-, and x-dominators (Yang/Ciesielski, ICDD’99)

- Implicit, multi-output decomposition (Wurth/Eckl/Legl, DAC’95)

- Decomposition based on Information Measures (Chojnacki/Jozwiak, 1997)

(presented by Artur Chojnacki)

Topics:

Implicit representation of partitions

- equivalence relations as char functions of partitions

- operations on partitions

Approaches to functional decomposition

- Implicit, multi-output decomposition (Wurth/Eckl/Legl,DAC’95)

Topics:

Implicit multi-output decomposition (part 2)

- finding the global partition

- implicitly selecting next preferable function

- Lmax algorithm

Parallel and serial FSM decomposition

- deriving the lattice of S.P. partitions

- find good partitions (partition pairs)

- performing decomposition implicitly using transition/output relations

Topics:

Extensions of Binary Decision Diagrams

- Multi-terminal BDDs (MTBDDs) (Clarke, DAC‘93)

- (Multiplicative) binary moment diagrams (BMDs/*BMDs) (Bryant, DAC’95)

- Edge-valued BDDs (EVBDDs) (Lai, DAC’92)

- Kronecker functional decision diagrams (OKFDDs) (Drechsler/Sarabi/Perkowski, DAC’94)

- Kronecker multiplicative moment diagrams (K*BMDs) (Drechsler, EDTC’96)

Word-level DDs vs. bit level DDs for verification

Binary expression diagrams (Andersen/Hulgaard,1997)

Advantages and limitations of the specialized DDs

Reading:

1) R E.Bryant, and Y.-A.Chen. "Verification of Arithmetic Circuits with Binary Moment Diagrams'', Proc. of DAC '95, pp. 535-541. Winner of best paper award in category ``Verification, Simulation, and Test.'' Available from Randy Bryant's Home.

2) R. Drechsler, B. Becker, S. Ruppertz. "The K*BMD: A Verification Data Structure". IEEE Design and Test of Computers,Vol. 14, No. 2, April-June 1997, pp.51-59. The electronic version is available from IEEE D&T to subscribers of IEEE Computer Society Digital Library.

3) B. Hatt. "Decision Graphs for Verification" (ECE572 Project). Available here.

Topics:

Examples of formal verification

Verifiable properties

Symbolic model checking

- Temporal logics and CTL

- Implementation of CTL model checking

Language containment

- Finite automata and L-automata

- Omega-regular languages

- Language containment algorithm

Last update 4:20pm, June 1, 2000.