Polynomial Formal Verification of Multipliers.
Not long ago, completely automatical formal verification of multipliers was not feasible, even for small input word sizes. However, with Multiplicative Binary Moment Diagrams (&ast;BMD), which is a new data structure for representing arithmetic functions over Boolean variables, methods were proposed by which verification of multipliers with input word sizes of up to 256 Bits is now feasible. Unfortunately, only experimental data has been provided for these verification methods until now.In this paper, we give a formal proof that logic verification with &ast;BMDs is polynomially bounded in both, space and time, when applied to the class of Wallace-tree like multipliers. Using this knowledge online detection of design errors becomes feasible during a verification run.
Introduction
Verifying that an implementation of a combinational circuit
meets its specification is an important step in the design
process. Often this is done by applying a set of test-input
patterns to the circuit. With these patterns a simulation is
performed to ensure oneself in the correct behavior of the
circuit.
In the last few years new methods have been proposed
for a formal verification of circuits concerning the logic
function represented by the circuit, e.g. [1]. These methods
are based on Binary Decision Diagrams (BDDs). But
all these methods fail to verify some interesting combinational
circuits, such as multipliers, since all BDDs for the
multiplication function are exponential in size [5].
Recently, a new type of decision diagrams the Multiplicative
Binary Moment Diagram (*BMD) [2] has been
introduced. *BMDs are well suited for representing linear
arithmetic functions with Boolean domain. *BMDs have
been successfully used to verify the behavior of combinational
arithmetic circuits such as multipliers with input word
sizes of up to 256 bits [3].
Motivated by these results, several extensions of this
approach have been discussed [7], [6]. The verification
method of [3] is based on partitioning the circuit into components
with easy word-level specifications. First it is
shown, that the bit-level implementation of a component
Research supported by DFG grant Mo 645/2-1 and BE 1176/8-2
module implements correctly its word-level specification.
Then the composition of word-level specifications according
to the interconnection structure of the whole circuit is
derived. This composition is an algebraic expression for
which a *BMD is generated. Then the resulting *BMD
is compared with the one generated from the overall circuit
specification. A problem arising with this methodology
is the need of high-level specifications of component
modules. Taking this problem into account, Hamaguchi
et.al. have proposed another method for verifying arithmetic
circuits. They called their method verification by backward
construction [9]. This method does not need any high-level
information. In [9] only experimental data has been provided
to show the feasibility of their method for some specific
multiplier circuits.
In this paper, we give a formal proof that verification
by backward construction is polynomially bounded with respect
to the input word size. We do not consider a specific
multiplier circuit, but the class of Wallace-tree like multipli-
ers, e.g. [11], [10]. Additionally, we consider not only the
costs of intermediate results, but also the costs, that arise
during the synthesis operation on the *BMDs. This leads to
the possibility to interrupt the verification process in presence
of a design or implementation failure.
Furthermore we give classes of variable orders and we
give classes of depth-first and breadth-first orderings of the
circuit with that our tight bounds can be reached.
2. Multiplicative Binary Moment Diagrams
In this section, we give a short introduction how to represent
integer-valued functions by the proposed decision diagram
type *BMD. Details can be found in [2], [3].
*BMDs have been motivated by the necessity to represent
functions over Boolean variables having non-Boolean
ranges, i.e. functions f mapping
a Boolean vector onto integer numbers or onto rational
respectively. Here, we restrict ourselves to integer
functions.
For this class of functions the Boole-Shannon expansion
can be generalized with -
multiplication and addition re-
spectively. f - x is called the constant moment and f -
is called the linear moment of f with respect to variable
x (\Gamma denotes integer subtraction). Equation (1) is the
moment decomposition of function f with respect to variable
x.
*BMDs are rooted, directed, acyclic graphs with nonterminal
and terminal vertices. Each nonterminal vertex has
exactly two successors. The edges pointing to the successors
are named low- and high-edge and the successors themselves
are named low- and high-successor, respectively. The
nonterminal vertices are labeled with Boolean variables.
The terminal vertices have no successor and are labeled
with integer values. The low- (high-) edge of a nonterminal
node points to the constant (linear) moment of the
function represented by this node. The *BMD data structure
is reduced and ordered in the common way. Addition-
ally, a *BMD makes use of a common factor in the constant
and linear moment. It extracts this factor and places
it as a so called edge-weight on the incoming edge to the
node. This could lead to smaller representations. For ex-
ample, a *BMD with root vertex v labeled with x and
weight m on the incoming edge to v represents the function
In the following, we
denote the node v, labeled with a variable x simply as node
x, if the context is clear.
In this paper, we will consider integer edge-weights
and integer values of terminal vertices since we are interested
in integer linear functions only. To make the *BMD-
representation canonical, a further restriction on the edge-weights
is necessary. The edge-weights on the low- and
high-edge of any nonterminal vertex must have greatest
common divisor 1. Additionally, weight 0 appears only as a
terminal value, and if either outgoing edge of a node points
to this terminal node, the weight of the other outgoing edge
is 1. Note that because of reduction a terminal node with
value 0 can not appear at a high-edge.
2.1. Basic Operations on *BMDs
We now present in detail an algorithm, which is the basis
for verification by backward construction. The method of
backward construction is based on substituting variables in
a *BMD for a function f by a *BMD for another function
g. According to Equation (1), this substitution is based on
the
x .
A sketch of the substitution algorithm can be seen in Figure
1. It starts with a *BMD(f) and a *BMD(g), which is
a notation for the *BMD representing the function f and
g, respectively. Additionally, the variable x that is to be
substituted, is handed to the algorithm. If the top variable
of *BMD(f) is not the variable to be substituted, the
algorithm calls itself recursively with the low- and high-
successor. If the variable x is found, an integer multiplication
and an integer addition is performed (line 3). Note that
both operations have exponential worst case behavior [8].
In the following we show, that under specific conditions,
the worst case will not occur. The key to this is a *BMD
with a specific structure, which we call Sum Of weighted
Variables (SOV). The *BMD for the unsigned integer encoding
a is an example of a *BMD
in SOV-structure. Its outline is given in Figure 2. Such
subst( *BMD(f), x/*BMD(g) )f
1 check for terminal cases;
return

Figure

1. Substitution algorithm

Figure

2. SOV-structure
a *BMD has the properties that there is exactly one nonterminal
node for each variable and the high-edge of each non-terminal
node is labeled with weight 1 pointing directly to
a terminal node labeled with the value of the corresponding
variable. Because of these properties the substitute algorithm
simplifies considerably: Let us assume f is a *BMD
in SOV, g is a *BMD not in SOV and the variable x is at an
arbitrary position in the middle of f . In a first phase lines
and 4 are in the middle of f . In a first phase lines 2 and
4 are executed continually until x is reached. Line 3 calls
a multiplication and an addition. The multiplication returns
its result immediately since high(f) is a terminal node. The
complexity of the addition depends on the *BMDs f and g.
But again, the SOV-structure reduces the number of execution
steps, since f -
y is a terminal node for all variables y.
Later on in the paper g will be a *BMD of known size, so
we can give a more detailed analysis. Returning from the recursive
calls of line 4, line 5 does no recursive calls because
of high(f). For the same reason line 7 ends immediately
and the *BMD E4 in line 8 has a depth of 1.
For these reasons, maintaining the SOV-structure as long
as possible reduces the number of execution steps of the
substitute algorithm. Since substitution is the basic operation
in the method of verification by backward construction
the overall number of execution steps reduces considerably,
too. In addition, the SOV-structure simplifies the analysis
of the complexity of the method extremely.
3. The Class of Wallace-Tree like Multipliers
Let be two n-bit
numbers binary representation. (If n
is not a power of 2 extend n to a power of 2 and set
the superfluous inputs to zero.) The multiplication of a
and b is then equivalent to summing up n partial products
shifted by j positions to the left
for We assume in the following, that we
can divide the circuit into two parts. One part calculates the
partial product bits a i 1. The other
part adds these partial products bits to the final result using
(only) fulladder-cells. How these cells are arranged, e.g. as
a 3to2 or as a 4to2 reduction, as a binary tree or as a linear
list, has no influence on the proof.
For a more detailed description of representatives of
Wallace-tree like multipliers please see [10], [4].
4. Complexity of Backward Construction
In this section we analyze the complexity of the method
of verification by backward construction, as introduced in
[9]. In Subsection 4.1 we explain the principles of the
method. In Subsection 4.2 the backward construction of the
*BMDs for the adder part of the circuit is analyzed. In Sub-section
4.3 we take the partial product bits into account and
discuss the resulting complexity. In the last subsection we
put together these parts to get the final overall complexity.
4.1. The Method of Backward Construction
In general, the method of verification by backward construction
works as follows: First, to each primary output a
distinct variable is assigned. In the next step the *BMD for
the output word is constructed by weighting and summing
up all *BMDs of these variables according to the given output
encoding. (We assume an unsigned integer encoding of
the outputs.) Note, that we obtain the SOV-structure for the
resulting *BMD. Then, a cut is placed, crossing all primary
outputs of the circuit. The cut is moved towards the primary
inputs, such that the output lines of each gate move onto the
cut according to some reverse topological order of the gates.
While moving the cut towards the primary inputs of the cir-
cuit, the *BMD is constructed as follows: For the next line
of the circuit crossing the cut, which is also an output line
of some gate of the circuit, find its corresponding variable
in the *BMD constructed so far. Substitute this variable by
the (output) function of the gate, delete the output line from
the cut, and add all input lines of the gate to the cut. Fi-
nally, the cut has been moved to the outputs of AND gates,
computing the partial product bits. The very final step is
the substitution of corresponding variables in the obtained
*BMD by the partial product bits. After this step, we obtain
the *BMD representing the multiplication of a and b if
the circuit is correct. As mentioned above, the cut is moved
according to a reverse topological order of the gates. In
general, there exists more than one such order. As we shall
see, our proofs are not based on the knowledge of a specific
reverse topological order, as long as we substitute the variables
representing the fulladder outputs before the variables
representing the initial partial product bits. Nevertheless,
we can give one specific class of variable orders, for that
our statements hold even if we apply a different topological
order.
4.2. Constructing the *BMD for the Adder
Part
In this subsection we analyze the costs of constructing
the *BMD for the adder-part of the multiplier. The
first lemma shows, that the substitution of the sum- and
carry-output of the same fulladder in a *BMD in SOV
maintains the SOV-structure. This means, that SOV is invariant
against these substitutions. For that reason, we
have to analyze the substitution costs for a single fullad-
der (Lemma 4.2) to get the overall costs (Theorem 4.1 and
Theorem 4.2).
Lemma 4.1 Let F be a *BMD in SOV and let X denotes
the set of variable of F . Let x be two variables in
representing the sum- and carry-output of the same
fulladder. The inputs to the fulladder are represented by
. Independent of the order on the variable
sets of the *BMDs involved in the substitution process, it
holds that substituting x F by the *BMDs for the
functions
and:
1. F 0 is in SOV.
2. The terminal value of the high-successors of the nodes
for is the same as that for the high-
successor of the node for x i in F .
Proof: The proof is based on a merely functional argu-
ment. For the sum- and carry-output we get the following
functions:
\Gamma2x l xm
by expressing the boolean operations \Phi and - by integer
addition, subtraction and multiplication, i.e., x \Phi
Let the variables x in the *BMD F represent the
sum- and carry-output of the same fulladder. These variables
have weights w and 2w, respectively. The substitution
of x
yields the following function f 0
as can easily be verified. The rest of the variables in f are
not affected since x k ; x l ; xm 62 X and the weighted variables
only once in f . Therefore the *BMD
representing function f 0 , must be in SOV again, independent
of the variable order. Furthermore all three high-
edges of the nodes for x k ; x l ; xm in F 0 point to a terminal
node with value w. This completes the proof. 2
Lemma 4.1 we can be sure, that the SOV-structure
of the *BMD is maintained, if we have fulladders as basic
cells and if we substitute the variables corresponding to both
outputs of a particular fulladder directly one after another.
This is independent of the chosen variable order and the
chosen reverse topological order of the DAG representing
the adder part of the multiplier. Additionally, at each point
of the substitution process, we know exactly the size of the
x
x

Figure

3. Representation of substituting x i by
Su and x j by Ca.
x
x

Figure

4. *BMD after substitution of variable
*BMD: After having processed the next fulladder, the size
is increased by one.
We proceed now with calculating the costs by counting
the calls of the substitute algorithm.
Lemma 4.2 Let F be a *BMD in SOV with size
defined as in Lemma 4.1. Substituting
is bounded by O(jF with respect to time, independent of
the variable order or order of substitutions.
Proof: We denote the *BMDs for
by Su and Ca. We consider first the
substitution of x i by Su. The substitution process can
be visualized in Figure 3. (Note that the order between
does not matter because the sum- and carry-
function are totally symmetric. Therefore, the nonterminal
node labels are omitted.) The substitute-algorithm calls itself
recursively until it reaches the node in F labeled with
variable x i . Obviously, the number of recursive subst-calls
is bounded by O(jF j). At the node labeled with x i , the
operation F low(x has to be carried out,
the *BMDs to which the
low- and high-edge of node x i point. Since F is in SOV,
F high(x i ) is a terminal node and the call to mult ends im-
mediately. Since F low(x i ) is in SOV, too, and Su is of constant
size, the addition is bounded by O(jF j). For all other
recursive subst-calls, there will be only a constant number
of mult- and add-calls because of the SOV-structure, as
can easily be verified. We get an overall bound of O(jF
for the substitution of x i by Su. The *BMD after this
substitution can be seen in Figure 4 for a variable order
For the substitution of x j by Ca, analogous arguments
hold, except for the fact, that the SOV-structure of F is destroyed
by Su (see Figure 4). First of all, this leads to some
additional recursive subst-calls. But this will be only a constant
because Su has constant depth. Furthermore,
we get some additional calls to add and mult during some
of the recursive subst-calls, when the nodes labeled with
variables x k ; x l ; xm meet each other. But this number is
bounded by a constant value too, since Su and Ca have
constant depth.
Therefore, since the resulting *BMD is of size jF j
according to Lemma 4.1, we get a time bound of O(jF
the substitution of x i by Su and x j by Ca independent of
the variable order on X and (X n fx g.
The proof for first substituting x j by Ca and then x i by Su
is analogous. 2
Lemma 4.1 and 4.2 leads directly to the space bound for
the construction of the *BMD for the adder part.
Theorem 4.1 Constructing the *BMD for the adder part of
the multiplication circuit using substitution is bounded by
respect to space. This is independent of the
chosen reverse topological order for the fulladder-cells.
Proof: The *BMD F 0 with which we start has size O(n)
as follows since there is one nonterminal node for each variable
representing a primary output. The resulting *BMD
constructed for the adder-part has size O(n 2 One nonterminal
node for each variable representing an initial partial
product bit. The exact size depends on the chosen realization
of the multiplier. With Lemma 4.1 and 4.2 we have the
space bound O(n 2 ). 2
After analyzing the space requirements for the substitu-
tions, we now consider the time requirements.
Theorem 4.2 Constructing the *BMD for the adder-part
using substitution is bounded by O(n 4 ) with respect to time,
independent of the chosen reverse topological order for the
fulladder-cells.
Proof: For the proof we first count the number of ful-
ladder elements. Depending on the realization, the exact
number of these elements differs. Asymptotically there are
cells, forming the adder-part of any
meaningful multiplier. Therefore the number of execution
steps has an upper bound of
the size of the initial *BMD according to the proof of Theorem
4.1. This sum is figured out as follows:
with
4.3. Substitution of the Partial Products
Up to this point we analyzed the complexity of the
method of verification by backward construction for the part
of the multiplier circuit that adds the initial partial product
bits to obtain the result of the multiplication. In the sequence
we analyze the costs of the final step, substituting
the partial product bits into the *BMD. By doing so, we

Figure

5. *BMD after substituting some partial
product bits.

Figure

6. Final *BMD for the multiplication.
will destroy the SOV-structure of the *BMD. Our starting
point is the *BMD constructed up to the outputs of the AND
gates. It has size m since there are n 2 partial
product bits. In fact, it holds
with m from the proof of Theorem 4.2 and with #FA denoting
the number of fulladder cells.
We assume in the following a fixed order among the aand
b-word, assigned to the primary inputs of the circuit. In
fact, the variable order within the a i and b j is of no interest
as long as all variables forming one input word are before
the variables forming the second input word. Otherwise the
final *BMD may be larger than 2n [2].
We define a low-path of a *BMD F as the path in F from
the root to a leaf, consisting of only low-edges. Note, that
there is only one such path in a *BMD.
We now show, that the intermediate *BMDs have a structure
like that in Figure 5. (The small box on an edge denotes
the multiplicative factor.) All nodes with a terminal
high-successor in the upper diagonal line, the low-path,
are marked with a variable x k , assigned to a fulladder input
line. These lines are also output lines of AND gates.
Nodes with a nonterminal high-successor are labeled with
a variable a i (also in the low-path). The high-successors of
them are labeled with a variable b j . These are located in the
lower diagonal line. The final *BMD is structured as shown
in

Figure

6.
Theorem 4.3 Let F be the *BMD constructed for the adder
part. Substitution of the variables of F by the *BMDs for
the initial partial product bits a i \Delta b j is bounded by O(n 2 )
with respect to space and O(n 4 ) with respect to time independent
of the variable order in F and independent of the
chosen reverse topological order for the AND gates.
Proof: Let F 0 denote an intermediate *BMD generated after
the substitution of some initial partial product bits. If the
node labeled with variable x has not yet been substituted, it
must be on the low-path of F 0 . Now we consider the substitution
of node x by the *BMD for an initial partial product
bit a i Obviously, the number
of recursive calls to the substitute algorithm (Figure 1) is
bounded by O(jF 0 j). During the last of the recursive subst
calls, i.e., at node x, the following operations have to be
carried out:
The call to mult ends immediately, since x has a terminal
high-successor because of the SOV-structure of F at the beginning
of the substitution process. For the add calls we
have to distinguish two different cases.
1. No nodes have been substituted by initial partial products
bits with variable a i until now. Since node x (one non-terminal
node) has to be substituted by \LambdaB MD(a i
nonterminal nodes) the size of F 0 increases by 1 if no node
for variable b j can be shared, and it remains unchanged otherwise

If variable a i comes after the predecessor of variable x in
the variable order, \LambdaB MD(a i reaches its final position
in *BMD F 0 by calls to add during the final substitute call,
i.e.line 3 of Figure 1. The number of these calls is obviously
bounded by O(jF 0 j).
If variable a i comes before the predecessor of variable x
in the variable order, a i reaches its final position in *BMD
F 0 by calls to add during resolving previous substitute calls
(line 8 of Figure 1). The number of these add calls is con-
stant, as one can easily make sure. Furthermore, there is
one call to MakeNode and one call to mult for each of the
previous subst calls (lines 6 and 7 of Figure 1).
2. There exists already a node for variable a i , i.e., some
nodes of F have already been substituted by initial partial
product bits a i
so far. If there exists also a
node for b j , e.g. created during the substitution of an initial
partial product bit a l \Delta b j , the size of F 0 during the substitution
may decreases by 1, if the node b j can be shared, or
remains unchanged, otherwise.
The only difference to the first case is, that there are an
additional number of at most n add calls, because of the
position of b j in the variable order among the b i 1
(the worst case occurs, if b
we have a bound on the total number
of calls of O(jF
Cases 1 and 2 together give a bound on the total number
of algorithm calls of O(jF 0 j) for the substitution of node x
by \LambdaB MD(a i we have at most an increase
of n in the size of the starting BMD F (the first n initial
partial product bits of the substitution process all have different
a-variables) and the size of F is O(n 2 ), the size of
the intermediate *BMDs during substitution is bounded by
This proves the first part of the theorem. Fur-
thermore, since the number of substitutions is bounded by
and the size of the starting *BMD F is O(n 2 ) we
get an overall time bound of
This proves the second part of the theorem and we have
completed the proof. 2
4.4. Complexity of Backward Construction
With Theorema 4.1, 4.2 and 4.3, we conclude, that the
method of backward construction applied to the class of
Wallace-tree like multipliers is bounded by O(n 2 ) with respect
to space and by O(n 4 ) with respect to time. These
bounds do (largely) not depend on the chosen variable order
during the single substitution steps. Additionally, these
bounds do also not depend on the order of substitutions as
long as we first substitute all fulladder-cells and afterwards
the initial partial product bits.
If we allow one further restriction on the variable order-
ing, we attain to be totally free in the substitution ordering
across both circuit parts. This means, there is a class of
variable orders, with that we can substitute an initial partial
product bit before having processed all fulladder cells.
Nevertheless, the complexity remains polynomial. We only
have to regard the reverse topological order over the whole
multiplier circuit.
We define an (x; a; b) variable order to be any variable
order, which has at first all x-variables, at second all a-
variables and at third all b-variables The x-variables denote
the fulladder in- and outputs and the a- and b-variables denote
the variables of the input words to the multiplier. Then
we can give the following theorem:
Theorem 4.4 Given an (x; a; b) variable order, the method
of backward construction, applied to the class of Wallace-
tree like multipliers, is bounded by O(n 2 ) with respect to
space and O(n 4 ) with respect to time independent of the
reverse topological order on the circuit.
Proof: The *BMD decomposes into two parts. The upper
part consists of x-variables only, and is in SOV. (Despite the
fact, that the last high-edge points to a nonterminal node,
labeled with an a-variable.) The lower part consists of aand
b-variables. We have to consider two cases:
1. Substituting Su (Ca), we first have to find the substituted
variable. That will be found in the upper part of
the *BMD. Depending on the variable ordering within
the x k , the add operation of the substitution continues
downward the *BMD. Maximally, it reaches the
edge, pointing to a 0 (respectively any a i , which ever
is the 'smallest' a-variable so far). There, the recursive
calls terminate, since x k ! a i , for all k; i. Theo-
rema 4.1, 4.2 can be applied for the costs, considering
only the size of the upper part of the *BMD.
2. Substituting a partial product, Theorem 4.3 can be applied
One open problem is the complexity if we allow, that initial
partial product bits are substituted before all fulladder-
cells are processed, but with a different variable order as
that from Theorem 4.4, i.e., not all x-variables are at the
beginning of the variable order. We expect, that the complexity
remains still polynomial, since the structure of the
resulting *BMD is similar to the one used here.
5. Conclusions and Future Research
In this paper we analyzed the complexity of the method
of verification by backward construction applied to the class
of Wallace-tree like multipliers. We gave a formal proof of
polynomial upper bounds on run-time and space requirements
with respect to the input word sizes for that method.
Note, that until now, only experimental data has been given
to show the feasibility of the method.
A conclusion of our results is, that we can prematurely
detect design errors by watching the *BMD, if these errors
result in non correct *BMD sizes. Assume, we have processed
only gates in the adder-part of the circuit. After processing
the ith gate the *BMD has size jF If the
actual *BMD has not that size, there is an error. Assume
now, that we considered at least some initial partial product
bits of the circuit. Then, the size of the *BMD depends on
which initial partial product bits have been substituted. Not
considering an accurate size bound, the *BMD must not be
larger than jF 0 j +#FA+n or smaller than 2n, at any time.
Future research directions are to remove the restrictions,
e.g. for variable order we mentioned above, and take a look
at integer dividers, which could not be verified by backward
construction so far.



--R

HSIS: A BDD-Based Environment for Formal Verification
Verification of Arithmetic Functions with Binary Moment Diagrams.
Verification of Arithmetic Circuits with Binary Moment Diagrams.
An Easily Testable Optimal-Time VLSI- Multiplier
On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication.
Hybrid Decision Diagrams - Overcoming the Limitations of MTBDDs and BMDs

Note on the Complexity of Binary Moment Diagram Representations.
Efficient Construction of Binary Moment Diagrams for Verifying Arithmetic Cir- cuits
Recursive Implementation of Optimal Time VLSI Integer Multipliers.
A suggestion for a fast multiplier.
--TR
Graph-based algorithms for Boolean function manipulation
On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication
Sequential circuit verification using symbolic model checking
Symbolic Boolean manipulation with ordered binary-decision diagrams
HSIS
Verification of arithmetic circuits with binary moment diagrams
Efficient construction of binary moment diagrams for verifying arithmetic circuits
Hybrid decision diagrams
PHDD
Logic Synthesis and Verification Algorithms
K*BMDs
Verification of Arithmetic Functions with Binary Moment Diagrams
integer multipliers;formal verification;equivalence checking;backward construction;multiplicative binary moment diagrams