This paper develops new data structures to represent Boolean functions. These functions are described by means of directed, acyclic graphs, in a manner that resembles the binary decision diagrams introduced by Lee [1] and Akers [2]. In the most general case, the difficulty of solving the problems of determining whether two Boolean expressions are equivalent or whether there exists an input combination that sets the value of an expression to 1 grows exponentially with the size of the expressions. As a consequence, a number of methods have been developed for representing and manipulating restricted classes of Boolean functions, so that exponential computations will be avoided.

In this paper, new procedures are presented for manipulating restricted classes of Boolean functions. In spite of the restrictions, many of the commonly used functions can be represented. The procedures, however, require some heuristics in selecting the ordering of the system inputs as arguments to all of the functions to be represented. For some functions, the size of the graph that represents the function is highly sensitive to this ordering, but the problem of computing an ordering that minimizes the size of the graph is itself an NP-complete problem. The paper presents experimental results from applying the procedures to some problems in logic design verification to demonstrate the practicality of the approach.