Topics:
Why BDDs?
Overview of the class material
Possibilities to adjust material to students' needs
Student projects and project requirementsReading:
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 methodsReading:
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 siftingReading:
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 problemReading:
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 DDsReading:
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