History-based dynamic BDD minimization

Binary decision diagrams (BDDs) are the state-of-the-art data structure in VLSI CAD. Since their size largely depends on the chosen variable ordering, dynamic variable reordering methods, like sifting, often have to be applied during the construction. Usually sifting is called each time a given node limit is reached and it is therefore called frequently during the creation of large BDDs. Often most of the runtime is spent for sifting while the BDD is built. In this paper we propose an approach to reduce runtime (and space requirement) when constructing BDDs for a given circuit or when computing the set of reachable states in sequential verification. Dependent on the history of the construction process different types of sifting are called. For the BDD construction of combinational circuits we present two methods, one is based on statistics of the unique table, the other one is based on the size reduction of the previous run of sifting. For sequential verification, we propose to select the type of sifting according to the number of iterations processed. Experimental results clearly demonstrate the efficiency of the approach. (C) 2001 Elsevier Science B.V. All rights reserved.