Method for verifying and representing hardware by decomposition and partitioning

A system and method for representing digital circuits and systems in multiple partitions of Boolean space, and for performing digital circuit or system validation using the multiple partitions. Decision diagrams are built for the digital circuit or system and pseudo-variables are introduced at decomposition points to reduce diagram size. Pseudo-variables remaining after decomposition are composed and partitioned to represent the digital circuit or system as multiple partitions of Boolean space. Each partition is built in a scheduled order, and is manipulable separately from other partitions.

BACKGROUND OF THE INVENTION
 The present invention relates generally to the field of computer-aided
 design (CAD) systems and methods, and in particular to CAD systems and
 methods for digital circuit design and verification.
 Computer-aided design of digital circuits and other complex digital systems
 is widely prevalent. In such computer-aided design, circuits and systems
 are usually designed in a hierarchial manner. The requirements of the
 circuit or system are defined in an abstract model of the circuit or
 system. The abstract model is then successively transformed into a number
 of intermediate stages. These intermediate stages often include a register
 transfer level model which represents a block structure behavioral design,
 and a structural model which is a logic level description of the system.
 Eventually a transistor net list and consequently the physical layout of
 the circuit or system are derived.
 The design of the circuit or system therefore proceeds from the general
 requirements level to the lower detailed level of a physical design,
 interposed between which are a number of intermediate levels. Each
 successive level of the design is tested or verified to ensure that the
 circuit or system continues to meet the design requirements. It is highly
 desirable to verify each level in the design as errors in one level of the
 design that are not corrected until after further levels have been
 designed drastically increases the cost of correcting such errors. Thus,
 it is important to test each level of the design against the requirements.
 As each level of the design is tested against the requirements, this task
 resolves to the task of comparing each level of the design to the prior
 level of the design. This testing of succeeding levels against immediately
 preceding levels can also be intuitively seen when it is realized that
 each succeeding level is often merely an optimization of the preceding
 level. Thus, the testing or verification of circuit designs can, to an
 extent, be viewed as similar to checking the backward compatibility of
 successive generations of circuits or systems.
 Binary decision diagrams (BDDs) have been used to solve CAD related
 problems. These problems include synthesis problems, digital-system
 verification, protocol validation, and generally verifying the correctness
 of circuits. BDDs represent Boolean functions. For example, FIG. 1 shows a
 circuit comprising first and second OR gates 11, 13, and an AND gate 15.
 The first OR gate has inputs N1 and N2. The second OR gate has inputs N2
 and N3, with input N2 being shared by the two OR gates. The outputs of the
 OR gates are fed into the AND gate. The AND gate has an output N6. Thus,
 the output of the AND gate can be represented by the boolean function
 N6=(N1 OR N2) AND (N2 OR N3).
 A BDD for this circuit is shown in FIG. 2. The BDD is composed of vertices,
 which may also be called nodes, and branches. Vertices from which no
 further branches extend are termed terminal vertices. The BDD is an
 Ordered BDD (OBDD) as each input is restricted to appearing only at one
 level of the BDD. The BDD may be reduced to a Reduced OBDD (ROBDD) as
 shown in FIG. 3. The rules for reducing OBDDs are known in the art. These
 rules include eliminating redundant or isomorphic nodes, and by
 recognizing that some nodes can be eliminated by exchanging the branches
 of a node with a node or its complement. The importance of ROBDDs is that
 ROBDDs are unique, i.e., canonical. Thus, if two OBDDs reduce to the same
 ROBDD, the circuits represented by the OBDDs are equivalent.
 In most applications, ROBDDs are constructed using some variant of the
 Apply procedure described in R. E. Bryant, Graph-Based Algorithms For
 Boolean Function Manipulation, IEEE Trans. Computer C-35(8): 667-691,
 August 1986, incorporated by reference herein. Using the Apply procedure
 the ROBDD for a gate g is synthesized by the symbolic manipulation of the
 ROBDDs of gate g's inputs. Given a circuit, the gates of the circuit are
 processed in a depth-first manner until the ROBDDs of the desired output
 gates are constructed.
 A large number of problems in VLSI-CAD and other areas of computer science
 can be formulated in terms of Boolean functions. Accordingly, ROBDDs are
 useful for performing equivalence checks. A central issue, however, in
 providing computer aided solutions and equivalence checking is to find a
 compact representation for the Boolean functions so that the equivalence
 check can be efficiently performed. ROBDDs are efficiently manipulable,
 and as previously stated, are canonical. In many practical functions
 ROBDDs are compact as well, both in terms of size (memory space) and
 computational time. Accordingly, ROBDDs are frequently used as the Boolean
 representation of choice to solve various CAD problems.
 ROBDDs, however, are not always compact. In a large number of cases of
 practical interest, many ROBDDs representing a circuit or system described
 by a Boolean function may require space which is exponential in the number
 of primary inputs (PIs) to the circuit or system. This makes solving for
 equivalence an NP-hard problem. The large space requirement, either in
 terms of memory or computational time, places limits on the complexity of
 problems which can be solved using ROBDDs.
 Various methods have been proposed to improve the compactness of ROBDDs.
 Some of these methods improve compactness, but do not maintain canonicity
 and manipulability of the ROBDDs. Such methods reduce the applicability of
 the use of ROBDDs. Other methods, which maintain canonicity and
 manipulability, represent the function over the entire Boolean space as a
 single graph rooted at an unique source. A requirement of a single graph,
 however, may still result in ROBDDs of such a size that either memory or
 time constraints are exceeded.
 Methods of reducing the size of ROBDDs have been proposed. The size of an
 ROBDD is strongly dependent on its ordering of variables. Therefore, many
 algorithms have been proposed to determine variable orders which reduce
 the size of ROBDDs. For some Boolean functions, however, it is possible
 that no variable order results in a ROBDD sufficiently small to be useful,
 or that no such variable order can be efficiently found.
 The space and time requirements of ROBDDs may also be reduced by relaxing
 the total ordering requirement. A Free BDD is an example of such an
 approach. A Free BDD (FBDD) is a BDD in which variables can appear only
 once in a given path from the source to the terminal, but different paths
 can have different variable orderings.
 Another approach to obtain a more compact representation for Boolean
 functions is to change the function decomposition associated with the
 nodes. Generally, a BDD decomposition is based on the Shannon Expansion in
 which a function .function. is expressed as x.function..sub.x
 +x.function..sub.x, or methods derived from the Shannon expansion such as
 the Apply method. Some other decompositions include the Reed-Muller
 expansion, or the use of expansion hybrids such as Functional Decision
 Diagrams (FDDs), or through the use of Ordered Kronecker Functional
 Decision Diagrams (OKFDDs). All of these methods, however, represent a
 function over the entire Boolean space as a single graph rooted at a
 unique source. Thus, these methods still face problems of memory and time
 constraints.
 Furthermore, many designs, particularly for sequential circuits, are not
 adequately verified. Usually a test-suite is prepared to test such
 designs. The test-suite includes a number of test cases in which the
 design is subjected to varying combinations of assignments for the primary
 inputs of the design. A single combination of assignments for the primary
 inputs forms an input vector. A sequence of input vectors, used to test
 designs having sequential elements such as flip-flops, forms a test
 vector.
 Test-suites are often prepared by engineers with specialized knowledge of
 the design being tested. Therefore test-suites are useful test devices.
 However, test-suites only test a very small portion of a state or Boolean
 space of the design. For designs with an appreciable number of primary
 inputs or possible test vectors, test-suites do not test a substantial
 portion of input vectors or test vectors of particular interest.
 SUMMARY OF THE INVENTION
 The present invention provides a method and system for evaluating digital
 circuits and systems that are otherwise unverifiable through the use of
 BDD-based verification techniques using windows of Boolean space
 representations of the digital circuits and systems. In a preferred
 embodiment, the digital circuit or system is represented as a Boolean
 function forming a Boolean space. The Boolean space is partitioned into
 partitions, which may be recursively partitioned into still further
 partitions. Partitions which are otherwise too large for the formation of
 a BDD are expressed in terms of a decomposed partition string having
 components or elements combinable to form the partition. These components
 or elements are combined in a scheduled order. If any of the combinations
 result in zero then the decomposed partition string also results in zero.
 Thus, combining all of the components or elements is unnecessary if any
 sub-combination results in zero, thereby allowing evaluation of the
 partition represented by the decomposed partition string.
 Accordingly, the present invention provides a method and system of
 verifying the equivalence of first and second circuits. The first and
 second circuits have corresponding sets of primary inputs and primary
 outputs. The first and second circuits are represented as Boolean
 functions and a Boolean space is represented by exclusive ORing the
 corresponding outputs of the Boolean functions. In building a decomposed
 Binary Decision Diagram for the Boolean space the Boolean space is
 partitioned during composition of a decomposition point when the Binary
 Decision Diagram resulting from composition exceeds a predetermined
 constraint on computer memory usage. The circuits can then be determined
 to be equivalent if all of the resulting partitions are zero.
 Moreover, the present invention provides a sampling method for use in the
 partial verification of otherwise unverifiable circuits, systems, and
 designs thereof. The state space of the circuit, system, or design is
 partitioned into multiple partitions. These partitions are formed through
 any of several methods, including methods that analyze test-suites for the
 circuit, system, or design. Additionally, if an intermediate BDD exceeds
 predefined constraints on memory usage the BDD can be replaced with a zero
 terminal vertice and other partitions of the state space evaluated.
 These and other features of the present invention will be more readily
 appreciated as the same becomes better understood by reference to the
 following detailed description when considered in connection with the
 accompanying drawings.

DETAILED DESCRIPTION OF THE INVENTION
 I. Overview
 The present invention comprises a method and system of circuit or system
 verification wherein partitioning a Boolean logic space representing the
 circuit or system is performed by composing at decomposition points. Each
 composition partitions the Boolean space into two separate partitions.
 Composition is performed through use of Shannon's equation and a
 functional restriction on the BDDs. Thus, each partition represents a
 disjoint part of Boolean space.
 In determining if a first circuit is equivalent to a second circuit each
 primary output of the two circuits are combined in an exclusive OR (XOR)
 operation. If the outputs of all of the XOR operations are always equal to
 zero, then the two circuits are equivalent. Accordingly, the entire
 Boolean space therefore comprises a representation F of a first circuit
 and a representation G of a second circuit, the primary outputs of which
 are combined in an XOR operation. Thus, for circuits represented by F and
 G to be equivalent, the Boolean space of F XOR G must always be zero. If
 the Boolean space of F XOR G is partitioned into any number of disjoint
 partitions, each of those partitions must also be equal to zero for the
 entire Boolean space of F XOR G to be zero. Thus, OBDDs may be built for
 each of the separate partitions, and each of the OBDDs can be checked to
 determine if the OBDDs reduce to zero, i.e., only have a single terminal
 vertex equal to zero. If all of the partitions reduce to zero, then F XOR
 G reduces to zero, and F and G represent equivalent circuits.
 Alternatively, the representations F and G may be manipulated separately,
 and resulting ROBDDs subsequently compared.
 The use of partitioned ROBDDs means that only one ROBDD, which represents
 less than all of the Boolean space, is required to be located in memory at
 any given time. As each partitioned ROBDD is smaller than any monolithic
 ROBDD, additional classes of problems which are otherwise unsolvable due
 to time and memory space constraints are now solvable. Additionally, as
 each partitioned ROBDD must reduce to zero for the circuits to be
 equivalent, processing may stop as soon as a partitioned ROBDD is found
 that does not reduce to zero, thereby saving additional processing time.
 Moreover, the variable ordering of each ROBDD can be different, thus
 further reducing the size of individual ROBDDs.
 Partitions are formed by composing decomposition points. Decomposition
 points are found in a number of ways. If a point is a known equivalent
 point, a partition is formed at the decomposition point using the
 equivalent OBDD.
 Decomposition points are also determined based on explosion principles.
 Monolithic OBDD's are generally built from the primary inputs towards the
 primary outputs using the Apply procedure. This is done until a monolithic
 OBDD which expresses the primary outputs in terms of the primary inputs is
 constructed. If during this process an OBDD about a node explodes in terms
 of memory usage, then that point is marked as a decomposition point, and
 the point is turned into a pseudo-variable. In building OBDD's closer to
 the primary outputs the pseudo-variable is used in place of the OBDD that
 would otherwise be used. A BDD utilizing a pseudo-variable b is
 illustrated in FIG. 9.
 A procedure for determining decomposition points in the context of building
 a decomposed BDD for a circuit representation having n gates or nodes is
 illustrated in FIG. 13. In Step 130 a counter is set to the first primary
 input. Step 131 determines if BDDs have been attempted to be built for all
 gates or nodes. Step 132 builds intermediate BDDs for each gate or node
 until a BDD blow-up in terms of size occurs. If such a blow-up occurs,
 Step 134 marks the gate or node as a decomposition point and Step 135
 inserts a pseudo-variable for the BDD for the gate or node marked as a
 decomposition point.
 Such a procedure provides at least two benefits. The necessity for building
 a BDD about the node may disappear. That is, the intermediate BDD which
 explodes in memory may not be necessary due to later operations. As an
 example, a simple circuit which has intermediate BDD's greater in size
 than the final BDD is shown in FIG. 4. The simple circuit comprises an OR
 gate 31 and an AND gate 33. The OR gate has inputs N10 and N11. The output
 N12 of the OR gate is fed to the AND gate, whose other input is N11. The
 output of the AND gate is N13. The BDD for N10 is shown in FIG. 5, and
 comprises a node N12 with two branches each to a terminal vertex. The BDD
 for N11 is similar, and is shown in FIG. 6. The BDD for N12 is shown in
 FIG. 7, and comprises 2 nodes. Yet the BDD for N13 has only 1 node, as
 shown in FIG. 8, as can be seen when it is understood that N13=(N10 or
 N11) AND N11, which is simply N13=N11. Thus, the final BDD for the circuit
 is smaller than at least one of the intermediate BDDs, and building the
 intermediate BDD is not necessary.
 Nevertheless, a canonical and easy to analyze representation for the target
 function (for example, the output functions) must still be built. To avoid
 a BDD explosion in this case, the BDD can be partitioned during
 composition of the decomposition points. Thus, FIGS. 10 and 11 illustrate
 the two partitions resulting from composing pseudo-variable b of the BDD
 of FIG. 9. Because such a partitioned BDD is of a smaller size than a BDD
 which is the sum of the partitions, a reduced amount of memory or time is
 required.
 FIG. 12 provides an overview of a method of circuit verification for a
 circuit 1 and a circuit 2 using a partitioning technique. In the overview
 C represents a combination of circuits 1 and 2 and F is a Boolean function
 representing circuit C. In Step 120 a decomposition in C for decomposition
 sets from the primary inputs to the primary outputs is formed. In Step 122
 the function F is represented by a combination of primary inputs and
 pseudo-variables. In Step 124 the representation of function F is composed
 and partitioned into Partitioned OBDDs. Step 126 determines if any of the
 resulting OBDDs are not equal to zero. If any of the resulting OBDDs are
 not equal to zero, then Step 127 declares circuit 1 and circuit 2 not
 equivalent. Otherwise, Step 128 declares circuit 1 and circuit 2
 equivalent.
 OBDDs are generated for each partition. If a partition contains another
 decomposition point further partitioning may need to be performed. Each
 partition may itself be partitioned into two disjoint Boolean spaces, and
 each subpartition may be further partitioned into disjoint Boolean spaces.
 Thus, the Boolean space may be partitioned into a large number of OBDDs,
 each of which are small.
 Some partitions may remain too large for BDD building. The partitions,
 however, are formed of a decomposed partition string. The decomposed
 partition string is a string of components, or elements, ANDed together.
 If a particular partition is formed as a result of recursively
 partitioning a number of higher level partitions this string may include a
 number of components. If any of the components are ANDed together with the
 result being zero, then the string, and thus the partition, must also be
 zero.
 Accordingly, the order of building a decomposed partition string is
 accomplished using a scheduling order. For instance, consider the problem
 of constructing the partitioned ROBDD of f, where f=a,b,c,d,e and
 a,b,c,d,e are all Boolean functions representative of some portion of a
 system or circuit topology. In a preferred embodiment a,b,c,d, and e are
 ranked both by their size (expressed in terms of number of nodes) and by
 the extent to which they each have a minimum of extra support with respect
 to each other. This ranking determines the schedule by which the
 components are combined, with component of minimum size and extra support
 combined first. The foregoing, as well as additional details, is more
 completely described in the following.
 II. Partitioned-ROBDDs
 A. Definition
 Assume there is a Boolean function f: B.sup.n.fwdarw.B, defined over n
 inputs X.sub.n ={x.sub.1, . . . , x.sub.n }. The partitioned-ROBDD
 representation, X.sub.f, of f is defined as follows:
 Definition 1. Given a Boolean function f:B.sup.n.fwdarw.B, defined over
 X.sub.n, a partitioned-ROBDD representation X.sub.f of f is a set of k
 function pairs, X.sub.f ={(w.sub.1, f.sub.1) . . . , (w.sub.k, f.sub.k)}
 where, w.sub.i : B.sup.n.fwdarw.B and .function..sub.i :B.sup.n.fwdarw.B,
 for 1.ltoreq.i.ltoreq.k, are also defined over X.sub.n and satisfy the
 following conditions:
 1. w.sub.i and .function..sub.i are represented as ROBDDs with the variable
 ordering .pi..sub.i, for 1.ltoreq.i.ltoreq.k.
 2. w.sub.1 +w.sub.2 + . . . +w.sub.k =1
 3. .function..sub.i =w.sub.i {character pullout}.function., for
 1.ltoreq.i.ltoreq.k
 Here, + an {character pullout} represent Boolean OR and AND respectively.
 The set {w.sub.1, . . . , w.sub.k } is denoted by W. Each w.sub.i is
 called a window function. Intuitively, a window function w.sub.i
 represents a part of the Boolean space over which f is defined. Every pair
 (w.sub.i, .function..sub.i) represents a partition of the function f. Here
 the term "partition" is not being used in the conventional sense where
 partitions have to be disjoint. If in addition to Conditions 1-3 in
 Definition 1, w.sub.i {character pullout}w.sub.j =0 for i.noteq.j then the
 partitions are orthogonal; and each (w.sub.i, .function..sub.i) is now a
 partition in the conventional sense.
 Condition 1 in Definition 1 states that each partition has an associated
 variable ordering which may or may not be different from the variable
 orderings of other partitions. Condition 2 states that the w.sub.i s cover
 the entire Boolean space. Condition 3 states that .function..sub.i is the
 same as f over the Boolean space covered by w.sub.i. In general, each
 .function..sub.i can be represented as w.sub.i {character pullout}f.sub.i
 ; the value of f.sub.i is a do not care for the part of the Boolean space
 not covered by w.sub.i. The size of an ROBDD F is denoted by
 .vertline.F.vertline.. Thus the sum of the sizes of all partitions,
 denoted by .vertline.X.sub.f.vertline., is given by
 .vertline.X.sub.f.vertline.=(.vertline..function..sub.1.vertline.+ . . .
 .vertline..function..sub.k.vertline.+.vertline.w.sub.1.vertline.+ . . .
 +.vertline.w.sub.k.vertline.). From Conditions 2 and 3, it immediately
 follows that:
EQU .function.=.function..sub.1 +.function..sub.2 + . . . =.function..sub.k
 (1)
 This type of partitioning in which f is expressed as a disjunction of
 .function..sub.i s is called a disjunctive partition. A conjunctive
 partition can be defined as the dual of the above definition. That is, the
 i.sup.th partition is given by (w.sub.i, .function..sub.1), Condition 2 in
 Definition 1 becomes w.sub.1 {character pullout} . . . {character
 pullout}w.sub.k =0, and Condition 3 becomes .function..sub.i =w.sub.i
 +.function.. In this case .function.=(.function..sub.1 {character pullout}
 . . . {character pullout}.function..sub.k).
 B. Canonicity of Partitioned-ROBDDs
 For a given set W={w.sub.1, . . . , w.sub.k } and a given ordering
 .pi..sub.i for every partition i, the partitioned-ROBDD representation is
 canonical. For a given function f and a given partitioned-ROBDD
 representation X.sub.f ={(w.sub.i,
 .function..sub.i).vertline.1.ltoreq.i.ltoreq.k} of f, .function..sub.i is
 unique. Since each .function..sub.i is represented as an ROBDD which is
 canonical (for a given ordering .pi..sub.i), the partitioned-ROBDD
 representation is canonical.
 Given a partition of the Boolean space, W={w.sub.1, . . . , w.sub.k }, the
 asymptotic complexity of performing basic Boolean operations (e.g. NOT,
 AND, OR) on the partitioned-ROBDD representations is polynomial in the
 sizes of the operands; the same as ROBDDs. Therefore, the compactness of
 representation does not cost anything in terms of the efficiency of
 manipulation. In fact, since partitioned-ROBDDs are in general smaller
 than monolithic ROBDDs and each partition can be manipulated
 independently, their manipulation is also more efficient.
 As discussed in A. Narayan et al., Partitioned-ROBDDs--A Compact, Canonical
 and Efficiently Manipulable Representation of Boolean Functions, ICCAD,
 November 1996, incorporated herein by reference, let f and g be two
 Boolean functions and let X.sub.f ={(w.sub.i,
 .function..sub.i).vertline.1.ltoreq.i.ltoreq.k} and X.sub.g ={(w.sub.i,
 g.sub.i).vertline.1.ltoreq.i.ltoreq.k} be their respective
 partitioned-ROBDDs satisfying Conditions 1-3 in Definition 1. Further
 assume that the i.sup.th partitions in both X.sub.f and X.sub.g have the
 same variable ordering .pi..sub.i. Then, (a) X.sub..function. ={(w.sub.i,
 w.sub.i {character pullout}.function..sub.i).vertline.1.ltoreq.i.ltoreq.k}
 is the partitioned-ROBDD representing f (i.e. NOT of f); and, (b) X.sub.f
 {character pullout}g={(w.sub.i, w.sub.i {character pullout}(f.sub.i
 {character pullout}g.sub.i)).vertline.1.ltoreq.i.ltoreq.k} is the
 partitioned-ROBDD representation of f{character pullout}g, where
 {character pullout} represents any binary operation between f and g.
 C. Complexity of Operations
 Given two ROBDDs F and G, the operation F{character pullout}G can be
 performed in .omicron.(.vertline.F.parallel.G.vertline.) space and time.
 In partitioned-ROBDDs, different partitions are manipulated independently
 and the worst case time complexity of f{character pullout}g is
 ##EQU1##
 which is O(.vertline.X.sub.f.parallel.X.sub.g.vertline.) Since only one
 partition needs to be in the memory at any time, the worst case space
 complexity is given by max
 (.vertline.f.sub.i.parallel.g.sub.i.vertline.)which is in general
 &lt;&lt;.vertline.X.sub.f.parallel.X.sub.g.vertline.. Also similar to ROBDDs,
 the size of the satisfying set of a function f can be computed in
 O(.vertline.X.sub.f.vertline.) for orthogonally partitioned-ROBDDs.
 D. Existential Quantification
 Besides the basic Boolean operations, another useful operation which is
 extensively used in formal verification of sequential circuits is the
 existential quantification (.E-backward..sub.x f) operation. The
 existential quantification of variable x from the function
 f(.E-backward..sub.x f) is given by .E-backward..sub.x f=f.sub.x +f.sub.x
 where f.sub.x and f.sub.x are the positive and negative cofactors of
 respectively. In the partitioned-ROBDD representation, the cofactors can
 be obtained easily by cofactoring each w.sub.i and .function..sub.i with
 respect to X, i.e., X.sub.f.sub..sub.x =(w.sub.i.sub..sub.x ,
 .function..sub.i.sub..sub.x ).vertline.1.ltoreq.i.ltoreq.k, and (w.sub.i,
 .function..sub.i).di-elect cons.X.sub.f } and X.sub.f.sub..sub.x
 =(w.sub.i.sub..sub.x , .function..sub.i.sub..sub.x
 ).vertline.1.ltoreq.i.ltoreq.k, and (w.sub.i, .function..sub.i).di-elect
 cons.X.sub.f }. But after performing the cofactoring operation, the
 positive and negative cofactors have different window functions (given by
 w.sub.i and w.sub.i respectively) and the disjunction cannot be performed
 directly on the partitions. This problem does not arise if we choose
 window functions which do not depend on the variables that have to be
 quantified. Existential quantification can be done as follows: Let X.sub.f
 ={(w.sub.i,f.sub.i).vertline.1.ltoreq.i.ltoreq.k} be a partitioned-ROBDD
 representation of, f such that .E-backward..sub.x w.sub.i =w.sub.i, for
 1.ltoreq.i.ltoreq.k. Then X.E-backward..sub.xf ={(w.sub.i,
 .E-backward..sub.x f.sub.i).vertline.1.ltoreq.i.ltoreq.k is the
 partitioned-ROBDD representation of .E-backward..sub.x f.
 Another important operation that is frequently used is the universal
 quantification of X from (denoted by .A-inverted.xf). A sufficient
 condition for universal quantification is that the window functions are
 orthogonal in addition to being independent of the variables to be
 quantified. Universal quantification can be done as follows: Let X.sub.f
 ={(w.sub.i, f.sub.i).vertline.1.ltoreq.i.ltoreq.k} be a partitioned ROBDD
 representation of such that .A-inverted.xw.sub.i =w.sub.i and w.sub.i
 {character pullout}w.sub.j =0 for 1.ltoreq.i, j.ltoreq.k and i.noteq.j.
 Then .chi..A-inverted.xf={(w.sub.i,
 .A-inverted.xf.sub.i)/1.ltoreq.i.ltoreq.k} is the partitioned-ROBDD
 representation of .A-inverted.xf.
 III. Heuristics for Constructing Partitioned-ROBDDs
 The performance of partitioned-ROBDDs depends critically on the generation
 of partitions of the Boolean space over which the function can be
 compactly represented. The issue of finding such partitions of the Boolean
 space is as central to the partitioned-ROBDD representation as the issue
 of finding good variable orderings is to monolithic ROBDDs. Some simple
 heuristics which are effective in generating compact orthogonally
 partitioned-ROBDDs are discussed below. Although a Boolean netlist model
 is used in the following discussion, the techniques are general and can be
 applied to any arbitrary sequence of Boolean operations.
 A given function F is first decomposed and the window functions for
 creating F's partitioned-ROBDD are obtained by analyzing the decomposed
 BDD for F. The number of windows is decided either a priori or
 dynamically. After a window w.sub.i is decided, a partitioned-ROBDD
 corresponding to it is obtained by composing F in the Boolean space
 corresponding to the window w.sub.1.
 A. Creating a Decomposed Representation
 Given a circuit representing a Boolean function
 .function.:B.sup.n.fwdarw.B, defined over X.sub.n ={x.sub.1 . . . x.sub.n
 }, the decomposition strategy consists of introducing new variables based
 on the increase in the ROBDD size during a sequence of ROBDD operations. A
 new variable is introduced whenever the total number of nodes in a ROBDD
 manager increases by a disproportionate measure due to some operation. For
 example, if R has become very large while performing the operation
 R=R.sub.1 +R.sub.2 on ROBDDs R.sub.1 and R.sub.2, the operation is undone.
 Instead, new variables .PSI..sub.1 and .PSI..sub.2 are introduced and R is
 expressed as .PSI..sub.1 +.PSI..sub.2. A separate array is maintained
 which contains the ROBDDs corresponding to the decomposition points.
 R.sub.1 and R.sub.2 corresponding to the .PSI..sub.1 and .psi..sub.2 are
 added to this array. In this way the instances of difficult functional
 manipulations are postponed to a later stage. Due to Boolean
 simplification many of these cases may never occur in the final result,
 especially if the final memory requirement is much less than the peak
 intermediate requirement as stated in J. Jain et al. Decomposition
 Techniques for Efficient ROBDD Construction, LNCS, Formal Methods in CAD
 96, Springer-Verlag, November, 1996, incorporated by reference herein.
 In a preferred embodiment, the check for memory explosion is done only if
 the manager size is larger than a predetermined threshold. Also,
 decomposition points are added when the ROBDD grows beyond another
 threshold value. This ensures that the decomposition points themselves do
 not have very large ROBDDs. Even a simple size-based decomposition scheme
 works quite effectively for demonstrating the potential of
 partitioned-OBDDs.
 At the end of the decomposition phase a decomposed representation is
 obtained. The decomposed representation is f.sub.d (.PSI.,X), of
 .function. where .psi.={.psi..sub.1, . . . , .psi..sub.k } is called a
 decomposition set of the circuit and each .psi..sub.i.epsilon..PSI. is a
 decomposition point. Let .PSI..sub.bdd ={.psi..sup.1bdd, . . . ,
 .psi..sub.kbdd } represent the array containing the ROBDDs of the
 decomposition points, i.e., each .psi..sub.i.epsilon..PSI. has a
 corresponding ROBDD, .psi..sub.1bdd, .epsilon..psi..sub.bdd, in terms of
 primary input variables as well as (possibly) other
 .psi..sub.j.epsilon..PSI., where .psi..sub.j.noteq..PSI..sub.i. Similarly,
 the array of .psi..sub.ibddw is represented by .PSI..sub.bddwi. The
 composition of .psi..sub.i in f.sub.d (.PSI.,X) is denoted by f.sub.d
 (.PSI.,X).multidot.(.psi..sub.i.rarw..psi..sub.ibdd) where,
EQU f.sub.d
 (.PSI.,X).multidot.(.psi..sub.i.rarw..psi..sub.ibdd)=.psi..sub.
 ibdd.multidot..function..sub.d
 +.psi..sub.ibdd.multidot..function..sub.d.psi.i [4]
 The vector composition of the .PSI. in f.sub.d (.PSI.,X) is denoted as
 f.sub.d (.PSI.;X).multidot.(.PSI..rarw..PSI..sub.bdd) and represents
 successive composition of .psi..sub.i 's into f.sub.d.
 B. Partitioning a Decomposed Representation.
 1. Creating .function., for a given w.sub.i
 Given a window function w.sub.i, a decomposed representation
 .function..sub.d (.psi.,X), and the ROBDD array .psi..sub.bdd of
 .function., a .function..sub.i is desired, such that the ROBDD
 representing .function..sub.1 =w.sub.1 {character pullout}.function..sub.i
 is smaller than .function.. The following observation is pertinent:
 Observation 1: Let .function..sub.i =.function..sub.dwi
 (.psi.,X)(.psi..rarw..PSI..sub.bdd,) and .function.=.function..sub.d
 (.psi.,X)(.psi..rarw..PSI..sub.bdd). If w.sub.i is a cube on PIs then
 .vertline..function..sub.i.vertline..ltoreq..vertline..function..vertline.
 for any given variable order for f and .function..
 Proof: We are given .function..sub.i =.function..sub.d.sub..sub.w
 .sub..sub.i (.PSI.,X)(.PSI..rarw..PSI..sub.bdd.sub..sub.w .sub..sub.i .
 If w.sub.i depends only on PIs, then the order of cofactoring and
 composition can be changed. Hence, .function..sub.i =[.function..sub.d
 (.PSI.,X)(.PSI..rarw..PSI..sub.bdd)].sub.w.sub..sub.i . This gives,
 .function..sub.i =.function..sub.w.sub..sub.i . If w.sub.i is a cube, then
 .vertline..function..sub.w.sub..sub.i
 .vertline..ltoreq..vertline..function..vertline. and hence
 .vertline..function..sub.
 i.vertline..ltoreq..vertline..function..vertline.. Now, given
 .function..sub.d.sub..sub.i .PSI..sub.bdd and w.sub.i s.sub.i, the
 cofactors .PSI..sub.w.sub..sub.i and .function..sub.w.sub..sub.i . By
 composing .PSI..sub.bdd.sub..sub.w .sub..sub.i in
 .function..sub.d.sub..sub.w .sub..sub.i , in .function..sub.d.sub..sub.w
 .sub..sub.i , the partition function can be created, .function..sub.i
 =.function..sub.w.sub..sub.i is formed. So given a set of window
 functions w.sub.i, the partitioned-ROBDD .sub..chi..function. of f is
 given by X.function.={(w.sub.i, w.sub.i {character
 pullout}.function..sub.w.sub..sub.i ).vertline.1.ltoreq.i.ltoreq.k}. It is
 easy to check that the above definition satisfies all the conditions of
 Definition 1. If w.sub.i is a cube, f.sub.i is guaranteed to have smaller
 size than the ROBDD for f. Also, the ROBDD representing w.sub.i has k
 internal nodes where k is the number of literals in w.sub.i. Since w.sub.i
 and .function..sub.w.sub..sub.i have disjoint support,
 .vertline.f.sub.i.vertline.=.vertline.w.sub.i {character
 pullout}f.sub.i.vertline.=(k+.vertline.f.sub.
 i.vertline.).apprxeq..vertline.f.sub.i.vertline.. Also, as each
 intermediate result of building f.sub.i will be smaller than that of
 building f, the intermediate peak memory requirement is also reduced.
 Note that observation 1 does not hold in the presence of dynamic variable
 reordering when f and f.sub.i can have different variable orderings.
 However, in practice since dynamic variable reordering is working on
 smaller graphs in the case of partitioning it is perhaps even more
 effective. Even when the window function is a more complex function of PIs
 than a cube, .function..sub.i =.function..sub.w.sub..sub.i is used. Here
 .function..sub.w.sub..sub.i is the generalized cofactor of .function. on
 w.sub.i. The generalized cofactor of .function. on w.sub.i is generally
 much smaller than .function.. But in this case the size of the i.sup.th
 partitioned-ROBDD .vertline..function..sub.i can be
 .omicron.(.vertline.w.sub.i.parallel..function..sub.i.vertline. in the
 worst case. To avoid this, use w.sub.i s which are small while using
 general window functions.
 2. Selection of Window Functions
 Methods to obtain good window functions can be divided into two categories:
 a priori selection and "explosion" based selection.
 a. A Priori Partitioning
 A priori partitioning uses a predetermined number of PIs to partition.
 Thus, if partitioning is done on `k` PIs then 2.sub.k partitions are
 created corresponding to all the binary assignments of these variables.
 For example, if partitioning is done on x.sub.1 and x.sub.2 then four
 partitions x.sub.1 x.sub.2, x.sub.1 x.sub.2, x.sub.1 x.sub.2 and x.sub.1
 x.sub.2 are created. These partitioned-ROBDDs are guaranteed to be smaller
 than the monolithic ROBDD. Memory requirements are always lower because
 only-one partition needs to be in the memory at a given time, this
 reduction in memory is large, and is accompanied by an overall reduction
 in the time taken to process all partitions as well.
 In selecting variables for partitioning, it is desirable to select those
 variables which maximize the partitioning achieved while minimizing the
 redundancy that may arise in creating different partitions independently.
 The cost of partitioning a function .function. on variable x is defined as
EQU cost.sub.x (.function.)=.alpha.[p.sub.x (.function.)]+.beta.[r.sub.x
 (.function.)]
 where p.sub.x (.function.) represents the partitioning factor and is given
 by,
 ##EQU2##
 and r.sub.x (.function.) represents the redundancy factor and is given by
 ##EQU3##
 A lower partitioning factor is good as it implies that the worst of the two
 partitions is small. Similarly, a lower redundancy factor is good since it
 implies that the total work involved in creating the two partitions is
 less. The variable x which has the lower overall cost is chosen for
 partitioning. For a given vector of functions F and a variable x, the cost
 of partitioning is defined as:
 ##EQU4##
 The PIs are ordered in increasing order of their cost of partitioning
 .function..sub.d and .PSI.. The best `k` PIs are selected, with `k` a
 predetermined number specified by the user. A similar cost function allows
 selection of not only PI variables, but also pseudo-variables, such as a
 .psi..sub.i.sub..sub.bdd expressed in terms of PIs, to create
 partitioned-ROBDDs. In this case, the cofactor operations become
 generalized cofactor operations for window functions which are non-cubes.
 This type of selection, where all the PIs are ranked according to their
 cost of partitioning .function..sub.d and .PSI., is called a static
 partition selection.
 A dynamic partitioning strategy is one in which the best PI (say x) is
 selected based on .function..sub.d and .PSI. and then the subsequent PIs
 are recursively selected based on .function..sub.d and .PSI. in one
 partition and in .function..sub.d.sub..sub.x and .PSI..sub.x in the other
 partition. Dynamic partitioning requires an exponential number of
 cofactors and can be expensive. This cost can be somewhat reduced by
 exploiting the fact that the only values that of interest are the sizes of
 the cofactors of .function..sub.d and .psi..sub.i.sub..sub.bdd S. An
 upper bound on the value of .vertline..function..sub.d.sub..sub.x
 .vertline. traversing the ROBDD of .function..sub.d and taking the x=1
 branch whenever the node with variable id corresponding to x is
 encountered. This method doesn't give the exact count as the BDD obtained
 by traversing the ROBDD in this manner is not reduced. The advantage is
 that no new nodes need to be created and the traversal is fast.
 b. Explosion Based Partitioning
 In this method the .psi..sub.i.sub..sub.bdd S in .function..sub.d are
 successively composed. If the graph size increases drastically for some
 composition (say .psi..sub.j), a window function w is selected based on
 the current .function..sub.d and .psi..sub.j.sub..sub.bdd . (The window
 functions are either a PI and its complement or some
 .psi..sub.k.sub..sub.bdd and its complement which is expressed in terms
 of PIs only and has a very small size.) Once the window function w is
 obtained two partitions (w{character pullout}.function..sub.d.sub..sub.w ,
 .PSI..sub.w) and(w{character pullout}.function..sub.d.sub..sub.w ,
 .PSI..sub.w) are created. The explosion based partitioning routine is
 recursively called on each of these the partitions.
 Consider two circuits A and B for which an equivalence check is desired.
 The circuits A and B have corresponding primary outputs F.sub.i and
 F.sub.2. To show equivalence F=F.sub.1.crclbar.F.sub.2 =0 must be true. To
 determine whether this is true a BDD is built for F using cutsets of
 internal equivalent points. In this process many outputs can be declared
 equivalent simply by building their BDDs in terms of the nearest cutset
 .mu..sub.i ={.psi..sub.1, . . . , .psi..sub.k }, of equivalent gates. This
 process can be very efficient when the output BDD for F can be easily
 built using .mu..sub.i, and the output BDD reduces to Boolean 0. This
 means that F.sub.1, F.sub.2 are functionally equivalent. However,
 sometimes the BDD F(.mu..sub.1) is very large and thus cannot be
 constructed. F(.mu..sub.1) also may not reduce to 0, in which case the BDD
 must be composed in terms of another cutset .mu..sub.j, where .mu..sub.j
 is a cutset falling between primary inputs and the previous cutset
 .mu..sub.i. During this composition process, the BDD can again blow up
 before the equivalences of F.sub.1, F.sub.2 can be resolved. The BDD
 partitioning strategy essentially takes advantage of the above scenarios
 which are highly important ones since the normal methods fail for these
 cases.
 The BDD partitioning strategy is, in part, to compose F(.mu..sub.i) to
 F(.mu..sub.j) and, if the graph size increases drastically for some
 composition (say of the BDD corresponding to gate .psi..sub.j), to
 partition when the composition result exceeds some limit. To select this
 limit, knowledge of several size related parameters is maintained during
 the process of composition of BDD F(.mu..sub.i) to F(.mu..sub.j). To
 explain these parameters, consider that h number of BDDs have already been
 composed, where 1.ltoreq.h.ltoreq.k from the set {.psi., . . . ,
 .psi..sub.k }. As an example, assume that the order in which the BDDs are
 composed is according to the increasing index of the .psi. variables.
 (That is, BDDs are composed in the order .psi..sub.1, .psi..sub.2, . . . ,
 .psi..sub.h.) The BDD of .psi. made in terms of cutset .psi..sub.i is
 written as .psi..sub.i (.mu..sub.j). A routine, DYNAMIC_BDD_TITION, to
 dynamically determine when to partition a BDD makes use of the following:
 Procedure: DYNAMIC_BDD_TITION
 1. ORIG_SIZE is the original BDD size of F(.mu..sub.i) expressed in terms
 of cutset .mu..sub.j.
 2. COMPOSED_ARGUMENT_SIZE is the sum of each BDD .psi..sub.i (.mu..sub.j),
 .psi..sub.2 (.mu..sub.j), . . . , .psi..sub.h (.mu..sub.j) that has been
 composed in the BDD F(.mu..sub.i).
 3. TOTAL_INPUT_SIZE=COMPOSED_ARGUMENT_SIZE+ORIG_SIZE.
 4. FINAL_SIZE is the "final" size of the BDD F(.mu..sub.i) obtained after
 having successively composed each of the h points .psi..sub.1 ;
 .psi..sub.2, . . . , .psi..sub.h. This BDD is denoted as F.sub.h. Also,
 let the PREVIOUS_SIZE is the size of F(.mu..sub.i) after composing h-1
 points.
 Partitioning is invoked if
 (A) FINAL_SIZE&gt;COMPOSED ARGUMENT_SIZE*BLOW_UP_FACTOR BLOW_UP_FACTOR can be
 varied according to the space available on the given machine, but in a
 preferred embodiment is 10.
 (B) FINAL_SIZE&gt;PREVIOUS_SIZE*BLOW_UP_FACTOR/NUM In a preferred embodiment
 NUM is 2. Also in a preferred embodiment, this criteria is only used in
 determining BDD blow-ups during composition, and not while forming a
 decomposed representation.
 (C) FINAL_SIZE&gt;PRE_SET_MEMORY_LIMIT Additionally, partitioning is invoked
 if the FINAL_SIZE is greater than a preset limit on the available memory.
 A procedure for determining BDD blow-ups while forming a decomposed
 representation is illustrated in FIG. 14. In forming a decomposed
 representation, BDDs for an output of a Boolean operation gate are formed
 by performing the Boolean operation on the BDDs of the inputs to the gate.
 As illustrated in the procedure of FIG. 14, B.sub.3 is the BDD for the
 output of the gate and B.sub.1 and B.sub.2 are the BDDs for the inputs to
 the gate. Step 140 determines if the size of B.sub.3 is larger than a
 pre-set threshold limit for memory usage. Step 141 determines if the size
 of B.sub.3 is greater than a constant times the quantity the size of
 B.sub.1 plus the size of B.sub.2. If either of the conditions of Step 140
 or Step 141 are true, then an intermediate_BDD_blowup variable is set to 1
 in Step 142. Otherwise, the intermediate_BDD_blowup variable is set to 0
 in Step 143.
 3. Equivalence Point Partitioning
 The foregoing also applies to techniques based on the extraction and use of
 internal correspondences using a combinational of structural and
 functional techniques to simplify the problem of verifying the entire
 networks. These correspondences could be just functional equivalences, or
 indirect implications between their internal nodes.
 The flow of these verification methods are described in U.S. patent
 application Ser. No. 08/857,916, incorporated by reference herein. Some of
 the framework of these techniques can be approximately described as the
 following:
 1. Determining easy equivalences between internal/output gates of two given
 circuits. Equivalent gates are merged together. More precisely, a common
 pseudo-variable is introduced for both members in any equivalent
 (complemented) gate pairs.
 2. Calculating potentially equivalent nodes in the resulting circuit using
 simulation.
 3. Determining which potentially equivalent gates are truly equivalent. The
 equivalent gates between two circuits are merged.
 4. Deducing equivalences of outputs using the internal equivalences
 determined in previous steps.
 Each time two gates are merged because they are found to be equivalent
 (inverse), those gates are marked as equivalent (inverse) gates. At such
 gates a pseudo-variable is introduced during BDD construction. More
 specifically, cutsets of such gates are made as described in U.S. patent
 application Ser. No. 08/857,916 and U.S. Pat. No. 5,649,165, which is also
 incorporated by reference herein. If during simulation the number of
 potentially equivalent nodes are determined to be very few, or if during
 building any BDD a BDD blowup occurs, then additional decomposition points
 are introduced so that the BDD sizes can be kept in check. The
 decomposition points can be introduced using functional decomposition
 procedures described in J. Jain et al., Decomposition Techniques for
 Efficient ROBDD Construction, LNCS, Formal Methods in CAD 96,
 Springer-Verlag, incorporated by reference herein. Thus, the decomposition
 points include both functional decomposition points as well as the points
 which are found to be equivalent (inverse) in a given pair of circuits.
 IV. Manipulating Partitions
 A. Composition
 Once partitioning is invoked the graphs are kept decomposed as follows. The
 compose in the BDD package is done using if-then-else (ITE) operations.
 However, the last ITE (compose) operation is undone, and the last
 operation decomposed as in following. Suppose on composing .psi..sup.h
 partitioning is invoked. For brevity of symbols in the following
 discussion, BDD .psi..sub.h (.mu..sub.j) is called B.sub.h. Composition
 can be mathematically written as follows:
EQU F.sub.h =B.sub.h {character pullout}F.sub.h=1 {character pullout}B.sub.h
 {character pullout}F.sub.h=0
 B.sub.h {character pullout}F.sub.h=1 represents one partition (p.sub.1) of
 the given function F and B.sub.h {character pullout}F.sub.h=0 represents
 the other partition (p.sub.2) of the function F. Both partitions are
 functionally orthogonal. Each of these partitions can be regarded as
 independent function, and the above process of decomposition and
 partitioning is once again recursively carried out, but F(.mu..sub.i) is
 replaced with B.sub.h {character pullout}F.sub.h=1.
 If for any partition, p.sub.1 for example, BDD B.sub.h {character
 pullout}F.sub.h=1 can be computed without any blowup, then the resulting
 OBDD is created. Else p.sub.1 is represented with a symbolic conjunction
 between BDD B.sub.h and BDD F.sub.h=1. This is a decomposed partition
 string and subsequent recursive calls of DYNAMIC_BDD_TITION() work on
 this decomposed partition string. So, either the remaining k-h BDDs
 .psi..sub.h=1, . . . , .psi..sub.k in the OBDD resulting from p.sub.1 or
 its partition string are composed.
 The next time partitioning is invoked on a decomposed partition string, due
 to composition of some BDD .psi..sub.q (.mu..sub.j), a symbolic
 conjunction with the BDD of .psi..sub.q (.mu..sub.j) and the decomposed
 partition string (conjuncted Boolean expression) in which .psi..sub.q
 (.mu..sub.j) was being composed may also be required. Thus the decomposed
 partition string grows in length. At the end of the recursion along any
 branch, the resulting decomposed partition string is stored as a member of
 an array (A.sub.d) of BDDs. Each member of this array is orthogonal to
 every other member in this array.
 A symbolic conjunction between two BDDs B1, B2 is done by not carrying out
 the actual conjunction but postponing the result until some point later in
 the future. Thus, instead of making a new BDD B3 which is an actual
 conjunction between B1, B2, a symbolic_conjunction_array A.sub.1 is made.
 A.sub.1 has 3 distinct elements: BDDs B1, B2, and the conjunction
 operation. Symbolic_conjunction_array A.sub.1 clearly represents a
 function this function f(A.sub.1) is equivalent to the function resulting
 from actually carrying out the AND between B1, B2.
 Now, if we need to conjunct some BDD B4 with the function represented by
 A.sub.1 =[B1, B2, AND] we produce a result which is A.sub.2 where A.sub.2
 -[B1, B2, B4, AND]. Thus the symbolic_conjunction_array grows in length.
 A1so, suppose if G inside symbolic_conjunction_array A.sub.1 then we will
 compute the result as a symbolic conjunction array A.sub.new =[B1 (G
 composed in B1), B2 (G composed in B2), AND] where B1 (G composed in B1)
 means composing BDD G inside BDD B1.
 A flow diagram for a procedure for a decomposed partition string is
 illustrated in FIG. 16 in which a decomposed partition string .alpha.
 already exists. The decomposed partition string a includes a
 pseudo-variable g and a BDD(g). Step 160 determines if a BDD B.sub.a blows
 up when B.sub.a is equal to the symbolic conjunction of BDD(g) and
 decomposed partition string a with g equal to one. If no blow-up occurs,
 decomposed partition string .alpha..sub.a is set equal to BDD B.sub.a in
 Step 161. Otherwise, in Step 162 decomposed partition string .alpha..sub.a
 is set equal to the symbolic conjunction of BDD(g) and decomposed
 partition string a with g equal to one. Decomposed partition string
 .alpha..sub.b is similarly determined using BDD(g) and decomposed
 partition string .alpha. with g equal to zero in place of BDD(g) and
 decomposed partition string .alpha. with g equal to one, respectively, in
 Steps 163, 164, and 165.
 Note that the stored decomposed partition string is a conjunction of
 various .psi..sub.q (.mu..sub.j) with a BDD that corresponds to partially
 composed F(.mu..sub.i). If the function F is equal to Boolean 0, then each
 member of this array must also be 0. Which means that if any partition is
 composed, then it should result in Boolean 0. Each partition is a symbolic
 conjunction of BDDs. Thus any partition p.sub.r is represented as
 conjunction of m BDDs such as p.sub.i =.function..sub.1 {character
 pullout}.function..sub.2 {character pullout} . . . .function..sub.m
 {character pullout}F.sub.r. Each .function..sub.i is BDD of some
 decomposition point whose composition was causing a blowup. F.sub.r is the
 BDD left after all k BDDs have been composed.
 Once any member p.sub.i of the array A.sub.d is obtained, if the cutset
 (.mu..sub.i) does not correspond to the primary inputs, and if the answer
 to the verification problem has not been yet obtained, then
 DYNAMIC-BDD-TITION() is used and p.sub.i is composed into another
 cutset (.mu..sub.t). (.mu..sub.t) is chosen between (.mu..sub.j) and the
 primary inputs. This process is continued until every BDD in the
 decomposed-partition-string is expressed in terms of primary input
 variables.
 Thus, a process for substantially the foregoing is illustrated in FIG. 15
 in which a decomposed partition string (BDD) exists, but not in terms of
 the primary inputs. In Step 150 a composition of a decomposition point is
 performed. Step 151 checks to determine if the resulting composed BDD
 blows up. If the resulting composed BDD does not blow up and the BDD is
 not satisfiable, as determined in Steps 151 and 152, respectively, the
 process of composition is repeated for other points. If the BDD is
 satisfiable, the circuits under comparison are not equivalent. If,
 however, a BDD blow-up occurs, two decomposed partition strings are
 created in Step 153. Step 154 determines if these two decomposed partition
 strings are represented in terms of primary inputs. If so, Step 155
 examines the decomposed partition strings. If the examination determines
 that any decomposed partition string represented in terms of primary
 inputs are not equal to zero, then the systems under comparison are not
 equivalent. Otherwise, the process is repeated until either all of the
 partitions have been determined to be zero and the circuits under
 comparison are declared equivalent.
 FIG. 17 illustrates a flow diagram for a process of examining decomposed
 partition strings written in terms of primary inputs. In Step 170
 components of such a decomposed partition string are scheduled for
 combination. A number of suitable scheduling techniques are discussed
 below, and any of these may be used for scheduling the combination order
 for the components. Step 171 determines if all of the components of the
 decomposed partition string have been examined. If not, then further
 components of the decomposed partition string are combined according to
 the schedule for combination in Step 172. The result of the combination is
 checked in Step 173 to determine if the result is zero. If the result is
 zero, the partition represented by the decomposed partition string is
 declared zero in Step 174. If all components of the decomposed partition
 string have been combined and no zero result has been obtained, then the
 partition represented by the decomposed partition string is declared
 non-zero in Step 175.
 B. Equivalence Checking
 The next step is to check whether the BDD p.sub.i =.function..sub.1
 {character pullout}.function..sub.2 {character pullout} . . .
 .function..sub.m {character pullout}F.sub.r is Boolean 0. Two procedures
 may be used in making this determination.
 1. SCHEDULING_PROCEDURE(). The Scheduling_Procedure routine arranges the
 BDDs in a manner which will make computing their Boolean AND easier.
 Methods of scheduling the components f.sub.1, f.sub.2, . . . , f.sub.m for
 combination are detailed below.
 2. LEARNING_METHOD(). The decomposed partition string may be mapped to a
 circuit if the sum of size of the BDDs in decomposed-partition-string is
 not very large. The methods such as given in R. Mukherjee et al., VERIFUL:
 Verification using Functional Learning, EDAC 1995 and J. Jain et al.,
 Advanced Verification Techniques Based on Learning, DAC 1995, both of
 which are incorporated by reference, or the techniques disclosed in U.S.
 patent application Ser. No. 08/857,916 may be used to discover whether the
 Boolean function represented by this partition is 0.
 1. Scheduling Schemes
 Assume .function.=g.sub.1.circle-w/dot.g.sub.2.circle-w/dot. . . .
 .circle-w/dot.g.sub.n, where .circle-w/dot.=AND or OR. Let b.sub.i be the
 BDD corresponding to g.sub.i, and S={b.sub.1,b.sub.2, . . . , b.sub.n }.
 The goal is to compute ROBDD(.function.) by .circle-w/dot.ing BDDs in S,
 two at a time.
 All of the following scheduling schemes are greedy, in that at each step,
 they select two ROBDDs B.sub.i and B.sub.j from S such that the resulting
 BDD B(i,j)=B.sub.i.circle-w/dot.B.sub.j is small. B.sub.i and B.sub.j are
 then deleted from S and B(i,j) is added to S. This step is repeated until
 .vertline.S.vertline.=1.
 Given a pair of BDDs b.sub.i, b.sub.j, and a Boolean operation
 .circle-w/dot., it is well known that the worst-case size of the resulting
 BDD b.sub.i.circle-w/dot.b.sub.j is
 .omicron.(.vertline.b.sub.i.parallel.b.sub.j.vertline.). Accordingly, a
 size-based approach selects the two smallest BDDs b.sub.i and b.sub.j,
 with the hope that the resulting BDD will be small as well.
 Under some situations, ordering BDDs based only on sizes is not sufficient.
 It an happen that the two smallest BDDs b.sub.i and b.sub.j are such that
 .vertline.b.sub.i.circle-w/dot.b.sub.j.vertline.=.vertline.b.sub.
 i.parallel.b.sub.j.vertline.. However, if BDDs b.sub.k and b.sub.m that
 are slightly bigger but have disjoint support sets are chosen then a much
 smaller intermediate BDD may be obtained.
 The next BDD is selected so that it introduces fewest extra variables after
 the operation is carried out. In other words, the first BDD (b.sub.i) has
 minimum support and the second BDD (b.sub.j) has, among all the remaining
 BDDs, the minimum extra support from the first BDD. Extra support is the
 numbers of additional variables introduced in the support of
 b(i,j)=b.sub.i.circle-w/dot.b.sub.j as compared to (b.sub.i). It is equal
 to .vertline.sup(b.sub.j)-sup(b.sub.i).vertline., where sup(b.sub.i) is
 the support set of b.sub.i.
 Thus, the following scheduling orders, with the first BDD b.sub.i the
 minimum-sized BDD, may be used:
 1. The second BDD b.sub.j is the one that shares maximum support with
 b.sub.i
 2. The second BDD b.sub.j is the one that has minimum extra support with
 respect to b.sub.i
 3. The remaining BDDs of the set S are ranked by size and extra support in
 L.sub.size and L.sub.sup. BDDs with minimum rank (size or extra support)
 are earlier in the lists.
 Then a very small number of BDDs (such as 3) are selected from the head of
 L.sub.size and L.sub.sup. An explicit AND operation is performed on each
 of these BDDs with b.sub.i. The BDD that results in the smallest size is
 the desired b.sub.j.
 2. Order of Composition
 After selecting a window function and creating the decomposed
 representation for the i.sup.th partition given by
 .function..sub.dw.sub..sub.i and .psi..sub.wi, the final step is to
 compose .psi..sub.wi in .function..sub.dw.sub..sub.i i.e,
 .function..sub.dw.sub..sub.i
 (.psi.,X)(.psi..rarw..psi..sub.bdd.sub..sub.w .sub..sub.i ) Although the
 final ROBDD size is constant for a given variable ordering, the
 intermediate memory requirement and the time for composition is a strong
 function of the order in which the decomposition points are composed.
 For every candidate variable that can be composed into .function..sub.d,
 cost is assigned which estimates the size of the resulting composed ROBDD.
 The variable with the lowest cost estimate is composed. A simple cost
 function based on the support set size performs well in practice.
 Accordingly, the decomposition variable which leads to the smallest
 increase in the size of the support set of the ROBDD after composition is
 chosen. At each step, the candidate .psi.s for composition are restricted
 to those decomposition points which are not present in any of the other
 .psi..sub.bdd s. This guarantees that a decomposition variable needs to be
 composed only once in .function..sub.d, as explained in A. Narayan et al.,
 Study of Composition Schemes for Mixed Apply/Compose Based Construction of
 ROBDDs, Intl. Conf. on VLSI Design, January 1996, incorporated by
 reference herein.
 V. Applications
 A. Combinational .PSI.Verification
 Partitioned ROBDDs can be directly applied to check the equivalence of two
 combinational circuits. The respective outputs of two circuits .function.
 and g, are combined by an XOR gate to get a single circuit. Partitioned
 ROBDDs are then used to check whether the resulting circuit is
 satisfiable. This is simply checking whether .function..sub.i.sym.g.sub.i
 =0 for all partitions. In practice, this technique can be easily used as a
 back end to most implication based combinational verification methods
 which employ ROBDDs. Such methods are disclosed in J. Jain et al.,
 Advanced Verification Techniques Based on Learning, DAC, p. 420-426, 1995
 and S. Reddy et al., Novel Verification Framework Combining Structural and
 OBDD Methods in a Synthesis Environment, DAC, p. 414-419, 1995, both of
 which are incorporated by reference herein. Verification can be terminated
 even without processing all the partitions if in any window w.sub.i the
 function .function..sub.i.sym.g.sub.i is found to be satisfiable.
 Another way of verifying two circuits is to probabilistically check their
 equivalence. Methods for doing so are disclosed in M. Blum et al.,
 Equivalence of Free Boolean Graphs Can Be Decided Probabilistically in
 Polynomial Time, Information Processing Letters, 10:80-82, March 1980 and
 J. Jain et al., Probabilistic Verification of Boolean Functions, Formal
 Methods in System Design, Jul. 1, 1992, both of which are incorporated by
 reference herein. In probabilistic verification, every minterm of a
 function .function. is converted into an integer value under some random
 integer assignment p to the input variables. All the integer values are
 then arithmetically added to get the hash code H.sub.p (.function.) for
 .function.. One can assert, with a negligible probability of error, that
 .function..tbd.g iff H.sub.p (.function.)=H.sub.p (g). In the case of
 orthogonal partitions, no two partitions share any common minterm. Hence,
 each partition can be hashed separately, and their hash codes added to
 obtain H.sub.p (.function.). This implies that to check if H.sub.p
 (.function.)=H.sub.p (g), both f and g partitioned and has had
 independently. Both f.sub.i and g.sub.i do not need to be in the memory at
 the same time. Further, it is not necessary that both .function. and g
 have the same window functions.
 B. Sequential and FSM Verification
 A key step in sequential circuit verification using ROBDDs is reachability
 analysis. Reachability analysis is also community called Model Checking,
 and Model Checking procedures are described in K. L. McMillan, Symbolic
 Model Checking, Klumer Academic Publishers 1993 and E. M. Clarke et al.,
 Automatic Verification of Finite-State Concurrent Systems Using Temporal
 Logic Specifications, 8 TOPLAS 244-263 (1986), both of which are
 incorporated herein by reference. Reachability analysis consists of
 computing the set of states that a system can reach starting from the
 initial states. Given the present set of reached states, R(s), and the
 transition relation for the system, T(s,s'), relating present state
 variables, s, with the next state variables, s', the set of next states,
 N(s'), is evaluated using the following equation:
EQU N(s')=.E-backward..sub..delta. [T(s,s'){character pullout}R(s)] (2)
 The set of next states is added to the set of present states and the above
 computation is repeated until a fixed point is reached. This fixed point
 represents the set of all reachable states of the system.
 In many cases the ROBDDs representing the transition relation T(s,s')
 become very large. To handle these cases, in partitioned transition
 relations in which the transition relations of individual latches, T(s,
 s')s.sub.2, are represented separately (with some possible clustering of
 T.sub.i s) is useful. The use of partitioned transition relations is
 described in J. R. Burch et al., Symbolic Model Checking: 10.sup.20 States
 and Beyond, Information and Computation, 98(2):142-170, 1992, incorporated
 by reference herein. Two types of partitioned transition relations were
 discussed: conjunctive and disjunctive. In such partitioning, the
 transition relation is given by T(s,s')=T.sub.1 (s,s'){character pullout}
 . . . {character pullout}T.sub.m (s,s'), where each T.sub.i is represented
 as a separate ROBDD. This type of partitioning is a special case of
 conjunctively partitioned-ROBDDs. The partitioning of the present
 invention is more general since T.sub.i s need not always correspond to
 individual latches. The usefulness of the conjunctively partitioned
 transition relations is also limited because existential quantification
 does not distribute over conjunctions. In the worst case, if all the
 T.sub.i 's depend on all the present state variables then conjunctive
 partition transitions cannot be used.
 An interesting case is that of disjunctive partitions in which existential
 quantification distributes over the partitions. The present invention
 allows for disjunctively partitioning the transition relation without
 having to place any restrictions on the underlying model of transition for
 a given system. In the present invention, any set of .function..sub.i s
 such that T(s,s')=.function..sub.1 + . . . +.E-backward..sub.s
 (R(s){character pullout}.function..sub.k) can be used to represent the
 transition relation. The set of next states can be evaluated using the
 following equation:
 N(s')=.E-backward..sub..delta. (R(s){character pullout}.function..sub.1)+
 . . . +.E-backward..sub..delta. (R(s){character pullout}.function..sub.k)
 This calculation can be performed by keeping only one .function..sub.i for
 1.ltoreq.i.ltoreq.k in the memory. Notice that in the above calculation
 the window functions which correspond to .function..sub.i s are not
 needed.
 Partial verification is useful for verifying sequential circuits because
 these circuits are often unverifiable. Using the methods and systems of
 the present invention provides significant information regarding such
 circuits.
 C. Partial .PSI.Verification Using Partitioning.
 The representation of some circuits or systems cannot be compactly
 represented even by partitioned ROBDDs. In these cases a significant
 fraction of the function generally may be constructed. For example, a
 circuit for which 132 out of 256 partitions can be constructed before
 program execution aborts due to time resource constraints allows about 52%
 of the truth table to be analyzed. In contrast, when using monolithic
 ROBDDs program execution aborts without giving any meaningful partial
 information. A simulation technique is also inadequate in covering the
 given function representation of the circuit or system. When a design is
 erroneous, there is a high likelihood that the erroneous minterms are
 distributed in more than one partition and can be detected by processing
 only a few partitions. Thus, in many cases errors in circuits or systems
 can be detected by constructing only one or two partitions.
 This sampling method can be applied to any design whether it is
 combinational, sequential, or even a mixed signal design. Generally a
 given design is simplified by creating partitions of its state space and
 analyzing only the functionality of the design within the partitions.
 The circuit is partitioned by applying the partitioning vectors and the
 design is verified for each of the partitioning vectors. These vectors are
 partial assignments either on input variables or internal variables of the
 given circuit or system. A partial assignment is an assignment on some of
 the variables but not all of the variables. The partitioning vectors
 simplify the circuit/system so that the circuit has a smaller truth table.
 Thus the resulting partitioned system will be easier to verify using
 either model checking or combinational verification methods.
 For a very complex design which cannot be verified using formal methods,
 the number of vectors chosen may be sufficiently small that the sampling
 is not very expensive in terms of computational resources. The number of
 variables on which partitioning is performed, however, are large enough
 that each partition is small enough so that formally verifying a given
 design is possible. As an example, for a sequential circuit with 1000
 flip-flops and 100 input variables, which is very difficult to verify
 using traditional BDD-based methods, 100 partitions may be formed using 20
 variables. The circuit may then be partially verified by examining
 partitions of the Boolean space of the circuit.
 A fixed number of partitioning vectors may be automatically chosen using
 splitting variable selection approach based on the criteria of redundancy
 and balancedness as described in A. Narayan et al., Partitioned-ROBDDs--A
 Compact, Canonical and Efficiently Manipulable Representation of Boolean
 Functions, ICCAD, November 1996. Specifically, if we want to partition on
 R variables (say, 20) then a splitting variable selection approach is
 applied to the combinational representation of the given sequential
 circuits and the R number of best variables are picked automatically based
 upon a cost function of redundancy and balancedness. In other words, given
 some Z, desired number of partitions can be created by generating (say,
 randomly) some Z (where Z=&lt;2.sup.R) number of Boolean assignments on these
 R variables. These Z partial assignments are either repeated in every
 application of a transition relation or the Z assignments can be changed
 in subsequent applications of transition relation by generating different
 or random assignments on the given R variables. These R variables may also
 change in subsequent applications of transition relations.
 In another embodiment, users may select input vectors from manually
 generated test-suites used to verify a given design. Most designs have
 such test-suites. Certain assignments of some subset of the input
 variables may be known to be critical to the design. Test-suites, however,
 often cannot include every possible combination of the remaining
 unassigned variables and therefore cannot verify the correctness of a
 design given assignments for some of the variables. The system and method
 of the present invention allow for such a verification through the use of
 the partitioning techniques described herein.
 The specialized knowledge of engineers with knowledge of the design under
 test may also be utilized, either directly or indirectly. The knowledge of
 the engineer or designer may be directly used by selecting the test
 vectors under the explicit guidance as the designer. The explicit guidance
 may take the form of application of transition relations or the choice of
 vectors to use for sampling on BDD blow-ups. The designer can also supply
 some Q input variables, typically control variables for creating samples
 for verification. Given some Z, the desired number of partitions can be
 created by generating (say, randomly) some Z (where Z=&lt;2.sub.Q) number of
 Boolean assignments on the Q variables.
 The knowledge of the engineer or designer may also be indirectly utilized.
 The manually generated test-suite for the design can be analyzed to
 determine partitioning vectors. Specifically all the test vectors in the
 test-suite can be written in an ordered fashion in a file. We can use k
 number of most common sequences of partial assignments in the test-suite
 and then use these for the sampling. So if some "sequences of partial
 assignments" are common between different test-vectors then such sequences
 are good candidates for sampling method. For purpose of clarity of
 description, note a string STR which is a sequence of partial assignments
 is derived from a sequence of input-combinations, assigned to the input
 variables, and can be depicted as follows:
 STR=partial.sub.-- 1 &lt;from-time-frame=1&gt;; partial.sub.-- 2
 &lt;from-time-frame-2&gt;; . . . ; partial_m&lt;from-time-frame-m&gt;, where each
 partial_i is a partial assignment.
 Partial.sub.-- 1 will be used to restrict the circuit in the first
 application of transition relation (as explained in the next section),
 partial.sub.-- 2 in the second application of transition relation, and so
 on. We will collect N number of such strings STR.sub.-- 1, STR.sub.-- 2, .
 . . , STR_N. The choice of N can be interactive and fully depends on the
 complexity of the given system. For example, with many of current systems
 having 1000 flip-flops, we believe N can range from 5 to 100. Now, we will
 do formal verification by making N different runs of a formal verifier,
 verifying a set of simpler circuits C.sub.1, C.sub.2, . . . , C.sub.N
 where each C.sub.i is a design that has been restricted using the partial
 assignments in it as described above as well as in the following section.
 In the scenario that the test-suite initially also contained only partial
 assignments on a subset of input variables then we can also see which
 variables occur most frequently in the given test-suite. If we want to
 partition on P variables (say, 20) then we look for P number of most
 commonly occuring variables in the test-suite. Given some Z, we can choose
 to create the desired number of partitions by generating (say, randomly)
 some Z (where Z=&lt;2.sub.P) number of Boolean assignments on these P
 variables. Additionally, if the user desires then he can restrict the
 sequence length of our chosen "sequences of partial assignments" to some
 first k number of time frames where k can even be 1.
 Additionally, recursive testing of designs and heirarchies of designs often
 occurs. Thus, any vectors found to generate errors in prior testing of the
 design also form appropriate partitioning vectors.
 Suppose the sequence of N vectors is as follows:
 [V.sub.1 =0, V.sub.2 =1]; [V.sub.1, V.sub.3 =1]; [V.sub.3 =1; V.sub.4 =1];
 . . . , [N-such sequences]. Furthermore, a sequential circuit M can be
 thought of as a concatenation of several identical combinational circuits
 C.
 The concatention is known to be done by connecting the next state variables
 of a circuit C to the present state variables of the circuit C coming next
 in the concatenation sequence. That is M can be thought of as M=C.sub.1
 &lt;connected-to&gt; C.sub.2 &lt;connected-to&gt; C.sub.3 . . . where each C.sub.i is
 a copy of the same combinational circuit. Thus, the circuit in time frame
 3 is reffered to as circuit C.sub.3.
 Now, during application of, say, a state space traversal verification
 method, we will initially restrict the given design by setting V.sub.1 =0,
 V.sub.2 =1. With this restriction certain states S.sub.1 are reached after
 application of a transition relation. V.sub.1 =0, V.sub.3 =1 are set once
 state S.sub.1 is reached and a transition relation is applied to reach
 S.sub.2. Once S.sub.2 is reached V.sub.2 =1; V.sub.1 =1 are set and the
 transition relation is again applied to reach state S.sub.3. This
 procedure continues until state S.sub.n is reached. Thus, all properties
 of the system for the states captured by S.sub.N can now be verified.
 Also, if in some application of a transition relation the BDD representing
 state space S.sub.i are blowing-up then the BDD is partitioned by either
 manually (interactively) providing values (restrictions) on some more
 input variables or by throwing away a part of the reached state space.
 After such partitioning we again continue with our reachability analysis
 till we decide to terminate our computation because of a reason such as we
 cannot carry on a BDD based analysis any further or because we have
 reached the fixed-point.
 In this way, though only a limited part of the functionality of the given
 design has been verified greater part of a very large space state has been
 processed. Partitioned-ROBDDs allow a remarkable control on the space/time
 resources and therefore functional-coverage. Thus, the success of a
 verification experiment can be ensured by changing the parameters of
 decomposition and the number of partitions that need to be created.
 D. Use in a Filter Approach
 The partitioning verification techniques of the present invention are also
 useful in the filter approach described in U.S. patent application Ser.
 No. 08/857,916. A filter approach utilizes a combination of communicating
 testing/verification techniques to verify a circuit or system. In essence,
 simpler and faster techniques are first used to verify or alter the
 circuit. If the simpler and faster techniques cannot verify the circuit,
 then the results of these techniques are passed to more elaborate and
 costly verification techniques. The most sophisticated techniques are
 techniques which, if given enough time and memory, can verify a circuit
 without the help of another verification technique. These most
 sophisticated techniques are referred to as core techniques. Within such a
 framework, the partitioned BDD techniques of the present invention are a
 core technique.
 E. Parallel Implementation of an ROBDD Package
 The present system and method invention provides a superlinear reduction
 (even exponential) in the resources required to build ROBDDs. Further,
 each partition is independent and can be scheduled on a different
 processor with minimal communication overhead. Each partition can also be
 ordered independently and can exploit full power of dynamic reordering.
 Thus, the present invention provides many advantages in verification of
 Boolean circuits and systems. Many circuits and systems that were
 heretofore unverifiable can be checked for equivalence. Although the
 present invention has been described in certain specific embodiments, many
 additional modifications and variations will be apparent to those skilled
 in the art. It is therefore to be understood that this invention may be
 practiced otherwise than specifically described. Accordingly, the present
 embodiments of the invention should be considered in all respects
 illustrative and not restrictive, the scope of the invention to be
 indicated by the appended claims rather than the foregoing description.