Method and apparatus for implicit verification of digital circuits

[0003] The present invention relates generally to digital circuit design verification, and more particularly to formal verification across differing circuit architectures.

[0004] In the design of digital integrated circuits, it is often desirable to be able to ascertain whether two circuits are equivalent. Equivalency of two combinational circuits can be defined, in a functional sense, as follows. A first design and a second design are equivalent if both accept the same set of input combinations, and if both produce the same output combination for each input combination.

[0005] The determination of circuit equivalency has become increasingly important with the emergence of large scale digital integrated circuits that incorporate an entire system on a chip. Such chips have reached a size and complexity level where it is difficult to verify them, in a timely manner, using traditional gate-level simulation. As a result, static verification tools are being more widely utilized by chip designers. Examples of such static-verification tools are PrimeTime, a static-timing analyzer, and Formality, a formal verification tool. Both PrimeTime and Formality are products of Synopsys, Inc., 700 East Middlefield Road, Mountain View, Calif. Static-timing analysis is used to analyze and verify the timing of the design and formal verification is used to verify a design's functionality by proving functional equivalence.

[0006] A design methodology that utilizes formal verification can reduce the number of time-consuming gate-level simulation runs. In a typical design process, utilizing logic synthesis and formal verification tools, the designer specifies his or her initial design at the register-transfer level (RTL). This RTL source specification is translated into a gate-level netlist by a logic synthesis tool, such as Design Compiler, produced by Synopsys, Inc., 700 East Middlefield Road, Mountain View, Calif. Formal verification is then used to compare the functional equivalency of the RTL source specification to the post-synthesis gate-level netlist. This gate-level netlist may then undergo several succeeding transformations that are intended to produce equivalent gate-level netlists. Such succeeding transformations can include: scan chain insertion, clock-tree synthesis, in-place optimization and manual editing. After each of these succeeding transformations, formal verification can be used to verify that the result of the latest transformation is functionally equivalent to the resulting gate-level netlist of the preceding transformation. For each of these comparisons a known-to-be-correct design (reference design) is compared against a design of unknown correctness (implementation design).

[0007] While formal equivalence checkers generally provide better coverage than gate-level simulation, such formal equivalency checking is fundamentally an NP-complete problem and therefore existing algorithms do not use reasonable memory or CPU resources for certain classes of circuits.

[0008] For example, (binary decision diagrams) BDDs have been successfully used for formal equivalency checking, but there are many functions for which the size of the BDD is exponential with respect to the size of the circuit being verified. This is most commonly known to occur with multiplier circuits. BDDs are generally incapable of verifying multipliers with more than sixteen bits in the multiplicands.

[0009] Other approaches to formal equivalency checking utilize the fact that (as discussed above) the implementation circuit is derived directly from the reference circuit through synthesis. Because of this, the two circuits usually have a great deal of structural similarity. Certain verification algorithms take advantage of this similarity by trying to find internal equivalence points and simple implications which enable the verification process to succeed. As long as the implementation circuit is directly synthesized from the reference circuit, such approaches can be successful and have been shown to verify multiplier circuits with multiplicand widths in excess of 64 bits. Unfortunately, multipliers with different architectures do not provide enough structural similarity to allow verification with the these methods.

[0010] Architectural changes are common, however, and particularly during the earlier part of the design process. For example, with respect to multipliers, it is common to swap one multiplier architecture for another in order to explore design tradeoffs. As a specific example, it would not be uncommon to substitute an array multiplier (as shown in FIG. 1) for a Wallace-tree multiplier (as shown in FIG. 2), or vice versa.

[0011] Across different architectures, there are known methods for verification, but only if the verification tool knows that the circuits to be verified are multipliers and also knows how the integers processed by the multiplier are encoded.

[0012] It would therefore be desirable to develop a general technique for formally determining equivalence between circuits of different architectures such that it is not necessary for the verification tool to know the particular functionality of the circuits to be compared nor the specific way in which the operands of the circuits are encoded.

[0013] The present invention utilizes a particular type of structural similarity between the reference and implementation designs, which we shall refer to as “structural dependence,” in order to broaden the class of circuits that are formally verifiable in an efficient manner. Structural dependence is the dependence of the higher-order result bits of a design upon the circuitry driving the lower-order result bits.

[0014] Because structural dependence is a rather general and high-level characteristic, two circuits which might be considered, according to conventional standards, as having very different structures and therefore not amenable to efficient formal verification, may in fact be efficiently comparable using the present invention.

[0015] Structural dependence is utilized in partitioning the two circuits, η and η′, to be compared. Each circuit has the fanin cones of its primary inputs ordered from smallest to largest. Each such fanin cone is the basis for forming a circuit partition, but part of a fanin cone may be excluded from a partition to the extent it is already part of another partition.

[0016] Structural dependence partitioning creates subcircuits η_ifor circuit η and subcircuits η′_ifor circuit η′. Each subcircuit (or partition) η_idrives a primary output z_iand each subcircuit (or partition) η′_idrives a primary output z′_i. In addition, each subcircuit η_imay have: a fanout set Y_ito its higher order subcircuit η_i+1, (if it has a higher order subcircuit and is connected to it), inputs from the fanout set Y_i−1of its lower order subcircuit η_i−1, (if it has a lower order subcircuit and is connected to it) and primary inputs from X (if it is driven by one or more primary inputs). Likewise, each subcircuit η′_imay have: a fanout set Y′_ito its higher order subcircuit η′_i+1(if it has a higher order subcircuit and is connected to it), inputs from the fanout set Y′_i−1of its lower order subcircuit η′_i−1(if it has a lower order subcircuit and is connected to it) and primary inputs from X (if it is driven by one or more primary inputs).

[0017] Since the lower order primary output bits have smaller fanin cones with fewer inputs than the higher order bits, they may be verifiable by known techniques. As we proceed toward the higher order bits, however, implicit verification using structural dependence becomes increasingly important.

[0018] Implicit verification operates as follows, for example, with respect to verifying the high-order primary output bit of two n bit circuits. While the following discussion is stated with respect to two multiplier circuits being compared, it applies to any two circuits which have been partitioned according to structural dependency.

[0019] A condition called C is defined which asserts that the high order primary output bits, of each of the two multipliers being compared, are equivalent. More specifically, condition C asserts that z_n−1=z′_n−1. At this point we are only considering z_n−1and z′_n−1as being outputs, respectively, of subcircuits η_n−1and η′_n−1.

[0020] A condition A is defined which asserts that all the lower-order primary output bits of the two multipliers are equivalent. More specifically, condition A asserts that z_i=z′_ifor 0≦i<n−1. Thus all the remaining subcircuits, η₀to η_n−2and η′₀to η′_n−2, are being considered in A.

[0021] We then try to prove the implication that if A is true then C is true, or mathematically A→C. This is equivalent to showing that the conjunction of A being true and C not being true can never be true, or mathematically A·{overscore (C)}=0.

[0022] Once A→C has been proven true, assuming that condition A is known to be true, it is then known by implication that C is true.

[0023] Implicit verification utilizes the fact that it is usually easier to prove the implication A→C than to prove C in isolation, since A being true while C being false usually has many conflicting requirements.

[0024] Rather than initially formulating a condition A comprised of asserting all lower order bits (i.e., those bits of lower order than C) as being equivalent, it is often advantageous to begin with an assertion (which shall be referred to as A_n−2) that just the next lower order bits are equivalent (i.e., z_n−2=z′_n−2). This more limited assertion may provide sufficient constraints such that the implication A_n−2→C can be proven. At this point, only subcircuits η_n−1, η′_n−1, η_n−2and η′_n−2are being considered. If A_n−2does not provide sufficient constraints, then it can be successively augmented with assertions that the next lower pairs of output bits are equivalent. For example, the next lower pair of output bits to be asserted as equivalent would be z_n−3=z′_n−3(which shall be referred to as A_n−3). At this point only subcircuits η_n−3and η′_n−3are being added for consideration in addition to the subcircuits η_n−1, η′_n−1, η_n−2and η′_n−2already considered for A_n−2→C . If the implication A_n−2·A_n−3→C can be proven true, then the next lower pair of output bits (which would result in the implication A_n−2·A_n−3·A_n−4→C) need not be considered.

[0025] In order to prove a particular condition (or antecedent) A as being true, such that it can be used in conjunction with a proven implication A→C to show that a consequent C is true, it is often advantageous to prove a “chain” of implications. The chain of implications typically begins with an implication whose consequent asserts the equivalency of low order output bits and therefore has an antecedent A that is provable by conventional means. Once the implication for the low order output bits has “fired” (i.e., its antecedent has been satisfied), its consequent can be used, in turn, to fire an implication for asserting the equivalency of the next higher-order output bit pair. Similarly, the equivalency of the next higher-order output bit pair can be used to fire an implication for proving equivalency of an even higher-order output bit pair. Such a chain of implication firings continues until all output bits, between the two circuits to be compared, have been shown equivalent.

[0026] Advantages of the invention will be set forth, in part, in the description that follows and, in part, will be understood by those skilled in the art from the description or may be learned by practice of the invention. The advantages of the invention will be realized and attained by means of the elements and combinations particularly pointed out in the appended claims and equivalents.

[0027] The accompanying drawings, that are incorporated in and constitute a part of this specification, illustrate several embodiments of the invention and, together with the description, serve to explain the principles of the invention:

[0028] FIG. 1 shows an eight-bit array multiplier as an exemplary architecture for verification by the present invention;

[0029] FIG. 2 shows an eight-bit Wallace tree multiplier as an exemplary architecture for verification by the present invention;

[0030] FIG. 3 depicts a partitioning of a circuit in accordance with its structural dependence;

[0031] FIGS. 4A and 4B illustrates two exemplary circuits for verification by the present invention and their partitioning into subcircuits by the present invention;

[0032] FIG. 5 presents the pseudo-code for implementing the general method of implicit verification of the present invention;

[0033] FIGS. 6A through 6F presents a simulated “execution” of the pseudo-code of FIG. 5 according to the exemplary circuits of FIG. 4;

[0034] FIG. 7 shows a table of experimental results from running a programmed implementation of the procedure of FIG. 5;

[0035] FIG. 8 depicts a hardware environment in which the present invention can be operated; and

[0036] FIGS. 9A through 9D show example circuits and their operating characteristics for the present invention.

[0037] Reference will now be made in detail to preferred embodiments of the invention, examples of which are illustrated in the accompanying drawings. Wherever possible, the same reference numbers will be used throughout the drawings to refer to the same or like parts.

[0038] The present invention utilizes a particular type of structural similarity between the reference and implementation designs, which we shall refer to as “structural dependence,” in order to broaden the class of circuits that are formally verifiable in an efficient manner. Structural dependence is the dependence of the higher-order result bits of a design upon the circuitry driving the lower-order result bits. Structural dependence is a feature of multiplier circuits, and it is a characteristic found in many other types of circuits as well.

[0039] Because structural dependence is a rather general and high-level characteristic, two circuits which might be considered, according to conventional standards, as having very different structures and therefore not amenable to efficient formal verification, may in fact be efficiently comparable using the present invention. For example, according to conventional standards, an array multiplier (as shown in FIG. 1) and a Wallace-tree multiplier (as shown in FIG. 2) would be considered architecturally different. However, because both these multiplier architectures share the property of structural dependence, they can be efficiently compared with each other by the present invention. A detailed discussion of the array multiplier and Wallace-tree multiplier architectures is presented below in connection with a discussion of certain test results from an implementation of the present invention.

[0040] STRUCTURAL DEPENDENCE

[0041] Structural dependence means that the primary output bits of a circuit can be ordered, from higher to lower order, such that the logic which drives the higher order primary output bits depends heavily on the logic driving the lower order primary output bits. Structural dependence in a circuit η is determined by partitioning the circuit as follows. The result of partitioning a circuit η, in accordance with the following method, is depicted in FIG. 3.

[0042] Let circuit η have primary inputs X={x₀, . . . , x_m−1} and primary outputs Z={z₀, . . . , z_n−1}.

[0043] First, order the primary outputs, from z₀to z_n−1, based on the increasing size of their fanin cones.

[0044] Starting with the smallest cone, whose output is called z₀, all the gates in the fanin of z₀are marked as being in the subcircuit η₀. Nets whose source is in η₀(and are not driven directly by a primary input), but which have sinks in other parts of the circuit, we place in the fanout set Y₀.

[0045] Next, all cells in the fanin cone of output z₁, which are not already in η₀, are put in subcircuit η₁. Nets whose source is in η₁(and are not driven directly by a primary input), but which have sinks in other parts of the circuit, we place in the fanout set Y₁. Note that no net in Y₁can have a sink in η₀.

[0046] Third, all cells in the fanin cone of output z₂, which are not already in η₀or η₁, are put in subcircuit η₂. Nets whose source is in η₂(and are not driven directly by a primary input), but which have sinks in other parts of the circuit, we place in the fanout set Y₂. Note that no net in Y₂can have a sink in η₀or η₁.

[0047] We continue in this fashion, for each output z_i, creating a subcircuit η_iand a fanout set Y_i, until we reach the last output z_n−1.

[0048] Each subcircuit η_icomputes a function 𝑓_i(X,Y_i−1). Note that the fanout set Y_n−1is necessarily empty.

[0049] If the sizes of the fanout sets are relatively large compared to the size of X, then we say that the circuit exhibits structural dependence.

[0050] IMPLICIT VERIFICATION OVERVIEW

[0051] Assume we have two structurally dependent circuits η and η′ that are to be shown equivalent. Each circuit is partitioned as discussed above (and shown in FIG. 3), creating subcircuits η_iwith fanout sets Y_ifor circuit η and subcircuits η′_iwith fanout sets Y′_ifor circuit η′. Since the lower order primary output bits have smaller fanin cones with fewer inputs than the higher order bits, they may be verifiable by known techniques. As we proceed toward the higher order bits, however, implicit verification using structural dependence becomes increasingly important.

[0052] Implicit verification operates as follows, for example, with respect to verifying the high-order primary output bit of two n bit circuits. While the following discussion is stated with respect to two multiplier circuits being compared, it applies to any two circuits which have been partitioned according to structural dependency.

[0053] A condition called C is defined which asserts that the high order primary output bits, of each of the two multipliers being compared, are equivalent. More specifically, condition C asserts that z_n−1=z′_n−1. At this point we are only considering z_n−1and z′_n−1as being outputs, respectively, of subcircuits η_n−1and η′_n−1.

[0054] A condition A is defined which asserts that all the lower-order primary output bits of the two multipliers are equivalent. More specifically, condition A asserts that z_i=z′_ifor 0≦i<n−1. Thus all the remaining subcircuits, η₀to η_n−2and η′₀to η′_n−2, are being considered in A.

[0055] We then try to prove the implication that if A is true then C is true, or mathematically A→C. This is equivalent to showing that the conjunction of A being true and C not being true can never be true, or mathematically A·{overscore (C)}=0.

[0056] A·{overscore (C)}=0 can be proven by a variety of methods. In a first embodiment, all combinations of inputs to the function A·{overscore (C)} are applied and none are shown to satisfy the expression. In a second embodiment, A and {overscore (C)} are each represented by BDDs which are then conjuncted together, in a manner known in the art, resulting in a BDD whose output value can be determined as being only zero.

[0057] Note also that proving A·{overscore (C)}=0 is mathematically equivalent to proving {overscore (A)}+C=1.

[0058] Once A→C has been proven true, assuming that condition A is known to be true, it is then known by implication that C is true.

[0059] Implicit verification utilizes the fact that it is usually easier to prove the implication A→C than to prove C in isolation, since A being true while C being false usually has many conflicting requirements.

[0060] IMPLICIT VERIFICATION PSEUDO-CODED METHOD

[0061] Before giving the pseudo-coded method for implicit verification, it will be useful to introduce a few additional definitions.

[0062] For a circuit η with inputs X and outputs Z, an input-output relation of η is defined to be the function χ(X,Z)→{0,1} where χ=1 only for consistent assignments of the inputs and outputs of η. The input-output relation of η can be built as follows. Let Z={z_i} be the set of outputs of η which implements functions z_i=𝑓_i(X). Then χ(X,Z)={overscore ((z_i𝑓_i))}.

[0063] A subcircuit η_i, with inputs X_iand outputs Z_i, has the same definition for χ_ias described above for the entire circuit η, except that X_iand Z_iare defined as follows. X_iis comprised of any primary inputs to η_iand of any inputs to η_ithat belong to Y_i−1. Z_iis comprised of the primary output z_iof η_iand of any outputs that belong to Y_i.

[0064] A pseudo-code description for the general method is depicted in FIG. 5.

[0065] The two circuits η and η′ to be verified are passed to the procedure “imp_ver.”

[0066] The partitioning operation invoked in line 2 partitions each of η and η′ according to the procedure discussed above with respect to FIG. 3.

[0067] The outer “for” loop, beginning at line 3, attempts to verify the equivalency of each output pair of outputs z_iand z′_i. For each such pair, the following operations are performed.

[0068] The consequent condition {overscore (C)}, that z_i≠z′_i, is formed by determining 𝑓_i𝑓_i. As discussed previously with respect to partitioning, 𝑓_iis the output of subcircuit η_i, not of the entire circuit η, and 𝑓′_iis the output of subcircuit η′_i, not of the entire circuit η′. As discussed above with respect to the overview of implicit verification, {overscore (C)} is formed, rather than C, because the object is to prove A→C by showing that A·{overscore (C)}=0. Computing {overscore (C)} puts constraints on the inputs of η_iand η′_i.

[0069] The inner “for” loop creates the antecedent A by adding, one at a time, the condition that the previous pairs of outputs, z_jand z′_j, are equivalent. This is accomplished in line 6 by forming the conjunction of the input-output relations for subcircuits η_iand η′_i(i.e., χ_j·χ′_j) and taking the conjunction of that with the assertion that the output functions of subcircuits η_iand η′_iare equal (i.e., {overscore (𝑓_j𝑓′_j)}).

[0070] If the quantity g ever becomes zero, then a “break” from the inner “for” loop is performed, in accordance with line 7, and the outputs z_iand z′_iare marked as implicitly verified. As discussed above, the determination of g as being zero can be accomplished by a variety of methods including proof by contradiction or conjunction of BDDs representing g, χ_j, χ′_jand ({overscore (𝑓_j𝑓′_j)}).

[0071] If the inner “for” loop ends without g becoming zero, then, in accordance with line 9, the outputs z_iand z′_iare marked as not being implicitly verified. In addition to marking the outputs as not being implicitly verified, a break from the outer “for” loop is performed with a notation that verification has failed. This breaking from the outer “for” loop ensures that whenever g does become zero (a condition that by itself only indicates that an implication has been proved) the pair of outputs represented by g has been identified as equivalent, since the outer loop would not have reached this point unless all the lower-order pairs of outputs have already been verified as equivalent.

[0072] If the outer “for” loop ends with all pairs of outputs being marked as equivalent, then the two circuits η and η′ are equivalent.

[0073] IMPLICIT VERIFICATION EXAMPLE

[0074] Pseudo-coded implicit verification will now be applied to the specific example of FIG. 4.

[0075] FIGS. 4A and 4B depict, respectively, two circuits η and η′ for verification by the pseudo-code method of FIG. 5. As can be seen, circuit η has already been partitioned into structurally dependent subcircuits η₀to η₃, while circuit η′ has already been partitioned into structurally dependent subcircuits η′₀to η′₃.

[0076] FIG. 6A depicts the functions 𝑓₀to 𝑓₃and χ₀to χ₃that represent η₀to η₃in the execution of the FIG. 5 pseudo-code. Similarly, FIG. 6B depicts the functions 𝑓′₀to 𝑓′₃and χ′₀to χ′₃that represent η′₀to η′₃in the execution of the FIG. 5 pseudo-code. FIGS. 6A and 6B correspond to the execution of line 2 of the pseudo-code. It should be noted that while the symbol of a Hi plus-sign surrounded by a circle (“”) has been used to represent the exclusive-OR function, the similar symbol of a dot surrounded by a circle is being used to represent the exclusive-NOR function.

[0077] FIG. 6C depicts the pseudo-code “for” loop of line 3 performing its first iteration with i=0. Specifically, FIG. 6C depicts the equation for g as computed at line 4. The inner “for” loop of line 5 is never executed and therefore imp_ver proceeds directly to line 9 where the g of FIG. 6C is determined to always compute the result zero. As discussed above, the determination of g as always resulting in a zero value may be accomplished by a variety of methods. For the purposes of illustration herein, the determination is made by noting that the variable x₀will never be different from itself. This determination of g proves that the lowest level bits of the two designs are equivalent.

[0078] FIG. 6D depicts the pseudo-code “for” loop of line 3 performing its second iteration with i=1. Specifically, FIG. 6D first depicts the equation for g as computed at line 4. The inner “for” loop of line 5 is then represented with j=0. The function g is recomputed according to line 6 of the pseudo-code and as shown in FIG. 6D below j=0. In accordance with line 7, and as further shown in FIG. 6D, g is determined to always compute the result zero with the result that the inner “for” loop is broken. For the purposes of illustration herein, the determination is made by noting that x₀x₁is never different from itself. Therefore, the g on the right-hand-side of the expression of line 7 is always of value zero, making the entire conjunction of the right-hand-side zero. Execution then proceeds to line 9 where it is noted that bits z₁and z′₁have been proven equivalent.

[0079] FIG. 6E depicts the pseudo-code “for” loop of line 3 performing its third iteration with i=2. Specifically, FIG. 6E first depicts the equation for g as computed at line 4. The inner “for” loop of line 5 is then represented with j=1. The function g is recomputed according to line 6 of the pseudo-code and as shown in FIG. 6E below j=1. In accordance with line 7, and as further shown in FIG. 6E, g is determined to always compute the result zero with the result that the inner “for” loop is broken. For the purposes of illustration herein, the determination is made by transforming the right-hand-side of the expression of line 6 into a sum-of-products form (such complete transformation to sum-of-products form not being shown in FIG. 6E). It is then noted that every product term of the sum-of-products form requires at least one of its variables to be both TRUE and not TRUE. Therefore it is noted that every product term evaluates to zero. Execution then proceeds to line 9 where it is noted that bits z₂and z′₂have been proven equivalent.

[0080] FIG. 6F depicts the pseudo-code “for” loop of line 3 performing its fourth iteration with i=3. Specifically, FIG. 6F first depicts the equation for g as computed at line 4. The inner “for” loop of line 5 is then represented with j=2. The function g is recomputed according to line 6 of the pseudo-code and as shown in FIG. 6F below j=2. In accordance with line 7, and as further shown in FIG. 6F, g is determined to always compute the result zero with the result that the inner “for” loop is broken. For the purposes of illustration herein, the determination is made by transforming the right-hand-side of the expression of line 6 into a sum-of-products form (such complete transformation to sum-of-products form not being shown in FIG. 6F). It is then noted that every product term of the sum-of-products form requires at least one of its variables to be both TRUE and not TRUE. Therefore it is noted that every product term evaluates to zero. Execution then proceeds to line 9 where it is noted that bits z₃and z′₃have been proven equivalent. With respect to the Summary of the Invention above, this execution of the outer “for” loop has proven A₂→C, with only subcircuits η₂, η′₂, η′₃and η′₃being considered.

[0081] Execution of the outer “for” loop then ends and line 12 is executed. Since all pairs of outputs between η and η′ have been verified as equivalent, the value “SUCCESS” is returned by imp_ver.

[0082] In summary, the operation of the FIG. 5 pseudo-code can be viewed as follows.

[0083] For each iteration of the outer “for” loop of line 3, a function g is computed which represents, in sum-of-products (SOP) form, a “set” of product terms. Each product term represents a combination of values which, when applied to the inputs of η_iand η′_i, cause the z_iand z′_ioutputs to be different. This set of possible combinations is then further constrained, and hopefully reduced to an empty set, by the combinations of inputs and/or outputs permitted by the lower-order bits of circuits η and η′.

[0084] Specifically, the inner “for” loop of line 5 begins with the subcircuits of the next most significant outputs z_jand z′_j. The right side of the expression of pseudo-code line 6 can be viewed as follows. The exclusive-NOR function represents, in SOP form, the combinations of values which, when applied to the inputs of η_jand η′_j, cause the z_jand z′_joutputs to be the same. The conjunction χ_jand χ′_jrepresents the combinations of values which, if applied to the inputs and outputs of η_jand η′_j, are consistent with the operation of η_jand η′_j. The set of combinations of χ_j·χ′_jis typically narrowed in its conjunction with the combinations of the exclusive-NOR function. The net result of determining χ_j·χ′_j·({overscore (𝑓_j𝑓′_j)}) is to produce a set of combinations which limit the values that all inputs into η_iand η′_i(both the Y_jand Y′_jinputs, as well as the primary inputs) may assume.

[0085] If χ_j·χ′_j·({overscore (𝑓_j𝑓′_j)}) does not provide enough constraints to bring g to zero, then another iteration of the inner “for” loop is performed, in which the constraints of the next less significant subcircuits are added.

[0086] As discussed above, the inner “for” loop will continue adding constraints, if necessary, until it utilizes the entire portion of circuits η and η′ upon which η_iand η′_iare structurally dependent by including the constraints of the least significant subcircuits η₀and η′₀.

[0087] Note that while the inner “for” loop of line 5 proceeds from i−1 to 0, an alternative approach would be for the loop to iterate from 0 to i−1 (although this approach would typically result in a consideration of all the bits from 0 to i−1).

[0088] Also note that while the outer “for” loop of line 3 proceeds from 0 to n−1, an alternative approach would be for the loop to iterate from n−1 to 0. Note that running the outer “for” loop in reverse effects the interpretation of any errors detected: an error detected while i is equal to some iteration value k (where 0≦k≦n−1) means that there is a lack of equivalency in all bits iterated over thus far, from i=n−1 down to and including i=k. When the outer “for” loop is proceeding from 0 to n−1, the detection of a lack of equivalency at bit i=k does not affect the fact that all the lower order bits, from i=0 up to and including i=k−1, have been verified.

[0089] TWO EXEMPLARY MULTIPLIER ARCHITECTURES

[0090] Array and Wallace-tree multipliers share the following architectural similarities. Given two n bit numbers, n partial products (of n bits each) are first generated. These n numbers are added together to form a total product. These two multiplier architectures differ, mainly, in how the partial products are added together.

[0091] In the “array multiplier,” for example, the partial products are added in a serial fashion using a linear array of carry-save adders (CSAs). CSAs are circuits which transform the problem of adding three numbers into the problem of adding two numbers. The advantage of CSAs is that they can perform their task in O(1) time. In the serial CSA array portion of an array multiplier (which adds the n partial products), CSAs must be utilized n times resulting in this portion of the array multiplier operating in O(n) time. At the end of the CSA serial array, the last two numbers are added with a carry-propagate adder (CPA), such as a carry-lookahead adder, which operates in O(log n) time. Thus the total time required for an array multiplier is O(n+log n)=O(n). FIG. 1 shows the array multiplier architecture schematically for eight bits.

[0092] In the “Wallace tree” multiplier architecture, as with the array multiplier architecture, the partial products are added using CSAs followed by a CPA. The Wallace tree architecture differs from the array multiplier architecture by arranging the CSAs in a balanced tree rather than as a linear array. The depth of the Wallace tree multiplier balanced tree is O(log n). When this balanced tree is followed by a CPA, the total time of the multiplication is O(log n+log n)=O(log n). FIG. 2 shows the Wallace tree architecture schematically for eight bits.

[0093] According to conventional standards, the array multiplier and Wallace tree multiplier do not share much structural similarity. There are no internal points which are functionally equivalent and it is difficult to form any implications between any two internal points of these circuits. Therefore, according to conventional techniques, it is difficult to formally verify equivalence between these two architectures.

[0094] These two architectures, however, both have a high degree of structural dependence making them efficiently verifiable with the techniques of the present invention.

[0095] TEST RESULTS

[0096] The procedure of FIG. 5 has been embodied as a program and used to verify array multipliers and Wallace-tree multipliers, generated with the architecture described above, for varying bit widths. The bit widths verified range from 8 to 32 bits.

[0097] Before verifying two multipliers, a preprocessing step was executed to determine any structurally equivalent points, according to known standards, in the two circuit networks. Since the array and Wallace-tree architectures are so structurally different, by known standards, the only equivalent points found were from the partial products next to the primary inputs. These partial products were then treated as primary inputs for purposes of applying the method of the present invention. Partitioning the circuits for structural dependence included sorting the outputs of each multiplier circuit according to the size of their variable support which has the result of effectively sorting the outputs from most-significant bit to least-significant bit. The functions determined for each multiplier circuit, in accordance with FIG. 5, were represented by BDDs. The basic operations of FIG. 5 were performed on the BDDs with a conventional BDD processing package having its dynamic variable ordering enabled. The results are presented in the table of FIG. 7, and discussed column-by-column as follows.

[0098] As can be seen, multipliers with 16 bits or less verified in under two minutes. Beginning with multipliers of 20 bits or more, CPU times greatly increased. This is believed to be due to the fact that dynamic variable reordering was needed and is computationally expensive. Multipliers of 32 bits were verified in under 6 hours. We are unaware of any known verification method which is able to verify multipliers of this size where the architectures are different as they are in this test case.

[0099] The amount of memory required approximately doubled for each additional four bits in the multipliers until 28 bits was reached. The memory requirements for verifying 28 and 32 bit multipliers were approximately the same. This is believed to be due to a hard limit on the number of BDD nodes required to trigger variable reordering. By repeatedly reaching this limit and significantly reducing the size of the BDDs each time the limit is reached, the maximum amount of memory used remained relatively constant.

[0100] The last column of FIG. 7 provides the maximum number of iterations required of the inner loop of the procedure of FIG. 5. This corresponds to the maximum number of lower order bits necessary for addition to the antecedent before a contradiction, to the assertion that the two bits being verified are not equivalent, is found. This number is small, compared to the total number of bits in the multiplier, for all the multiplier sizes tested. Consequently, for each pair of bits verified, a relatively small portion of the multiplier circuits was traversed.

[0101] OPERATING CHARACTERISTICS

[0102] Based on the above results and analyses of the present invention, certain operating characteristics are expected of the present invention, particularly with respect to the verification of multiplier circuits.

[0103] Consider the case of verifying two multipliers, each with n bits for outputting the product, with the verification process proceeding from the 0^thoutput bits of each multiplier up to the n−1^thoutput bits of each multiplier. A characteristic utilization of computational resources (i.e., memory and/or time) is expected and illustrated in FIG. 9C. Specifically, proceeding from the 0^thbits of the two multipliers, up to about the middle bits (i.e., around the ½×(n−1) bits), the time and/or memory resources required for verifying each successively higher-order bit will increase. This is shown by the generally upward sloping segment 902 of the graph of FIG. 9C. After peaking at around these middle bits, the time and/or memory resources required for verifying each successively higher-order bit will tend to decrease until the last n−1^thoutput bit is reached. This is depicted in FIG. 9C as the generally downward sloping segment 903.

[0104] For certain circuit constructions, however, this characteristic can be expected to vary in a predictable manner. Consider, for example, the circuit of FIG. 9A. This circuit is a multiplier with a total of n−1 output bits. If such a circuit were to be verified, for example, against itself the present invention would be expected to exhibit a characteristic such as is shown in FIG. 9C.

[0105] Verifying the circuit of FIG. 9A against the circuit of FIG. 9B would result in a characteristic such as that shown in FIG. 9D. FIG. 9B represents a duplication of the circuit of FIG. 9A, except for the following changes.

[0106] Subcircuit η_(¾×n)is changed such that its inputs that were formerly driven by subcircuit η_(¾×n)−1are now driven by a subcircuit η′_(¾×n)−1. Each of the subcircuits η′₀to η′_(¾×n)−1is identical to the subcircuits η₀to η_(¾×n)−1except that the output functions, that drive z₀to z_(¾×n)−1in η₀to η_(¾×n)−1, have been removed. The subcircuits η′₀to η′_(¾×n)−1are connected to each other, and to the primary inputs, in an identical manner as subcircuits η₀to η_(¾×n)−1.

[0107] The verification of the circuit of FIG. 9A against the circuit of FIG. 9B proceeds as follows. Starting from a low, in terms of computational resources, when verifying z₀of FIG. 9A against z₀of FIG. 9B, the computational resources required for verifying each succeeding pair of output bits will increase until a maximum is reached at about bit ½×(n−1). This is the segment 904 of FIG. 9D. From about output bit (½×(n−1))+1 up until output bit (¾×n)−1, the characteristic will generally decrease, in terms of computational resources required, for each successive output bit. This is segment 905 of FIG. 9D. However, at output bit (¾×n) the computational resources required greatly increases by at least several times the previous peak that occurred around output bit ½×(n−1). This is due to the fact that the partitioning of the circuit of FIG. 9B according to structural dependency will put subcircuit η_(¾×n), and subcircuits η′₀to η′_(¾×n)−1, into a common and very large partition. In fact, if n is large enough, it would be expected for the computational requirements to become so large such that the verification of bit (¾×n) (or of any higher-order bit) becomes intractable. This would be expected to occur, for example, where n=64. Assuming that the computational resource requirements are still tractable, from output bit (¾×n) until output bit n−1 the computational resources required generally decrease. This is depicted by segment 906 of FIG. 9D.

[0108] It should be noted in the above discussion that where n is being multiplied by a fractional value it may be necessary to round the result to the nearest integer (either upwards or downwards) in order to refer to a particular output bit for a particular circuit.

[0109] HARDWARE ENVIRONMENT

[0110] Typically, the verification architecture of the present invention is executed within the computing environment (or data processing system) such as that of FIG. 8. FIG. 8 depicts a workstation computer 800 comprising a Central Processing Unit (CPU) 801 (or other appropriate processor or processors) and a memory 802. Memory 802 has a portion of its memory in which is stored the software tools and data of the present invention. While memory 803 is depicted as a single region, those of ordinary skill in the art will appreciate that, in fact, such software may be distributed over several memory regions or several computers. Furthermore, depending upon the computer's memory organization (such as virtual memory), memory 802 may comprise several types of memory (including cache, random access memory, hard disk and networked file server). Computer 800 is typically equipped with a display monitor 805, a mouse pointing device 804 and a keyboard 806 to provide interactivity between the software of the present invention and the chip designer. Computer 800 also includes a way of reading computer readable instructions from a computer readable medium 807, via a medium reader 808, into the memory 802. Computer 800 also includes a way of reading computer readable instructions via the Internet (or other network) through network interface 809. The software tools and data of the present invention may be stored as computer readable instructions on a computer readable medium, such as 807. The software tools and data of the present invention may also be transported into a computer system over a network and through a network interface, such as 809. Such network transmission may involve the use of a carrier wave.

[0111] While the invention has been described in conjunction with specific embodiments, it is evident that many alternatives, modifications and variations will be apparent to those skilled in the art in light of the foregoing description. Accordingly, it is intended to embrace all such alternatives, modifications and variations as fall within the spirit and scope of the appended claims and equivalents.