Haim Cohen received his BSc in computers and software engineering from Technion—Israel Institute of Technology. He is a software engineer at the Analog Devices DSP design center in Herzlia, Israel. He can be reached at [email protected] and [email protected].
Boolean expressions are common in electronic design automation (EDA) software, and you might even meet them in totally different problem domains. Whether you are involved in large projects or just need to write some small utility to solve a specific problem, you should be familiar with at least one good Boolean expression library that can do some of the job for you.
You can think of Boolean expressions as functions of Boolean variables. An expression can be a single variable or operations on one or more other expressions. Given an assignment of the expression variables, it evaluates to a constant value. For example, the Boolean expression !(a1 XOR b1) & !(a0 XOR b0) evaluates to 1 if and only if the two 2-bits binary numbers a1 a0 and b1 b0 are identical. It is important to remember that different Boolean expressions can be logically equivalent, which means they represent the same Boolean function.
Boolean expression libraries should give you the ability to create, manipulate, and analyze Boolean expressions in a relatively straightforward manner and with good performance. By "analyze" I mean the ability to retrieve information about a given Boolean expression. For example, after creating a complex Boolean expression, you might wonder which inputs—variable assignments—evaluate to 1. An input vector for which the expression is true is called a "satisfying assignment." If there are no such inputs, it means that the complex expression you created is actually equivalent to the constant 0. The last problem is a well-known computer-science problem—the SAT problem, which is the root of almost all NP-complete problems.
One approach to dealing with Boolean expressions is by using a data structure called Binary Decision Diagram (BDD). (Actually, the correct term to use is "Reduced Order Binary Decision Diagram," ROBDD, but you might find that in BDD's terminology, ROBDDs are referred to as BDDs.) Let's just say that BDD is a graph-like data structure that implements a Boolean expression in a compact way.
There are several libraries that let you implement and manipulate Boolean expressions, including CAL (http://www-cad.eecs.berkeley .edu/Respep/Research/bdd/cal_bdd/), BDD (http://www-2.cs.cmu.edu/ afs/cs/project/modck/ pub/www/bdd.html), CUD (http://vlsi.colorado .edu/~fabio/), and PBF (http://www-2.cs.cmu .edu/~bwolen/software/), among others. In this article, I focus on the BuDDy library (http:// sourceforge.net/projects/buddy), which was developed by Jrn Lind-Nielsen at the IT University of Copenhagen. BuDDy exposes a BDD interface rather than a Boolean expression interface. However, once you think of the BDD type as a Boolean expression, it is easy to work with BuDDy using a small subset of the interface without a deep understanding of BDDs.
The BuDDy Library
Although BuDDy does not have the GNU public license, the code is open for modifications and is in public domain. BuDDy is implemented in C but has a wrapping C++ interface. You can use the C interface, but it is easier to use the C++ interface without worrying about performance because all the internals are implemented in C.
BuDDy has an internal garbage collection mechanism optimizing its memory usage, totally transparent if you decide (and you better) to use the C++ interface. BuDDy also has a cache that saves the last results of operations. Almost everything performance related is configurable through the interface, and the library begins runs with default values, so you can start using it without being familiar with all the possible configurations.
BuDDy has a rich set of operations, which can help you implement very complex operations with only a few code lines. Among the operations in the interface are the abilities to define the variables (inputs) of the expressions you are going to create, refer a large vector of binary variables as a vector of encoded integers, and create a vector of expressions.
The manipulation operation includes the ability to perform various kinds of Boolean operations on one or more expressions, and vector-oriented operations on vectors of expression (such as ==, >, and the like), referring to them as encoded integer or bitwise—operating on each expression in the vector separately.
The results of the operations are Boolean expressions or vectors, which, together with the overloaded operators of the C++ interface, give a powerful syntax to create complex Boolean expressions easily. Although the examples demonstrate the power of BuDDy, they cannot cover all the aspects and capabilities of the library.
If you use BuDDy in your application, I recommend that you at least read the functions reference of the library to get some idea about which kind of operations are already supplied to you in BuDDy. In this article, I'll present three examples that demonstrate some of BuDDy's capabilities. With each example, I first explain the problem, then present the solution, and finally implement the solution with BuDDy.
Propagation Enabling Assignment
Suppose you have a logic gate that implements some Boolean function. For some reason (for example, the need to simulate the electric circuit that implements this gate), you need to fix all the inputs of that gate except one input to constant values of 0 and 1 so that a signal can propagate from the nonfixed input to the output. By "propagate" I mean that a change in the input (from 0 to 1 or 1 to 0) causes a change in the output.
To do so, you need to find at least one assignment for the fixed inputs that will enable propagation from the nonfixed input to the output. An example of this is the AND gate of two inputs: an assignment of 1 in one of the inputs enables a propagation of a signal from the other input to the output. In the OR gate, a fixed value of 0 in one of the inputs enables a propagation from the other input.
To simplify the explanation of the solution, assume you have a gate of three inputs and one output, which implements the Boolean function z(a,b,c) = ( a | b ) & c. ( "|" stands for "OR", and "&"for "AND"). The task is to find all the assignments of a and c that enable a propagation from b to the output z. The new function p(a,c) = z(a,0,c) XOR z(a,1,c) gives 1 for each a and c that fulfill the requirement.
Why is it true? From the definition of "propagation of a signal from b to z," you can see that you need to find a and c so different b values result in different output values. This is exactly what p(a,c) checks: Different values of b (0 or 1) give different outputs. (The difference of the outputs is checked by XORing the outputs in each different input of b.) So if you have at least one pair of a and c values for which p(a,c) is true, you get the solution!
Listing 1 is the BuDDy implementation taken from the file gate.cpp and is relatively straightforward. First, declare the number of variables in the expression. Since the number of variables in the original function z is 3, you use z to create p, so you declare three variables, as in line 1.
Since the basic data types in BuDDy are the BDDs (Boolean expressions), you create three expressions that represent the three input variables a, b, and c—lines 2, 3, and 4, respectively. The function bdd_ithvar() returns the BDD corresponding to a variable's index. The z function is also an expression, and it is defined in line 5. In lines 6 and 7, you create z(a,1,c) and z(a,0,c), respectively. With bdd_restrict(), you can restrict one or more variables of expression to constant values, and get a BDD that represents the new expression—in this case z(a,1,c) and z(a,0,c). In line 9, you create p(a,c) by XORing z(a,1,c) with z(a,0,c). The last thing to do is to find out the values of a and c for which p is true.
BuDDy prints a Boolean expression by printing all its satisfying vectors (input vectors for which the expression is true), so the easiest way to get the solution is to print p, as in line 9. The output of the program execution is in Listing 1, line 9. The output is composed of vectors (only one vector, in this case), and each place in the vector has the variable's index from the left side of the colon and its value from the right side of the colon. Those vectors represent the input variables for which the Boolean expression is true. The value of the variable with index 0 (which is a as defined in Listing 1, line 2) is 0, and the value of the one with index 2 (variable c) is 1.
You can conclude that p(a,c) is true only for a=0 and c=1. If you take a look at the truth table of the function z(a,b,c) in Figure 1, you can verify that only for the aforementioned values of a and c, a signal can propagate from b to the output. The power of the Boolean expression library is its performance. When using the BDD data structure to implement Boolean expressions, operations like this are performed in less time than required for exhaustive testing of all the possible inputs.
Logic Equivalence of Two Boolean Expressions
If you are dealing with Boolean expressions, it might be of interest to find out if two Boolean expressions are logically equivalent; that is, if they implement the same Boolean function, although expressed in a different way. For example, a & ( b | c ) is logically equivalent to a & c | a & b, although the first function is expressed with two Boolean operations and the second one with three operations. The naive way to determine whether two expressions are logically equivalent is, of course, to try all the possible inputs in the worst case.
When Boolean expressions are implemented with BDDs, this operation averages less time than the time required for exhaustive testing of all the possible inputs. This feature is achieved because BDD is a compact representation of a Boolean expression.
To explain the solution, I use as an example a comparator implementation that checks whether two numbers are equal. Using this example, I show how a series of variables can be referred to as one vector, which lets you perform complex operations on vectors of bits without the need to implement that operation on single bits. For example, BuDDy lets you multiply two binary vectors of variables and get a new vector. Thanks to this feature, you do not have to implement the Boolean equations of multiplying two integers. I create three functions to implement a comparator of 16 bits, as in Figure 2. The first two functions should be logically equivalent, and the third one should not be equivalent to the first two since it intentionally has an erroneous implementation.
You can see in Figure 2 how the comparator eq_1 is implemented (of course, this is not efficient in any terms, it is just for the example) by checking that both vectors are less than or equal to one another, therefore equal.
The comparator eq_2 is implemented by checking that all the bits are equal. The eq_wrong comparator looks much like eq_1, except it has a flaw—the right block is < instead of <=. Using BuDDy, I implement all three comparators and show that eq_1 is logically equivalent to eq_2, while eq_wrong is not equivalent to the first two comparators.
Listing 2 is from file comp.cpp. In line 3, I declare the required number of variables as before. Since each input of the comparator is 16 bits, you need 32 variables. In lines 4 and 5, I create vectors of variables, bvec. The function bvec_var creates bvec using the previously defined variables. The parameters to bvec_var are <bits number>, <from>, and <step>, so the resulting bvec is composed of <bits number> bits, which are the previously defined variables with the indices <from>, <from>+<step>, <from>+2*<step>, ...and so on.
You can see in line 6 how easy it is to perform the >= and <= operations on bvecs, as they were integers. Under the hood, BuDDy is performing the required Boolean operations on the bvec elements, which are BDDs. The eq_1 comparator is defined in line 6. In lines 7, 8, and 9, I implement the eq_2 comparator. This time I perform the Boolean operations directly on the BDDs that compose the bvec. In line 10, I create eq_wrong, which is intentionally wrong. In the rest of the code, I check the logic equivalence of the comparator implementations using the != operator on the two Boolean expressions. eq_1 and eq_2 should be equivalent, in contrast to eq_1 and eq_wrong, which should not be equivalent.
Formatted Output With Finite Domain Blocks
In this last example, I present how the binary input vectors can be seen as integer vectors using the eq_1 comparator (from the previous example) to print all the inputs for which eq_1 is true.
What are "Formatted Output With Finite Domain Blocks"? When you work with Boolean expressions, you have a vector of Boolean input variables. Sometimes it is more convenient to display this vector as a vector of integers, where each "block" in the vector represents an integer. For example, 10 binary variables can represent two integers: one of 3 bits, and the second of 7 bits.
Formatted Output With Finite Domain Blocks (fdds) let BuDDy display the output in terms of integers instead of bits. Listing 3 is the code for this example. The complete code is in the file equiv.cpp (available at http://www.cuj.com/code/). In line 5, I define how the binary input vector is organized into blocks, where each block represents an integer. In this example, you organize the binary input vector into two blocks, each one represents integers from 0 to 3.
Each integer represents one input (composed of 2 bits) to the comparator. In the rest of the code, I create the eq function as in the previous example, and then print it. Printing the function the usual way, as in line 13, gives you all the vectors for which eq is true, in the binary form. Each vector is composed of four components, and each component is the bit index and its value. This is exactly as before.
In line 16, I take advantage of the finite domain blocks defined before, and print the eq function using the fddset manipulator. This time the output is more readable—there are four vectors as before, but the vectors are composed of two 2-bits integers instead of 4 bits. You can see how each integer is corresponded to a finite domain block defined in line 5.
Conclusion
BuDDy is a powerful library for Boolean expression manipulation; it combines as easily as a C++ interface and is an efficient implementation based on the novel BDD data structure. Although you can work with BuDDy without understanding what BDDs are, it is worth understanding the concept of BDD structure and usage when developing large applications that are heavily based on Boolean expression.
