Dynamic variable ordering for ordered binary decision diagrams
Top Cited Papers
- 30 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
The ordered binary decision diagram (OBDD) has proven useful in many applications as an efficient data structure for representing and manipulating Boolean functions. A serious drawback of OBDD's is the need for application-specific heuristic algorithms to order the variables before processing. Further, for many problem instances in logic synthesis, the heuristic ordering algorithms which have been proposed are insufficient to allow OBDD operations to complete within a limited amount of memory. The paper proposes a solution to these problems based on having the OBDD package itself determine and maintain the variable order. This is done by periodically applying a minimization algorithm to reorder the variables of the OBDD to reduce its size. A new OBDD minimization algorithm, called the sifting algorithm, is proposed and appears especially effective in reducing the size of the OBDD. Experiments with dynamic variable ordering on the problem of forming the OBDD's for the primary outputs of a combinational circuit show that many computations complete using dynamic variable ordering when the same computation fails otherwise.Keywords
This publication has 9 references indexed in Scilit:
- Proving circuit correctness using formal comparison between expected and extracted behaviourPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Logic verification using binary decision diagrams in a logic synthesis environmentPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Evaluation and improvement of Boolean comparison method based on binary decision diagramsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Dynamic variable ordering for ordered binary decision diagramsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Minimization of binary decision diagrams based on exchanges of variablesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- On variable ordering of binary decision diagrams for the application of multi-level logic synthesisPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Efficient implementation of a BDD packagePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Shared binary decision diagram with attributed edges for efficient Boolean function manipulationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986