ECE 510 OCE (Spring 2000)

Binary Decision Diagrams and Their Applications in Logic Synthesis, Verification, and Testing

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

Attention: The final version of slides is available at 5pm on lecture days!

Class Schedule*

Lecture 1.  March 28, 2000, Tuesday - Introduction
Why BDDs?
Overview of the class material
Possibilities to adjust material to students' needs
Student projects and project requirements

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

Lecture 2.  March 30, 2000, Thursday - Fundamentals - PowerPoint - PDF - Color PDF

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

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.

Lecture 3.  April 4, 2000, Tuesday - Basic manipulation algorithms and complexity issues - PowerPoint - PDF - Color PDF

The ITE operator and its properties
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

Lecture 4.  April 6, 2000, Thursday - BDD-Based Representations - PowerPoint - PDF - Color PDF

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

Lecture 5.  April 11, 2000, Tuesday - Variable reordering - PowerPoint - PDF - Color PDF

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

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

Lecture 6.  April 13, 2000, Thursday - Programming with BDDs (1) - PowerPoint - PDF - Color PDF

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

BuDDy Manual.

Lecture 7.  April 18, 2000, Tuesday - BDDs for Symmetric Functions - Constraint satisfaction problems - PowerPoint - PDF - Color PDF

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

Lecture 8.  April 20, 2000, Thursday - Image computation and reachability analysis - PowerPoint - PDF - Color PDF

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

Lecture 9.  April 25, 2000, Tuesday  - Programming with BDDs (2) - PowerPoint - PDF - Color PDF

Mapping elementary BDD variables
Building transition/output relation from STG
BDD operators for image computation
Programming reachability analysis procedures
Programming error trace generation

Lecture 10.  April 27, 2000, Thursday - Advanced Topics in Reachability Analysis - PowerPoint - PDF - Color PDF

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

Lecture 11.  May 2, 2000, Tuesday - FSM Equivalence Checking and FSM State Minimization - PowerPoint - PDF - Color PDF

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

Lecture 12.  May 4, 2000, Thursday - Preliminary discussion of projects

Lecture 13.  May 9, 2000, Tuesday - (1) Compatible Projection (2) Implicit Formulation for Problems in Boolean Networks - PowerPoint - PDF - Color PDF
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

Lecture 14.  May 11, 2000, Thursday - Covering problems and two-level logic minimization - PowerPoint - PDF - Color PDF

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)

Lecture 15.  May 16, 2000, Tuesday - Functional Decomposition (1) - PowerPoint - PDF - Color PDF

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

Lecture 16.  May 19, 2000, Thursday - Functional Decomposition (2) - PowerPoint - PDF - Color PDF

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)

Lecture 17.  May 23, 2000, Tuesday - Implicit multi-output decomposition - PowerPoint - PDF - Color PDF

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)

Lecture 18.  May 25, 2000, Thursday - Implicit decomposition of finite state machines - PowerPoint - PDF - Color PDF

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

Lecture 19.  May 30, 2000, Tuesday - Verification Using Specialized Decision Diagrams - PowerPoint - PDF - Color PDF

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

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.

Lecture 20.  June 1, 2000, Thursday - Sequential Verification - PowerPoint - PDF - Color PDF

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

Lecture 21.  June 6, 2000, Tuesday - Conclusions and presentations of projects

Lecture 22.  June 8, 2000, Thursday - Conclusions and presentations of projects


* The schedule is subject to change without notice

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