Efficient Implementation of a BDD Pack.age Karl S. Brace’ Dept of ECE Carnegie Mellon Pittsburgh, PA 152 13 Randal E. Bryant* School of Computer Science Carnegie Mellon Pittsburgh, PA 152 13 Richard L. Rudell Syinopsys, Inc. 1098 Alta Avenue Mountain View, CA 94043 Abstract Efficient manipulation of Boolean functions is an important component of many computer-aided design tasks. This paper describes a package for manipulating Boolean functions based on the reduced, The ordered, binary decision diagram (ROBDD) representation. package is based on an efficient implementation of the if-then-else (ITE) operator. A hash table is used to maintain a strong carwnical form in the ROBDD, and memory use is improved by merging the hash table and the ROBDD into a hybrid data structure. A memory funcfion for the recursive ITE algorithm is implemented using a hash-based cache to decrease memory use. Memory function efficiency is improved by using rules that detect. when equivalent functions are computed. The usefulness of the package is enhanced by an automatic and low-cost scheme for rec:ycling memory. Experimental results are given to demonstrate why various implementation trade-offs were made. These results indicate that the package described here is significantly faster and more memory-efficient than other ROBDD implementations described in the literature. in CAD have an exponential size in the sum-of-:products representation [9], and checking tautology in a general Boolean network appears to be intractable [lo], making these representations unacceptable for a general package. The representation we have found most useful for manipulating Boolean functions is the reduced, ordered, binary-decision diagram (ROBDD) [Il. 12. 131. The ROBDD is a canorlical fOm, so the tautology test is a constant-time comparison against the unique representation of the function 1. While the size of the ROBDD can be exponential in the worst case, ROBDD's remain small for many of the functions we are interested in. We are aware of several computer implementations of ROBDD's, but few have been put forward as a reusable package, and fewer still have had their performance measured and compared. Our primary goal was to develop a generic package interfac:e that would hide the details of the package implementation, yet still be efficient in computer run-time and memory use. We also wanted to understand the various trade-offs possible in an ROBDD package to tailor such a package for our applications in CAD. 2 Programming Techniques 1 Introduction The efficient representation and manipulation of Boolean functions is important for many algorithms in a wide variety of applications. In particular, many problems in computer-aided design for digital circuits (CAD) can be expressed as a sequence of operations performed over a set of Boolean functions. Some exampIes from CAD are combinational logic verification [l, 21, sequential-machine equivalence [3]. logic optimization of combinational circuits [4]. test pattern generation [5], timing verification in the presence of false paths [6], and symbolic simulation [7]. Hence it is desirable to develop a general-purpose software package for manipulating Boolean functions which allows variables to be created, and allows standard Boolean operations such as AND, OR, and NOT to be performed on functions. The package should also allow a function to be tested for tautology - i.e., to determine whether the function evaluates to I for all inputs. The problem with developing such apackagels that the tautology problem is co-NP complete [8]. This implies that all known solutions require time which grows exponentially with the number of variables in the worst case. However, by developing clever representations and efficient manipulation algorithms, it is often possible to avoid an exponential computation. Many different representations have been proposed for manipulating Boolean functions and each has a corresponding algorithm to test for tautology. However, many of the functions of interest *This researchpartially funded by Semiconductor Research Corporation contract number 90-DC-068. A hash table associates a value with a key. A hashfunction applied to the key selects which of N linked lists the key,value pair is stored. The loadfactor of a hash table is defined as cx =: n/N, where n is the number of keys stored in the table. A memory function for the function F is a table of values (z, F(r)) that the function has already computed. If F is called with argument 2 again, F(z) is returned without any computation. A hash-based cache is a hash table where a collision chain is not used to resolve collisions. Instead, at insert time, any existing element at the particular array position is discarded and replaced with the new entry. At lookup time, if the element does not match the stored key, a cache miss occurs and no element is returned. A strong canonical form is a form of preconditioning which reduces the complexity of an equivalence test between elements in a set. A unique id is assigned to each unique element in the set, so an equivalence test is a simple scalar test between the unique id’s of each element. Garbage collection is a class of techniques to periodically free unused memory. It is useful when references to the structures being freed prevent incremental freeing. The cost of searching for these references is amortized over many free operations. 3 BDD Overview 3.1 Basic Definitions Basic definitions for binary decision diagrams (also known as function graphs) are given in [13]. We review some of these definitions here for reference. 27th ACM/IEEE Design Automation Conference@ Paper 3.1 40 0 1990 IEEE 0738-100X/90/0006/0040 $1 .OO A binary decision diagram (BDD) is a directed acyclic graph (DAG). The graph has two sink nodes labeled 0 and 1 representing the Boolean functions 0 and 1. Each non-sink node is labeled with a Boolean variable v and has two out-edges labeled 1 (or then) and 0 (or else). Each non-sink node represents the Boolean function corresponding to its 1 edge if v = 1. or the Boolean function corresponding to its 0 edge if v = 0. An ordered binary &&ion diagram (OBDD) is a BDD with the constraint that the input variables are ordered and every source to sink path in the OBDDvisits the input variables in ascending order. A reduced ordered binary decision diagram (ROBDD) is an OBDD where each node represents a distinct logic function. Bryant [13] was the first to prove that the ROBDDis well-defined. Bryant also showed the ROBDD is a canonical form for a logic function; that is, two functions are equivalent if, and only if, the ROBDD'S for each function are isomorphic. It is well known that the size of the ROBDD for a given function dependson the variable order chosen for the function. This paper is not concerned with the variable ordering problem. In practice, we have found that a simple topological based ordering heuristic, such as proposed by Malik et al. [l], is sufficient for many applications in CAD. Notation The sink nodes of the ROBDDare written as 1 and 0. A variable is denoted by a lowercase letter, such as v. The variables in the ROBDDare totally ordered. We say that v is smaller than w (v < w) if v comes before w in the variable order (higher up in the ROBDD). At each node F there is a variable v and v is called the fop variable of F. The top variable of a set of formulas is the smallest of the top variables of those formulas. Each node in the ROBDDrepresents a Boolean function, and is written using a capital letter, such as F, and can be denoted by the triple (v, G, H), where v is the top variable of F, G is the node connected to the I (or then) edge of F, and H is the node connected to the 0 (or else) edge of F. A node in the ROBDDwhich represents a function the user is interested in is called a formula. Other nodes, which are needed to build a user’s formula, are called internal nodes. 1F 1is the number of nodes below F in the ROBDD. 4.2 ITE Operator The If-Then-Else or ITE operator forms the core of the package. ITE is a Boolean function defined for three inputs F, G, H which computes: If F then G else H. This is equivalent to: ite(F,G,W)= Expression 0 oool 0010 0011 0100 0101 0110 0111 loo0 1001 1010 1011 1100 1101 1110 1111 AND(F,G) F>G F FG NO-W) FIG NAND(F,G) 1 F-G F-E F F.G G F@G F+G F+G F@G F F+?? P P+G F-G 1 Equivalent form 0 ite( F, G, 0) ite(F,E,O) F ite(F,O, G) G ite(F,c,G) ite(F,l,G) ite(F,O,c) ite(F,G,E) ite(G,O, 1) ite( F, 1, E) ite(F,O, 1) ite( F, G, 1) ite(F,E, 1) 1 Figure 1: All two variable functions described using lTE. The unique-table maps a triple (v, G, H) to an ROBDDnode Each node in the ROBDDhas an entry in the unique-table. Before a new node is added to the ROBDD,a lookup in the unique-table determines if a node for that function already exists. If so, the existing node is used. Otherwise, the new node is added to the ROBDD and a new unique-table entry is made. By assumption, when we create a new node F, the nodes G and H will already obey the strong canonical form. Hence, the function F exists in the ROBDD if, and only if, the triple (v, G, H) is already in the unique-table, thus maintaining the strong canonical form. The unique table allows a single multi-rooted DAG to represent all of the user’s formulae simultaneously. 4.4 Unique-Table A hash table imposes a strong canonical form on the nodes in the ROBDD.so that each node in the ROBDDrepresents a unique logic function. Hence, this hash table is called the unique-table. Recursive Formulation of ITE Shannon’s decomposition theorem states that where F, and Fc are F evaluated at v = 1 and v = 0 respectively. Let F = (2u,T, E) and assumev < zu. Finding the cofactors of F with respect to v is trivial: F. = F (if v < v) or T (if v = w), andFT=F(ifv