Hybrid decision diagrams.
Abstract: Functions that map boolean vectors into the integers are important for the design and verification of arithmetic circuits. MTBDDs and BMDs have been proposed for representing this class of functions. We discuss the relationship between these methods and describe a generalization called hybrid decision diagrams which is often much more concise. We show how to implement arithmetic operations efficiently for hybrid decision diagrams. In practice, this is one of the main limitations of BMDs since performing arithmetic operations on functions expressed in this notation can be very expensive. In order to extend symbolic model checking algorithms to handle arithmetic properties, it is essential to be able to compute the BDD for the set of variable assignments that satisfy an arithmetic relation. In our paper, we give an efficient algorithm for this purpose. Moreover, we prove that for the class of linear expressions, the time complexity of our algorithm is linear in the number of variables.
Introduction
Functions that map boolean vectors into the integers are important for the design and verification
of arithmetic circuits. In this paper, we investigate how to represent and manipulate
such functions efficiently. In a previous paper [6], we have proposed two ways (MTBDDs
and BDD arrays) for representing this class of functions using Binary Decision Diagrams.
Recently, Bryant and Chen [4] have proposed Binary Moment Diagrams (BMDs) for representing
this class of functions. In this paper, we show that the BMD of a function is the
MTBDD that results from applying the inverse Reed-Muller transformation [9] to the func-
tion. Furthermore, it can be computed using the techniques that we have developed. The
transformation matrix in this case is the Kronecker product [2] of a number of identical 2 \Theta 2
matrices. We show that the Kronecker products of other 2 \Theta 2 matrices behave in a similar
way. In fact, the transformations obtained from Kronecker products of other matrices will
in many cases more concise than the BMD. We have further generalized this idea so that the
transformation matrix can be the Kronecker product of different matrices. In this way, we
obtain a representation, called the Hybrid Decision Diagram (HDD), that is more concise
than either the MTBDD or the BMD.
A similar strategy has been used by Becker [7]. However, his technique only works for
the boolean domain and is not suitable for functions mapping boolean vectors into integers.
When using his technique, all of the transformation matrices, the original function and the
resulting function must have boolean values. Our technique, on the other hand, works over
the integers. By allowing integer values, we can handle a wider range of functions. Moreover,
we can obtain larger reduction factors since we have more choices for the transformation ma-
trices. When our technique is applied to boolean functions, it can often achieve comparable
and sometimes better results than dynamic variable reordering. Thus, in some cases, it can
serve as an alternative to dynamic variable reordering. We conjecture that a combination of
both techniques together may result in reductions that neither technique can achieve alone.
One of the main limitations of Bryant and Chen's work is that performing arithmetic operations
on functions represented by BMDs is very expensive. We show how these operations
can be implemented not only for BMDs, but for hybrid decision diagrams as well. Although
the worst case complexity of some of these operations is exponential, our algorithms work
quite well in practice. In addition, we show how logical operations can be performed on
hybrid decision diagrams that are used to represent boolean functions.
Most of the properties that we want to verify about arithmetic circuits can be expressed
as arithmetic relations. In order to extend symbolic model checking algorithms [5] to handle
properties, it is essential to be able to compute the BDD for the set of variable
assignments that satisfy a relation. Bryant and Chen do not provide an algorithm for this.
In this paper, we give an efficient algorithm for this purpose. Moreover, we prove that
for the class of linear expressions, the time complexity of our algorithm is linear in the
number of variables. Our techniques for handling arithmetic operations and relations are
used intensively in the verification of a SRT division algorithm similar to the one that is
used in the Pentium.
Our paper is organized as follows: Section 2 gives the basic properties of MTBDDs
that are used in the remainder of the paper. In particular, this section shows how matrix
operations can be implemented. Section 3 describes the relationship between BMDs and the
inverse Reed-Muller transformation. This section also introduces Kronecker product and
shows how it can be used to generalize BMDs. The next section introduces hybrid decision
diagrams and provides experimental evidence to show the usefulness of this representation.
Sections 5 and 6 are the main sections of the paper. In Section 5, we show how arithmetic
operations can be implemented. In Section 6, we give an efficient algorithm for computing the
set of assignments that satisfy an arithmetic relation expressed in terms of hybrid decision
diagrams. The paper concludes in Section 7 with a brief summary and a discussion of
directions for future research.
2. Multi-terminal binary decision diagrams
Ordered binary decision diagrams (BDDs) are a canonical representation for boolean formulas
proposed by Bryant [3]. They are often substantially more compact than traditional
normal forms such as conjunctive normal form and disjunctive normal form. They can also
be manipulated very efficiently. Hence, BDDs have become widely used for a variety of
CAD applications, including symbolic simulation, verification of combinational logic and,
more recently, verification of sequential circuits.
A BDD is similar to a binary decision tree, except that its structure is a directed acyclic
graph rather than a tree, and there is a strict total order placed on the occurrence of
variables as one traverses the graph from root to leaf. Algorithms of linear complexity exist
for computing BDD representations of :f and f g from the BDDs for the formulas f and g.
Z be a function that maps boolean vectors of length m into integers.
Suppose are the possible values of f . The function f partitions the space B m
of boolean vectors into N sets fS g, such that S
g. Let f i be
the characteristic function of S i , we say that f is in normal form if f (x) is represented as
This sum can be represented as a BDD with integers as its terminal nodes.
We call such DAGs Multi-Terminal BDDs (MTBDDs) [6, 1].
Any arithmetic operation fi on MTBDDs can be performed in the following way.
We now give an efficient algorithm for computing f(x) fi g(x).
ffl If f is a leaf, then for each leaf of g, apply fi with f as the first argument.
'i
'i
Z Z Z
Z Z~
ae
ae
ae
ae
ae=
Z Z Z
Z Z~
ae
ae
ae
ae
ae=
f
100

Figure

1: BDDs for f and g
'i
Z Z
Z Z Z~
ae
ae
ae
ae
ae=
'i
Z Z
Z Z Z~
ae
ae
ae
ae
ae=
'i
Z Z
Z Z Z~
ae
ae
ae
ae
ae=

Figure

2: BDD of f fi g
ffl If g is a leaf, then for each leaf of f , apply fi with g as the second argument.
Otherwise, f and g have the form in Figure 1, and the BDD for f fi g, depending on
the relative order of x i and x j , is given in Figure 2.
The resulting diagram may not be in normal form. In order to convert it into normal form,
a reduction phase is needed. The algorithm for this phase is essentially identical to the
reduction phase in Bryant's algorithm for constructing BDDs [3] .
Let M be a 2 k \Theta 2 l matrix over Z. It is easy to see that M can be represented as a
Z, such that
y), where  x is the bit vector for i and
y is the bit vector for j. Therefore, matrices with integer values can be represented as
integer valued functions using the representation shown above. We can also perform various
matrix operations using MTBDD representation. In particular, matrix multiplication can
be computed in the following way: Suppose that two matrices A and B have dimensions
B be the product of A and B, then C will
have dimension 2 k \Theta 2 m . If we treat A and B as integer-valued functions, we can compute
the product matrix C as
y
where
y means "sum over all possible assignments to
y". In practice,
y M(x;
y) can be
computed as:
In this way, each variable in
y is eliminated by performing an addition. Although this
operation works well in many cases, the worst case complexity can be exponential in the
number of variables.
Such integer functions can also be represented as arrays of BDDs. These BDDs have
boolean values and each of them corresponds to one bit of the binary representation of the
function value. In general, it is quite expensive to perform operations using this representation

3. Kronecker transformations
Recently, Bryant and Chen[4] have developed a new representation for functions that map
boolean vectors to integer values. This representation is called the Binary Moment Diagram
(BMD) of the function. Instead of the Shannon expansion use
the expansion is equal to f After merging the common
subexpressions, a DAG representation for the function is obtained. They prove in their
paper that this gives a compact representation for certain functions which have exponential
size if represented by MTBDDs directly.
There is a close relationship between this representation and the inverse Reed-Muller
transformation [9]. The matrix for the inverse Reed-Muller transformation is defined recursively
by
\GammaS
which has a linear MTBDD representation. Let be the binary representation of
can be represented as a column vector
where the value of the ith entry is f(i). We will not distinguish between a function and its
corresponding column vector. The inverse Reed-Muller transformation can be obtained by
multiplying the transformation matrix and the column vector b
using the technique
described in previous section.
Theorem 1 The MTBDD of b
f is isomorphic to the BMD of f .
Proof: The theorem is easy to prove by induction on the number of variables.
Base Case: If the number of variables is 0, the function is a constant and b
. Both the
MTBDD of b
f and the BMD for f are terminal nodes and therefore isomorphic.
'i
'i
'i
@
@
@R
\Gamma\Psi
x n0 \GammaS n\Gamma11 00
'i
'i
\GammaS
\GammaS n
'i
@
@
@R
\Gamma\Psi

Figure

3: MTBDD for S n
Induction Step: Let . The roots of both the BMD for f and the MTBDD
for b
f are x n . The left child of the root of the BMD for f is the BMD for f j xn=0 , while
the right child is the BMD for f j When f is represented as a column vector,
the upper half is f j xn=0 and the bottom half is f j xn=1 . The inverse Reed-Muller matrix is
\GammaS
. The result of the transformation is therefore:
\GammaS
\Theta
If this vector is represented by MTBDD, the left child is the MTBDD for the inverse Reed-Muller
transform of f j xn=0 and the right child is the MTBDD for the inverse Reed-Muller
transform of f . By induction hypothesis, both children are isomorphic to the
children of the root of the BMD for f . Therefore the BMD of f is isomorphic to the MTBDD
for b
f .
The Kronecker product of two matrices is defined as follows:
a 11 . a 1m
a n1 . anmC C
a 11 B . a 1mB
a
The inverse Reed-Muller matrix can be represented as the Kronecker product of n identical
matrices:
\GammaS
!\Omega
!\Omega
-z
The inverse Reed-Muller transformation is not unique in this respect. Other transformations
that are defined as Kronecker products of 2 \Theta 2 matrices may also provide concise
representations for functions mapping boolean vectors into integers. In particular, Reed-Muller
matrix R n and Walsh matrix W n can be represented as Kronecker products shown
below:
R
R
!\Omega
-z
and
W
!\Omega
!\Omega
-z
Although a Kronecker transformation can be performed by matrix multiplication, there
is a more efficient way of computing it. It is a well known property of the Kronecker product
that
O
Y
i\Gamma1\Omega A
where each A i is a 2 \Theta 2 matrix and I k is the identity matrix of size k \Theta k. A transformation
of the form (I 2
i\Gamma1\Omega A
i\Omega I 2 k\Gammai ) is called a basic transformation. Let A
a 00 a 01
a 10 a 11
and let g be a function represented as a MTBDD, then the basic transformation
i\Gamma1\Omega A
can be computed as
As a result of this observation, the Kronecker transformation can be performed by a series of
basic transformations. Moreover, it can be proved that the order of the basic transformations
does not affect the final result.
In fact, the Kronecker product of any non-singular 2 \Theta 2 matrices can be used as a
transformation matrix and will produce a canonical representation for the function. If the
entries of the 2 \Theta 2 matrix are restricted among f0; 1; \Gamma1g, there are six interesting matrices
All other matrices are either singular or would produce BDDs that are isomorphic to one of
the six matrices.
We have applied these transformations to the functions discussed in paper[4]. The transformation
can be partitioned into two groups of three each. The MTBDDs of the results
after applying the transformations in the same group have the same complexity.
base
For example, the complexity of XY after the Kronecker transform with base matrix
can be obtained from the complexity of a more general formula
c)
d) where c i and d j are constants. We can prove that the resulting MTBDD
size for this formula after the transformation does not exceed 2nm+2n+2m+1 by induction
on the number of total variables. The base case when there are no variables is trivial. For
simplicity, let's suppose x n is the top variable. Then the right child should be the transformed
MTBDD for
By induction hypothesis, the size for the left child does not exceed 2m + 1. In a similar
manner, we can show the left child is the transformed MTBDD for
By induction hypothesis, the size does not exceed 2(n
Therefore the total size of the transformed BDD has an upper bound of (2nm
The possibility of using BMDs to represent boolean functions is discussed in [4]. In gen-
eral, the BMD does not appear to be better than the ordinary BDD for representing boolean
functions. In order to see why this is true, consider the boolean Reed-Muller transformation,
which is sometimes called the Functional Decision Diagram or FDD[8]. This transformation
can be obtained by applying the modulo 2 operations to all of the terminal nodes of the
BMD. Consequently, the size of FDD is always smaller than the size of the BMD. Since the
inverse boolean Reed-Muller transformation is the same as the boolean Reed-Muller trans-
formation, the FDD of the FDD is the original BDD. Therefore, for every function f such
that jFDD f j ! jBDD f j, there exists another function f 0 which is the boolean Reed-Muller
transform of f such that jBDD f In particular, both the BMD and the FDD
representations for the middle bit of a multiplier are still exponential.
4. Hybrid decision diagrams
In the previous sections, we have discussed transformations that can be represented as the
Kronecker product of a number of identical 2 \Theta 2 matrices. If the transformation matrix is
a Kronecker product of different 2 \Theta 2 matrices, we still have a canonical representation of
the function. We call transformations obtained from such matrices hybrid transformations.
A similar strategy has been tried by Becker [7]. However, his technique only works for the
boolean domain. When using his technique, all of the transformation matrices, the original
function and the resulting function must have boolean values. Our technique, on the other
hand, works over the integers. By allowing integer values, we can handle a wider range of
functions. Moreover, we can obtain larger reduction factors since we have more choices for
transformation matrices.
We can apply this idea to reduce the size of BDD representation of functions. Since
there is no known polynomial algorithm to find the hybrid Kronecker transformation that
minimizes BDD size, we use a greedy algorithm to reduce the size. If we restrict the entries
in the matrix to the set f0; 1; \Gamma1g, then there are six matrices we can try. For each variable,
we select the matrix that gives the smallest BDD size. The BDDs obtained from such
transformations are called Hybrid Decision Diagrams (HDDs). We have tried this method
on the ISCAS85 benchmark circuits. In some cases we have been able to reduce the size
of BDD representation by a factor of 1300. However, reductions of this magnitute usually
occur when the original function has a bad variable ordering. If dynamic variable ordering
is used, then our method gives a much smaller reduction factor.
example circuit without reordering with reordering
circuit jinputj output jBDDj jBMDj jHDDj jBDDj j BMD j jHDDj

Table

1: Experimental results for hybrid transformations of some ISCAS85 circuits
We have tried several techniques to increase the number of possible matrices. The first
technique involves increasing the number of entries in the matrices. This can be accomplished
by allowing the entries to take larger values or by using the complex numbers
1g. Unfortunately, neither extension improved the
results significantly.
The second technique involves using transformation matrices that are Kronecker products
of larger matrices. For example, we have tried hybrid Kronecker transformations based on
4 \Theta 4 matrices instead of 2 \Theta 2 matrices. Although we have been able to reduce the BDD
size even further using this technique, the time it takes to find such transformations is much
bigger since the number of possibilities is considerably larger.
Note that our technique can achieve comparable and sometimes better results than dynamic
variable reordering. Thus, in some cases, it can serve as an alternative to dynamic
variable reordering. We conjecture that the combination of both techniques together may
result in reductions that neither technique can achieve alone.
5. Arithmetic operations on hybrid decision diagrams
In order to make the techniques described in the previous sections more useful, it is desirable
to be able to perform various arithmetric operations on on hybrid BDDs. In this paper, we
only consider the cases of addition and multiplication of two integers.
Suppose that f is transformed into f 0 by the matrix T 1 and g is transformed into g 0 by
the matrix T 2 using the techniques discussed in the previous sections. Scalar multiplication
is simple to perform.
When finding the sum of two function is also simple.
the transformation applied to the sum must be determined first. Suppose we use
as the transformation matrix for the result,
Next, we consider how to perform multiplication. We choose T 2 as the transformation
matrix for (f \Delta g). Suppose the top level variable is x i . Assume the top level transform for
f is
a 11 a 12
a 21 a 22
with inverse
a 0
11 a 0a 0a 0!
. Assume also the top level transform for g is
with inverse
. Then
!\Omega
b
b
'i
'i
Z Z Z
Z Z~
ae
ae
ae
ae
ae=
Z Z Z
Z Z~
ae
ae
ae
ae
ae=00
l f 0
l
r

Figure

4: BDDs for f 0 and g 0
'i
Z Z
Z Z Z~
ae
ae
ae
ae
ae=0
l (f \Delta g) 0
r

Figure

5: BDD of (f \Delta g) 0
b
b
\Theta
Consequently,
(b 11 a 0
(b 11 a 0
22
+(b 11 a 0b 0+ b 12 a 0b 0)(f r \Delta g l
22
(b 21 a 0
(b 21 a 0
22
+(b 21 a 0b 0+ b 22 a 0b 0)(f r \Delta g l (b 21 a 0b 0+ b 22 a 0b 0)(f r
Since both (f \Delta g) 0
l and (f \Delta g) 0
r can be computed in term of (f l \Delta
, we can compute the transformation of the product in a recursive manner. If we
store these intermidiate results, the total number of recursive calls to compute (f \Delta g) 0 will
be at most jf 0 jjg 0 j. Because of the additions that are needed in the computation, the worst
case complexity can still be exponential. However, in practice, this algorithm works quite
well. As an example, in Table 2, we show the time it takes to compute the hybrid decision
diagram for (
from the hybrid decision diagrams for (
time(sec) 1.6 2.0 2.2 2.5 3.0 3.5 3.5 4.5 5.5 6.6

Table

2: Experimental results for computing (
Now that we are able to add and multiply functions, we can perform all of the standard
logical operations. For example
6. Equations and inequalities
Frequently, it is useful to be able to compute the set of assignments that make f 1  f 2 , where
can be one of =; 6=; !; ; ?; or . For example, the following inequality is extremely
important for the correctness of the radix-4 SRT floating point division algorithm.
Both divisor and remainder in the inequality can be regarded as arrays of boolean variables.
In order to verify the correctness of the algorithm, it is necessary to determine the set of
assignments to these variables that make the inequality true.
Finding the set of assignments that satisfy an inequality can be reduced to the problem
of finding the set of assignments that make a function f positive. Equations can be handled
in a similar manner. A straightforward way of solving the problem is to convert f to an
MTBDD and then pick the terminal nodes with the correct sign. However, this does not
work very well in general, because some functions have MTBDDs with exponential size but
hybrid BDDs of polynomial size. For example, let f
of these functions and their difference have linear size BMDs. The BDD for the set of
assignments satisfying f linear size. But the MTBDD size for f
exponential.
We have developed an algorithm that can substantially reduce the cost for computing
relations between certain functions. In the process, we only need to know the
sign of the function values. Thus, if we find out that all of the values in a sub-HDD have the
same sign, we can conclude that all assignments in the sub-HDD will have the same value
for the relation. Consequently, we don't need to continue to expand this sub-HDD.
To obtain a good algorithm for this problem, it is necessary to determine efficiently if a
sub-HDD has uniform sign. This can be achieved by computing upper and lower bounds for
the sub-HDD. The algorithm given below determines this information. If the intermediate
results are stored, the algorithm takes time linear in the number of BDD nodes.
boundvalues(f, upper, lower)
begin
if(f is terminal node)
let -a11, a12, -a21, a22 be the inverse matrix at node f;
It is easy to prove that this algorithm gives lower and upper bounds for the function
represented by the hybrid BDD. Let l 11 stand for lower11, u 11 stand for upper 11, etc. Let
f l stand for left(f), f r stand for right(f). Suppose that the recursive calls to the children
produce correct values. Then l 1  f l  u 1 and l 2  f r  u 2 .
l 11  a 11 f l  u 11
l 12  a 12 f r  u 12
l 21  a 21 f l  u 21
l 22  a 22 f r  u 22
a 11 a 12
a 21 a 22
\Theta
f l
f r
a
a
l
Therefore, the lower and upper give correct bounds for f .
The improved algorithm for computing the BDD for the set of assignments that make the
function f positive is given below. A similar algorithm is used to find the set of assignments
that make a function zero.
bdd greaterthan0(f)
begin
if(f is terminal node)
if(f.value ?
else
boundvalues(f, upper, lower);
if(upper !=
if(lower ?
let -a11, a12, -a21, a22 be the inverse matrix at node f;
return(bddifthenelse(level(f), left, right));
This algorithm works extremely well for verification of arithmetic circuits. The following
theorem guarantees the efficiency of this algorithm for the set of linear expressions when the
Hybrid Decision Diagrams are BMDs. Most of the formulas that occur duing the verification
of the SRT division algorithm are in this class. These expressions have the form
1n
x
x
x
xx mn2
c
c

Figure

and the c i 's are integer constants. We use
the variable ordering x 1n
is a constant, the BMD for f is shown in Figure 6
Lemma 1 When f is represented as a BMD, the number of recursive calls to the greater than 0
procedure for computing the BDD for f at each level cannot exceed 4(
Proof: Suppose we consider the recursive calls to the BMD nodes that has x ij as the top
variable. The inverse transformation matrix for BMD nodes is the 2 \Theta 2 Reed-Muller matrix
. Thus, the recursive calls in the procedure greater than 0 apply to either the left
child or the sum of both children. The BMD nodes that are recursively called
variable must be the sum of the sub-BMD in Figure 6 with top variable x ij and some of the
right children of ancestors of the sub-BMD. The right children of all of the ancestor nodes
of this sub-BMD are constant nodes with the value c k 2 l where 1  k  m and l  j. The
sum of those right children can be rewritten in the form d2 j where d is an integer constant.
Therefore the BMD nodes with top variable x ij have the form shown in Figure 7.
0 otherwise and c 00
c k otherwise .
When we apply the procedure bound values to this BMD, the upper bound computed is
equal to d2
. This can be proved by induction on the structure
of the BMD. The base case is trivial. For the induction step, consider node with variable
There are two cases. The first case is when m. In this case, by induction hypothesis,
upper1 is equal to d2
Since the right branch is a constant,
x
x
xx
c
c
c

Figure

7: BMD nodes explored at level x ij
upper2 is c i 2 j . Therefore,
Similar proof can be obtained for the other case when m. In the same way, we are able to
prove that the lower bound computed by the procedure is
Hence
c 000
c 00
c 00
c 00
c 00
c 00
If d  \Gamma2
k , then upper is negative or 0 and the algorithm will return constant
false. Likewise, if d ? \Gamma2
k , lower is positive and the algorithm will return constant
true. Therefore, the recursive calls to the children can only occur when \Gamma2
\Gamma2
k . Since d is integer, there can be at most 2 \Theta (\Gamma2
recursive calls.
Theorem 2 The complexity of greater than 0 for f is O(n 2
Proof: There are n levels. Each level takes 4
recursive calls. Each recursive call
takes time O(n) to compute the upper and lower bound values. Therefore, the total time is
In the case of linear inequalities, all the new BMDs that are generated have the form of
is a constant and g is an existing BMD. If we remember the constant without
actually adding it to the BMDs, we are able to avoid generating new BMD nodes. After
introducing this technique, the complexity for compute greater than 0(f) can be further
reduced to O(n
j). For the example we had at the beginning of the section, the
relationship between the time it takes to compute the inequality and the number of bits is
shown in the Figure 8.
7. Summary and directions for future research
In this paper, we have discussed the relationship between MTBDDs and BMDs. We have
also described a generalization called hybrid decision diagrams which is often much more
concise. An efficient implementation of arithemetic operations on hybrid decision diagrams
is also given.
Computing the BDD for the set of variable assignments that satisfy an arithmetic relation
is important for reasoning about arithmetic circuits. We give an efficient algorithm for this
purpose. Moreover, we prove that for the class of linear expressions, the time complexity of
our algorithm is linear in the number of variables.
There are a number of directions for future research. Currently, we use a greedy algorithm
to choose the appropriate transformation matrix at each level in a hybrid decision
1.03.01.72.2
2.5 2.53.03.4time(sec)
No. of bits

Figure

8: time to compute \Gamma2 \Delta divisor  3 \Delta remainder  2 \Delta divisor
diagram. Although it seems unlikely that there is an efficient algorithm to find the optimal
transformation, it may be possible to develop a better heuristic that would permit an even
more concise representation.
In hybrid decision diagrams, the transformation matrices for all the nodes at one level
must be the same. If we allow these transformation matrices to differ, we should have more
freedom in selecting the transformation and, therefore, be able to reduce the representation
further.
Finally, our algorithm for solving arithmetic relations works extremely well for linear
equations and inequalities. Although the current algorithm can handle some nonlinear equations
and inequalities as well, it may be possible to extend this algorithm or to find a new
algorithm that can handle more complicated nonlinear equations and inequalities.



--R

Algebraic decision diagrams and their applications.
Introcution to matrix analysis

Verification of arithmetic functions with binary moment diagrams.
Symbolic model checking: 10 20 states and beyond.
Spectral transforms for large boolean functions with applications to technology mapping.
Efficient representation and manipulation of switching functions based on ordered kroenecker functional decision diagrams.
Fast ofdd based minimization of fixed polarity reed-muller expressions
Application of boolean algebra to switching circuit design and error de- tection
--TR
Graph-based algorithms for Boolean function manipulation
Symbolic model checking
Spectral transforms for large boolean functions with applications to technology mapping
Efficient representation and manipulation of switching functions based on ordered Kronecker functional decision diagrams
Fast OFDD based minimization of fixed polarity Reed-Muller expressions
Verification of arithmetic circuits with binary moment diagrams
Algebraic decision diagrams and their applications
Introduction to matrix analysis (2nd ed.)

--CTR
M. Thornton , R. Drechsler, Spectral decision diagrams using graph transformations, Proceedings of the conference on Design, automation and test in Europe, p.713-719, March 2001, Munich, Germany
Yirng-An Chen , Randal E. Bryant, ACV: an arithmetic circuit verifier, Proceedings of the 1996 IEEE/ACM international conference on Computer-aided design, p.361-365, November 10-14, 1996, San Jose, California, United States
James Smith , Giovanni De Micheli, Polynomial methods for component matching and verification, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.678-685, November 08-12, 1998, San Jose, California, United States
James Smith , Giovanni De Micheli, Polynomial methods for allocating complex components, Proceedings of the conference on Design, automation and test in Europe, p.45-es, January 1999, Munich, Germany
M. Clarke , M. Khaira , X. Zhao, Word level model checkingavoiding the Pentium FDIV error, Proceedings of the 33rd annual conference on Design automation, p.645-648, June 03-07, 1996, Las Vegas, Nevada, United States
methods and coverage metrics for functional verification, Proceedings of the conference on Design, automation and test in Europe: Proceedings, March 06-10, 2006, Munich, Germany
Rolf Drechsler , Bernd Becker , Stefan Ruppertz, The K*BMD: A Verification Data Structure, IEEE Design & Test, v.14 n.2, p.51-59, April 1997
Yirng-An Chen , Randal E. Bryant, PHDD: an efficient graph representation for floating point circuit verification, Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, p.2-7, November 09-13, 1997, San Jose, California, United States
James Smith , Giovanni De Micheli, Polynomial circuit models for component matching in high-level synthesis, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, v.9 n.6, p.783-800, 12/1/2001
R. Drechsler, Using Word-Level Information in Formal Hardware Verification, Automation and Remote Control, v.65 n.6, p.963-977, June 2004
Christoph Scholl , Bernd Becker , Thomas M. Weis, Word-level decision diagrams, WLCDs and division, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, p.672-677, November 08-12, 1998, San Jose, California, United States
Rolf Drechsler , Wolfgang Gnther , Stefan Hreth, Minimization of word-level decision diagrams, Integration, the VLSI Journal, v.33 n.1, p.39-70, December 2002
Louis Kruger , Somesh Jha , Eu-Jin Goh , Dan Boneh, Secure function evaluation with ordered binary decision diagrams, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA
Christoph Scholl , Bernd Becker , Thomas Weis, On WLCDs and the Complexity of Word-Level Decision DiagramsA Lower Bound for Division, Formal Methods in System Design, v.20 n.3, p.311-326, May 2002
Jin Yang , Aloysius K. Mok , Farn Wang, Symbolic model checking for event-driven real-time systems, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.2, p.386-412, March 1997
Martin Keim , Rolf Drechsler , Bernd Becker , Michael Martin , Paul Molitor, Polynomial Formal Verification of Multipliers, Formal Methods in System Design, v.22 n.1, p.39-58, January
Jawahar Jain , James Bitner , Magdy S. Abadir , Jacob A. Abraham , Donald S. Fussell, Indexed BDDs: Algorithmic Advances in Techniques to Represent and Verify Boolean Functions, IEEE Transactions on Computers, v.46 n.11, p.1230-1245, November 1997
Rolf Drechsler , Bernd Becker , Stefan Ruppertz, K*BMDs: A New Data Structure for Verification, Proceedings of the 1996 European conference on Design and Test, p.2, March 11-14, 1996
Stefan Hreth , Rolf Drechsler, Formal verification of word-level specifications, Proceedings of the conference on Design, automation and test in Europe, p.11-es, January 1999, Munich, Germany
Randal E. Bryant, Binary decision diagrams and beyond: enabling technologies for formal verification, Proceedings of the 1995 IEEE/ACM international conference on Computer-aided design, p.236-243, November 05-09, 1995, San Jose, California, United States
Pejman Lotfi-Kamran , Mohammad Hosseinabady , Hamid Shojaei , Mehran Massoumi , Zainalabedin Navabi, TED+: a data structure for microprocessor verification, Proceedings of the 2005 conference on Asia South Pacific design automation, January 18-21, 2005, Shanghai, China
S. Hreth , R. Drechsler, Dynamic minimization of word-level decision diagrams, Proceedings of the conference on Design, automation and test in Europe, p.612-617, February 23-26, 1998, Le Palais des Congrs de Paris, France
John Lafferty , Alexander Vardy, Ordered Binary Decision Diagrams and Minimal Trellises, IEEE Transactions on Computers, v.48 n.9, p.971-986, September 1999
Christoph Kern , Mark R. Greenstreet, Formal verification in hardware design: a survey, ACM Transactions on Design Automation of Electronic Systems (TODAES), v.4 n.2, p.123-193, April 1999
Edmund M. Clarke , Bernd-Holger Schlingloff, Model checking, Handbook of automated reasoning, Elsevier Science Publishers B. V., Amsterdam, The Netherlands, 2001
circuit analysis computing;hybrid decision diagrams;multi-terminal binary decision diagrams;digital arithmetic;MTBDDs;arithmetic circuits verification;integers;binary decision diagrams;symbolic model checking algorithms;computational complexity;time complexity;boolean vectors;linear expressions