Factored Edge-Valued Binary Decision Diagrams.
Factored Edge-Valued Binary Decision Diagrams form an extension to Edge-Valued Binary Decision Diagrams. By associating both an additive and a multiplicative weight with the edges, FEVBDDs can be used to represent a wider range of functions concisely. As a result, the computational complexity for certain operations can be significantly reduced compared to EVBDDs. Additionally, the introduction of multiplicative edge weights allows us to directly represent the so-called complement edges which are used in OBDDs, thus providing a one to one mapping of all OBDDs to FEVBDDs. Applications such as integer linear programming and logic verification that have been proposed for EVBDDs also benefit from the extension. We also present a complete matrix package based on FEVBDDs and apply the package to the problem of solving the Chapman-Kolmogorov equations.
Introduction
Over the past decade a drastic increase in the integration of VLSI chips has taken place. Conse-
quently, the complexity of the circuit designs has risen dramatically so that today's circuit designers
rely more and more on sophisticated computer-aided design (CAD) tools. The goal of CAD tools
is to automatically transform a description in the algorithmic or behavioral domains to one in the
physical domain, i.e. down to a layout mask for chip production. We divide this process into four
different levels: system, behavioral, logic and layout.
At the logic level, the behavior of the circuit is described by boolean functions. The efficiency
of the algorithms applied in this level depends largely on the chosen data structure. Originally,
representations such as the sum of products form or factored form representations were predominant.
Today, the most popular data structure for boolean functions is the Ordered Binary Decision
Diagram (OBDD) which provides a compact and canonical representation. In the wake of the
successful introduction of the concept of function graphs by OBDDs, various other function graphs
have been proposed which are not constrained to boolean functions but can be used to denote
arithmetic functions. These function graphs have been used for state reduction in finite state
machines and logic verification of higher-level specifications. Additionally, they have been applied
to problems outside CAD, such as integer linear programming and matrix representation.
Since the introduction of OBDDs by R. E. Bryant [5], several different forms of function
graphs have been proposed. Functional Decision Diagrams (FDD) have been presented as an
alternative to OBDDs for representing boolean functions [3]. Ordered Kronecker Functional
Decision Diagrams (OKFDD) have been introduced in [10] as a generalization of OBDDs and
FDDs. Multi-Terminal Binary Decision Diagrams (MTBDD) [9] have been proposed to represent
integer valued functions and extended to functions on finite sets [2]. Edge-Valued Binary Decision
Diagrams (EVBDD) [12][13][14] provide a more compact means of representing such functions.
Recently Binary Moment Diagrams (BMD and *BMD) [7] were introduced which permit efficient
word-level verification of arithmetic functions (including multipliers of up to 62-bit word size).
This paper presents Factored Edge-Valued Binary Decision Diagrams (FEVBDD) as an extension
to EVBDDs. By associating both an additive and a multiplicative weight with the edges,
FEVBDDs can be used to represent a wider range of functions concisely. As a result, the computational
complexity for certain operations can be significantly reduced compared to EVBDDs.
Additionally, the introduction of multiplicative edge weights allows us to directly represent the
complement edges which are used in OBDDs. This paper also describes uses of FEVBDDs in
applications such as integer linear programming, logic verification and matrix representation and
manipulation.
2 Review of Edge-Valued Binary Decision Diagrams
Edge-Valued Binary Decision Diagrams, which were proposed by Lai, et al. [12][13][14] offer
a direct extension to the concept of OBDDs. By associating a so-called edge value ev to every
then-edge of the OBDD they are capable of representing pseudo-boolean functions such as integer
valued functions. Their application has proven successful in such areas as formal verification and
integer linear programming, spectral transformation, and function decomposition.
Definition 2.1 An EVBDD is a tuple hc; fi where c is a constant value and f is a rooted, directed
acyclic graph E) consisting of two types of vertices.
ffl A nonterminal vertex f 2 V is represented by a quadruple
child t (f); child e (f); evi, where variable(f) 2 fx is a binary variable

ffl The single terminal vertex f 2 T with value 0 is denoted by 0.
There is no nonterminal vertex f such that child t child e (f) and ev = 0, and there are no
two nonterminal vertices f and g such that g. Furthermore, there exists an index function
such that the following holds for every nonterminal vertex. If child t (f)
is also nonterminal, then we must have
child e (f) is nonterminal, then we must have
Definition 2.2 An EVBDD hc; fi denotes the arithmetic function c
f is the function f denoted by evi. The terminal node 0 represents the constant
denotes the arithmetic function
Definitions (2.1), (2.2) provide a graphical representation of pseudo-boolean functions. As a
consequence integer variables have to be encoded in binary as in
is a n-bit integer variable. It has been shown that EVBDDs form a canonical representation of
functions.
Definition 2.3 Given an EVBDD hc; fi representing f(x function F that for
each variable x assigns a value F(x) equal to either 0 or 1, the function EVBDDeval is defined as
c f is the terminal node 0
child e (f)i; F)
boolean arithmetic

Table

1: Arithmetic equivalents of boolean functions
Boolean functions can be represented in EVBDDs by using the integers 0 and 1 to denote
the boolean values true and false. Boolean operations are implemented through arithmetic
operations as shown in Table 1. A method has been described by Lai, et al. that converts any
OBDD representation of a boolean function to its corresponding EVBDD representation. It can
be proven that both function graphs OBDD v and EVBDD denoting the same function f
share the same topology except that the terminal node 1 is absent from the EVBDD and the edges
connected to it are redirected to the single terminal node 0. Additionally, it was shown that boolean
operations executed on EVBDDs have the same time complexity O(jf j \Delta jgj) as boolean operations
on OBDDs. The concept of complement edges can not be realized in EVBDDs.
As has been done for OBDDs, a generic operation apply can be defined that implements
arbitrary arithmetic operations on the EVBDD representations of two arithmetic
functions f and g. In general, the time complexity of such an operation on two EVBDDs
and
the flattened EVBDDs of respectively. A flattened EVBDD is defined in exactly the
same manner as an MTBDD. For operations such as addition, subtraction, scalar-multiplication, etc.
the time complexity of apply can be drastically reduced by exploiting certain properties. A scalar
multiplication c \Delta f) can be done with time complexity O(jhc f ; f ij) by simply multiplying all
edge values by c. All operations op, such as addition, that fulfill the additive property
have the reduced time complexity O(jhc f
Based on EVBDDs, the concept of structured EVBDDs (SEVBDDs) has been developed in
[14]. SEVBDDs allow the modeling of conditional expressions and vectors. Their main use lies in
the field of formal verification.
3 Factored Edge-Valued Binary Decision Diagrams
Factored Edge-Valued Binary Decision Diagrams (FEVBDD) are an extension to EVBDDs. By
associating both an additive and a multiplicative weight with the true-edges 1 FEVBDDs offer a
more compact representation of linear functions, since common subfunctions differing only by an
affine transformation can now be expressed by a single subgraph. Additionally, they allow the
notion of complement edges to be transferred from OBDDs to FEVBDDs.
Definition 3.1 An FEVBDD is a tuple hc; w; f; rulei where c and w are constant values, f is a
rooted, directed acyclic graph E) consisting of two types of vertices, and rule is the set of
weight normalizing rules applied to the graph.
ffl A nonterminal vertex f 2 V is represented by a 6-tuple 2
child t (f); child e (f); ev; w is a binary
variable.
ffl The single terminal vertex f 2 T with value 0 is denoted by 0. By definition all branches
leading to 0 have an associated weight
There is no nonterminal vertex f such that child t
there are no two nonterminal vertices f and g such that g. Furthermore, there exists an index
function such that the following holds for every nonterminal vertex. If
child t (f) is also nonterminal, then we must have
If child e (f) is nonterminal, then we must have
Definition 3.2 A FEVBDD denotes the arithmetic function c f
is the function f denoted by i. The terminal node 0 represents the constant
denotes the arithmetic function
Definition 3.3 Given a FEVBDD representing
that for each variable x assigns a value F(x) equal to either 0 or 1, the function FEVBDDeval is
defined as:
1 The GCD rule requires also a multiplicative weight to be associated with the else-edges.
2 If we use the rational rule it holds that w nodes. Thus we can represent a nonterminal vertex by a
5-tuple hvariable(f); child t (f); child e (f); ev; w t
c f f is the terminal node 0

Figure

As an example, we construct the various function graphs based on the different decompositions
of function f given in its tabular form in Figure 1.
(2)
9 +3 (y(3 +2 z)
Equation (2) is in a form that directly corresponds to the function decomposition for MTBDDs or
ADDs and the tabular form. Equations (3) and (4) reflect the structure of the decomposition rules
for EVBDDs and FEVBDDs, respectively. The different function graphs are shown in Figure 1.

Figure

goes here.

Figure

3 goes here.

Figure

4 goes here.
Representations of signed integers based on FEVBDDs are presented in Figure 2 and representations
of word-level sum and product are given in Figures 3 and 4.
Lemma 3.1 Given two FEVBDDs which have been generated
using the same weight normalizing rule and with f and g being non-isomorphic, it holds
that there exists an assignment F 2 f0; 1g n such that c f +w f \Delta f 6= c g +w g \Delta g for this assignment.
Proof:
Case 1: if c f 6= c g then let
.
Case 2: c by the definition of non-isomorphism it holds that 9F such that
Consequently, we have
that for this assignment F.
Case 3: c we assume that it holds that f and g are non-isomorphic and that
for all assignments F. This implies that w f
g.
Consequently, f and g are isomorphic which contradicts the original assumption. Thus, it
holds that 9F such that c f g. 2
Theorem 3.1 Two FEVBDDs that have been generated
using the same weight normalizing rule, i.e. rule , denote the same function, i.e.
only if c , and f and g are isomorphic.
Proof:
Sufficiency: If c and f and g are isomorphic, then 8F,
directly from
the definitions of isomorphism and FEVBDDeval.
Necessity: If c f 6= c g then let holds that FEVBDDeval(hc f
then let F be an arbitrary assignment
such that FEVBDDeval(h0;
it holds that FEVBDDeval(hc f
and g are isomorphic
then it holds by the definition of isomorphism and FEVBDDeval that
It follows that c f +w f \Delta
val 6= c g +w g \Delta val. If f and g are non-isomorphic lemma 3.1 holds. Nowwe have to prove the lemma
for the last condition f being isomorphic to g. We need to show that if f and g are not isomorphic,
then 9F 2 f0; 1g n such that FEVBDDeval(h0;
Without loss of generality, we assume index(variable(f)) - index(variable(g)). Let
prove the lemma by induction on k.
Base: If and g are terminal nodes. Furthermore, and g are
isomorphic.
Induction hypothesis: Assume the above holds for
Induction: We show that the hypothesis holds for
i.
Case 1:
If ev f 6= ev g then let F(x n\Gammak it holds that
ev g and w t f
then let F be an arbitrary assignment such that F(x n\Gammak
holds that FEVBDDeval(h0;
\DeltaFEVBDDeval(h0;
and g t
are isomorphic it holds that FEVBDDeval(h0;
val. Thus we have that ev f +w t f
and g t
are nonisomorphic then lemma 3.1 is applicable. Almost the identical prove can
be given for ev
, and w e f
and
, or f e
and g e
are nonisomorphic.
Subcase 1: If f t
and g t
are nonisomorphic, then from
and the induction hypothesis, we see that there exists some F
such that FEVBDDeval(h0;
let F 0 be defined as F 0
Subcase 2: Otherwise f e
and g e
are nonisomorphic, then by similar arguments, letting
By definition of a reduced FEVBDD, we cannot have ev
being isomorphic to f e
. If ev f 6= 0, let F(x n\Gammak
then FEVBDDeval(h0;
g is independent of the first n \Gamma k bits. If ev
then let F be
an assignment such that F(x n\Gammak
index(variable(g)))). Furthermore, let F be such that FEVBDDeval(h0;
val f 6= 0 and FEVBDDeval(h0; If the corresponding subgraph of
f with top-variable x n\Gammak and g are isomorphic then it holds that val
val g . If the graphs
are non-isomorphic we can apply the same reasoning as we did in the proof of lemma 3.1. Oth-
erwise, f t
and f e
are non-isomorphic and at least one of them is not isomorphic to g. If f t
and
are non-isomorphic, then by induction hypothesis, there exists an assignment F such that
1 and F 0 It holds that FEVBDDeval(h0;
As shown above, FEVBDDs form a canonical representation of a function only for specific
weight normalizing rules that uniquely determine how the node weight of a new node is computed
based on its both descendants. We propose two basic rules that can be used to guarantee canonicity
for FEVBDDs. Given two FEVBDDs
rule the node weight w of hc; w; f ; rulei is computed as follows
1. GCD rule:
2. RATIONAL rule:
make new node(x i ,hc
f
/* compute the new weights */
/* guarantee uniqueness */
return

Table

2: Make New Node
These weight normalizing rules (cf. Table are applied whenever a new node is generated using
the make new node routine. (cf. Table 2). This routine enforces both the canonicity of the function
graph as well as its uniqueness.
The routine find or add preserves the uniqueness of all nodes. Before a new node is actually
created a quick hash table lookup is performed and, if the node is already a member of the table,
the stored node with its unique ID is returned. Otherwise, a new node entry in the hash table is
created and the new node with its unique ID is returned. Thus it is guaranteed that every node is
stored only once in the hash table.
Although the GCD rule requires a multiplicative weight to be associated with both the true- and
the else-edges, there are some cases where it might be the rule of choice. If the function range is
purely integer the GCD rule avoids dealing with fractions. This is particularly valuable, since all
arithmetic operations on fractions are significantly more time consuming than the built in hardware
routines for integers. Furthermore, the restriction to integers by use of the GCD rule brings a clear
advantage in memory efficiency. Even though we need to store an additional weight, the memory
consumption per node is less than when using the rational rule which requires the use of fractions.
This is because every fraction is internally represented as one integer for the numerator and one
norm weight(ev; w
f
case 'GCD':
else if(w T 6=
else
return(sign
case 'RATIONAL':
return
else if(w T 6=
return
else return ev;
break;

Table

3: Norm Weight
for the denominator. Of course, as soon as the application requires the use of fractions the rational
rule should be preferred. Nevertheless, the GCD rule is still applicable since we define:
gcd( u
3.1 Operations
As has been done for OBDDs [5] and EVBDDs [14], we provide a generic algorithm apply that
implements arbitrary arithmetic operations on two FEVBDDs (cf. Table 4). Apply takes two
FEVBDDs rule g i, as well as an operation op as its arguments.
Both FEVBDDs have to be based on the same weight normalizing rule. The algorithm recursively
branches at the top variable, i.e. the variable with the least index in f or g until it reaches a terminal
case. Terminal cases depend on the operation op; as an example, for op='+' we have the terminal
case
The computational efficiency of this algorithm can be improved significantly by taking advantage
of a computation cache. Before the recursive process is started, a quick lookup in the
computation cache is performed and if successful, then the result of op is returned immediately
without further computation. The entries of the cache are uniquely identified by a key consisting
of the operands and the operation op. Whenever a new
result is computed it is stored in the computation cache. In general the complexity of operations
performed by apply is O(khc ik).
As mentioned before we can further improve the computational complexity of apply by making
use of properties of specific operations. We adapt the concept of an additive property proposed for
EVBDDs by Lai, et al., [14] and extend it to the so-called affine property for FEVBDDs.
Definition 3.4 An operator op applied to is said to satisfy
the affine property if
The factor w is defined as can be of arbitrary value. 3
3 Similar to the rational rule we can alternatively define the affine property as follows:
All the benefits of the affine property remain the same.
/* check for a terminal case */
if(terminal
return
/* is the result of op already available in the computation cache */
if(comp table lookup(hc rule g i,op,hc ans ; w ans ; ans; rule ans i))
return (hc ans ; w ans ; ans; rule ans i);
/* perform the recursive computation of op*/
child t (g); rulei;
else f
child t (f); rulei;
child e (f); rulei;
else f
ge
/* store the result in the computation cache */
comp table insert(hc
return

Table

4: Apply
Operations that satisfy the affine property are addition, subtraction, scalar multiplication and logical
bit shifting. The main advantage of the affine property lies in reducing the computational complexity
of apply. Since we can separately compute the parts of the result generated by the constants c f and
c g and by the two subgraphs h0; w rulei, the hit ratio of the computation
cache can be drastically increased by separating the influence of the constants and always storing
only the results for This concept is applied to every recursion step so that the constant
value is never passed down to the next recursion level. Unfortunately, we still have to pass the
multiplicative weights w f and w g since they cannot be separated from the functions f and g. To
achieve a further improvement in the hit ratio, we extract the common divisor w from w f and w g and
promote only w 0
f and w 0
g . This is an advantage in such cases as reducing the problem of performing
to the already computed problem (0
quantify the influence of the GCD extraction the worst case computational complexity for operations
satisfying the affine property is given as O(jhc f
the EVBDDs corresponding to the FEVBDDs respectively.
Scalar multiplication and logical-bit shifting offer a better computational complexity since they
can be computed in time independent of the size of the function graph. Scalar multiplication only
requires the weights of the root node to be multiplied. In the case of EVBDDs we have to multiply
every edge weight with the scalar; a task of complexity O(jf j).
Since multiplication does not satisfy the affine property we are basically required to use the
original version of apply. For the multiplication of two functions that both have a high percentage
of reconverging branches, the following approach tends to improve the cache efficiency:
We now have only O(jhc calls to multiply but every call requires
three calls to apply for adding the separate terms. The first addition is not costly since the first term
is always a constant, however, the second and third addition are potentially costly.
In addition to the additive property, two further properties - the bounding property and the
domain-reducing property - have been introduced by Lai, et al. [14] [12]. As has been done for
the additive property, these properties can be easily adapted to FEVBDDs.
3.2 Representation of Boolean Functions
Boolean Functions are represented in FEVBDDs by encoding the boolean values true and false
as integers 1 and 0, respectively. All the basic boolean operations can be easily represented using
only arithmetic operations. Thus we can easily represent any boolean function using FEVBDDs.
Although we could implement the boolean operations based on their corresponding arithmetic
functions, it is by far better in terms of computational complexity to directly use apply for boolean
operations. All we need to do is to provide the necessary terminal cases for apply(hc
boolean op). In the case of the boolean conjunction operation for example the
terminal cases are:
1.
2.
3. if(hc
To convert a boolean function from its OBDD to its FEVBDD representation we can adapt the
algorithm suggested by Lai in [14]. Additionally, the concept of multiplicative weights allows us
to directly represent the so called complement edges, so that we need to take care of this case in
the algorithm:
1. convert the terminal node 0 to h0; 0; 0; rulei and 1 to h1; 0; 0; rulei.
2. for each nonterminal node hx i ; t; ei in the OBDD such that t and e have already been converted
to FEVBDDs as the following conversion rules
are applied:
3. if the branch leading fromnode hx i ; t; ei to t or e is a complement edge we have to perform the
complementation by computing e, respectively. This is achieved by multiplying
both weights c t (c e ) and w t (w e ) by \Gamma1 and later adding 1 to c t (c e ). The four basic conversion
rules are listed below:
The above conversion rules are not complete in the case of FEVBDDs since we can now
also have variations in the multiplicative weights which can either be +1 or \Gamma1. These cases
however are handled exactly according to the norm weighting rule that has been presented
before, so that we do not explicitly list them here.
As it has been done for EVBDDs [14], it can be shown that the following theorems hold.
Theorem 3.2 Given an OBDD representation v of a boolean function with complement edges
being allowed and an FEVBDD have the same topology except that
the terminal node 1 is absent from the FEVBDD v 0 and the edges connected to it are redirected to
the terminal node 0.
Theorem 3.3 Given two OBDDs f and g with complement edges being allowed and the corresponding
FEVBDDs time complexity of boolean
operations on FEVBDDs (using apply) is O(jfj \Delta
An example of a FEVBDD representing a boolean function with complement edges is given
in

Figure

5. This FEVBDD represents the four output functions of a 3-bit adder. It has the same
topology (except for the terminal edges) as the corresponding OBDD depicted in the same figure.
As it is shown in this example, FEVBDDs successfully extend the use of EVBDDs to represent
boolean functions as they inherently offer a way to represent complement edges. Furthermore, the
boolean operation 'not' can now be performed in constant time since it only requires manipulation
of the weights of the root node.

Figure

5 goes here.
3.3 Logic Verification
The purpose of logic verification is to formally prove that the actual implementation satisfies the
conditions defined by the specification. This is done by formally showing the equivalence between
the combinational circuit, i.e. the description of the design and the specification of the intended
behaviour.
In general, the implementation is represented by an array of boolean functions f b and the
specification is given by a word-level function fw . In order to transform the bit-level representation
to the word-level we can use any encoding function to encode the binary input signals to the circuit.
The set of input signals is partitioned into several subsets of binary signals x every
array x i is then encoded using an encoding function encode i that provides a word-level interpretation
of the binary input signals. Common encoding functions are signed-integer, one's-complement and
two's-complement. The corresponding FEVBDDs are shown in Figure 2. Thus, the implementation
can be described by an array of boolean functions f b The specification is given as a
word-level function fw (X Verification is then done by proving the equivalence between
an encoding of the binary output signals of the circuit, i.e. the array of boolean functions, and the
word-level function of the encoded input signals:
encode out (f b
This strategy for logic verification was first proposed by Lai, et al., using EVBDDs [12][14]. Since
FEVBDDs can describe both bit-level and word-level functions, they can be successfully applied
to logic verification.
Although all word-level operations can be represented by FEVBDDs, the space complexity of
certain operations becomes exponential so that their application is limited to small word-length.
Both EVBDD and FEVBDD representations of word-level multiplication are exponential;
FEVBDDs however offer significant savings in memory consumption over EVBDDs. As can
be seen in Figure 4 for word-level multiplication of two three-bit integers, the EVBDD contains
28 internal nodes whereas the FEVBDD representation requires only 10 nodes. In general, the
EVBDD denoting the multiplication of two n-bit integers has (n nodes. The
corresponding FEVBDD contains only n+ nodes and the ratio of EVBDD nodes
to FEVBDD nodes is n+1
. As can be seen from this ratio, the savings in the number of nodes in
the FEVBDD representation are of order n. As an example, a 16-bit multiplier requires 1,114,095
EVBDD nodes but only 65,551 FEVBDD nodes. Even if we take into account that a FEVBDD
node requires 20 bytes versus only 12 bytes per EVBDD node, the savings remain significant
(EVBDD:13.3 Mbyte, FEVBDD: 1.3 Mbyte).
As has been done for EVBDDs [14], FEVBDDs can also be extended to structured FEVBDDs
which allow the modeling of conditional expressions and vectors.
3.4 Integer Linear Programming
An algorithm FGILP for solving Integer Linear Programming (ILP) problems based on EVBDDs
has been proposed by Lai, et al. in [15]. FGILP realizes an ILP solver based on function graphs,
which uses a mixed branch-and-bound/implicit-enumeration strategy. It has been shown that this
approach can successfully compete with other branch-and-bound strategies that require the solution
of the corresponding Linear Programming problems. The latter strategy is the one most widely
applied in commercial programs.
An ILP problem can be formulated as follows:
minimize
subject to
with x i integer
Since both EVBDDs and FEVBDDs allow only binary decision variables, the encodings shown
in

Figure

2 have to be applied. A 32-bit integer, for example, can be represented by an EVBDD
or FEVBDD with nodes. Since FEVBDDs form an extension of EVBDDs we can also apply
FEVBDDs to solve ILP problems. We expect a reduction in the memory requirement for FGILP
when using FEVBDDs. This is due to the fact that different multiples of the integer variables x i
appear in equations (5) and (6). If we use EVBDDs to represent these multiples of x i , we have
to build an EVBDD for every different coefficient a ij since scalar multiplication on EVBDDs is
performed by multiplying all edge weights with the factor. If we use FEVBDDs, however, we
only have to store the FEVBDD representing x i once. Multiples of x i can be easily realized by
associating the corresponding multiplicative edge weights with dangling incoming edges leading
to x i . As an example, storing 6x, 7x and 5x requires 96 nodes if we use EVBDDs but only
nodes if we apply FEVBDDs.
3.5 Implementation of Arbitrary Precision Arithmetic
The introduction of multiplicative weights in combination with the RATIONAL rule for weight
normalizing makes it necessary to extend the value range of the edge weights from the integer
domain to the rational domain. This is done in a way such that any future expansion to other
domains such as the complex domain can be easily achieved. All operations on edge weights are
accessed through a standardized interface that invokes the specified function and then executes
the requested operation depending on the current mode. Thus, the FEVBDD code remains fully
independent of the selected domain. By changing to another mode we can easily switch from the
integer domain to the rational domain, for example. This means we can still use the fast routines
for single precision integers when necessary.
Multiple precision integers are realized as arrays of integers and the arithmetic operations are
implemented based on the algorithms for multiple precision arithmetic given by Knuth in [11].
Multiple precision fractions are implemented as arrays of two multiple precision integers where
one integer represents the numerator and the other one the denominator. It is enforced by the
package that the numerator and denominator remain relative prime and only the numerator can
be signed. This is achieved by computing the greatest common divisor (GCD) of numerator and
denominator and dividing both the numerator and denominator by the GCD. This operation is
performed whenever an input is given. Internally the data is guaranteed to remain in the normalized
form as this form is strictly enforced by all operations. Thus, a rational value is always uniquely
represented by the numerator and denominator.
The GCD can be computed very fast by Euclid's algorithm or the binary GCD algorithm
[11]. For multi-precision fractions we use the binary GCD algorithm since it works very fast for
integers of multiple word length. It only relies on subtraction and right shifting and does not
require division operations. For single word precision fractions we employ the classical version
of Euclid's algorithm since division can be executed very efficiently for single word integers. The
basic arithmetic operations for fractions are realized as follows:
ffl multiplication:
ffl division:
U
ffl addition:
3.5.1 Symbolic Operations and Finite Fields
FEVBDDs are not constrained to integer valued functions. As one can already see in the use of a
rational rule, we can easily represent functions with rational function values. Complex values are
also feasible; additionally, we can use symbolic computation. Even though the value ranges can be
extended by using rational or complex edge weights, the decision variables still have to be binary.
Thus, if we want to represent linear functions containing variables from the above value ranges,
we have to encode them binarily such as it has been done for integers. Generally this approach
leads to a means to represent any function on finite fields by FEVBDDs as it has been proposed for
ADDs [2]. In this case the FEVBDD generally represents the function
where \Phi and fi denote operations on the finite field. The ITE operator acts as a switch that either
selects the subfunction denoted by the true- or else-edge. Contrary to the ADD approach we can
exploit relationships between the subgraphs.
4 Matrix Representation and Manipulation
Matrices have been successfully represented using MTBDDs [8] [9] and ADDs [2] and implementations
of the basic matrix operations such as addition and multiplication have been given. A
popular class of matrices that can be efficiently represented by MTBDDs and EVBDDs is the class
of Walsh matrices which can be generated by a recursive rule.
4.1 Representation of Matrices
The basic idea in using function graphs to represent matrices is to encode both the row and
column position of the matrix elements using binary variables. An 8 \Theta 8 matrix, for example,
requires 3 binary variables for the rows and another 3 for the columns. Basically, we can view
the problem of representing a m \Theta n matrix as representing a function from the finite set
of all element positions to the finite set R of its elements.
The binary variables giving the row position are called row designators x 2 fx g, the
ones denoting the column position are called column designators y 2 fy g. For the
imposed variable ordering row and column designators are mixed together such that the order is
g. Because of this chosen variable ordering subtrees in the function graph
directly correspond to submatrices in the given matrix, as can be seen in Figure 6. Based on this
correspondence the pseudo-boolean function denoting the matrix M can be given easily:
fM xy

Figure

6 goes here.
Furthermore, this ordering allows matrices to be be represented compactly if they have submatrices
that are identical (MTBDDs) or can be transformed into each other by an affine transformation 4
(FEVBDDs). Since the concept of square matrices, i.e. vertical size
to keep many algorithms efficient and simple we will from now on only consider square matrices
with max(m;n). To make non-square matrices square we can easily pad them with rows
or columns filled with zeros. This does not significantly increase our memory consumption for
storing the matrix since the padded blocks are uniform and can therefore be represented by only a
few nodes.
As it has already been mentioned, MTBDDs only offer a compact and memory efficient
representation of matrices that feature identical subblocks. They require a different terminal node
for each distinct matrix element. FEVBDDs can do far better than that. The concept of FEVBDDs
allows two subblocks to be represented by the same subgraph if they differ only by an affine
transformation of their elements. We will now introduce a special class of matrices that can always
be represented by a FEVBDD of linear size. For this class of matrices the sizes of the corresponding
MTBDD, EVBDD and *BMD are likely to be exponential.
Definition 4.1 A recursively-affine matrix is recursively generated using the following rules:
1. we begin with a 1 \Theta 1 matrix M is a integer or rational constant value
2. in every recursion step a new matrix M n+1 is created based on the previous result M n such
with being arbitrary integer or rational numbers.
4 An affine transformation is a transformation of the form y ! a

Figure

7 shows the general structure of the FEVBDD that corresponds to a recursion step in building
up a recursively affine matrix. In every recursion step a structure as shown in Figure 7 is added to
the already constructed FEVBDD.

Figure

7 goes here.
As can be seen from Figure 7 we only need 3 nodes to represent a recursively-affine
matrix of size n x n. As an example of a recursively affine matrix we build in Figure 8 the FEVBDD
for the matrix M given below:
9 5
26 22 64

Figure

8 goes here.
An important class of matrices that belongs to the family of recursively-affine matrices is the set
of Walsh matrices in the Hadamard ordering [17]. These matrices can be used to compute spectral
transforms of boolean functions. They are recursively defined as follows:

Figure

9 shows both the FEVBDD and EVBDD representations of the Walsh matrix H h
3 . As can
be seen in Figure 9, the size of the FEVBDD representation is 2 \Delta n where n denotes the order of
the Walsh matrix. The size of the EVBDD representation is 4

Figure

9 goes here.
Generally speaking, employing function graphs such as MTBDDs or FEVBDDs to represent
sparse matrices offers the following advantages:
1. In comparison with normal sparse data structures, function graphs do provide a uniform
log 2 (N) access time, where N is the number of real elements being stored in the function
graph (for example, all non-zero elements of a sparse matrix)
2. Function graphs may not be able to beat sparse-matrix data structures in terms of worst space
complexity. However, recombination of isomorphic subgraphs may give a considerable
practical advantage to function graphs over other data structures. This is particularly valid
for FEVBDDs since the same subgraph can represent all the matrices that can be generated
by an affine transformation of the matrix represented by the subgraph.
4.2 Operations
Operations on matrices can be divided into two major groups. The first group comprises termwise
operations such as scalar multiplication, addition, etc. The second group is formed by matrix
multiplication, matrix transpose and matrix inversion. Termwise operations are easily implemented
based on function graphs. We can simply use apply to compute all termwise operations on matrices.
This is obviously possible since apply(op) performs the operation op on every single function value,
i.e. it works in a termwise manner. Matrix specific operations such as transposition require their
own tailored algorithms.
Matrix multiplication is clearly a non-termwise operation since it requires computing the scalar
vector product of a row of the left matrix with a column of the right matrix to get the value of a
single matrix element of the product matrix. Therefore, we will present two different recursive
procedures to perform matrix multiplication on function graphs. The first method was proposed
by McGeer [9]. This algorithm has the most direct link to the common conventional method for
matrix multiplication. In every recursion step the problem is divided into four subproblems until
a terminal case has been reached. In these steps operands are expanded with regard to a pair of
row and column designators. This expansion even takes place if the function graphs are actually
not dependent on the current pair of internal variables. By doing so there is no need for a scaling
step as is necessary in the second method. Let matrix multiplication be denoted by ? and matrix
addition by +. This method can be formally stated as:
or written in terms of matrices:4 h xy h xy
f xz f xz5 ?4 g zy g zy
zy g zy5
The computations performed in every recursion step are:
Obviously, this method requires eight calls to matrix multiply and four calls to matrix add in every
recursion step, i.e. for every internal variable pair.
The second method was proposed by Bahar [2]. Unlike the previous method it only expands
the top variable of the two operands ffx g. In
the process of matrix multiplication, the following variable order
is imposed to decide whether the top variable of f or g has to be selected as the top variable
for expansion. Depending on the character of the expansion variable var one of the following
computations is being made in every recursion step.
This approach only expands internal variables that are actually encountered in the function graphs
f and g. It requires to keep track of missing z variables in f and g since every z expansion step
corresponds to performing matrix addition. If p gives the number of omitted z expansions between
two recursion steps we have to scale the result by 2 p before returning it. When using a cache we
always store the unscaled results and scale the entry accordingly when reading the cache.
Another method was proposed by Clarke [9]. Its basic idea is to take all the products first and
then compute all the sums.
For our matrix package we have implemented the second method which appears to be superior
to the other two [2]. We implemented two different versions of this method. Version 1 passes the
value of the edge weights down with every recursion step of matrix multiply and is of O(kfk \Delta kgk)
complexity. As we have done for multiplication of two FEVBDDs we suggest a second version for
function graphs with a high ratio of reconverging branches (e.g. for recursively-affine matrices) as
follows.
[f
The operations rowadd and coladd which generate matrices such that
a
i a 0i
a
i a in
only have complexity O(jf j). This second version requires only O(jf j \Delta jgj) calls to matrix multiply
but every recursive call to matrix multiply also requires three calls to matrix add. It improves
the cache efficiency of matrix multiplication considerably, if both operands are represented by
FEVBDDs with a high ratio of reconverging branches. This outweighs the added overhead of three
calls to matrix add. If this is not the case, it is better to use the original approach since it does not
require the additional overhead.
Matrix transposition is performed by exchanging the roles of column and row designators
belonging to the same expansion level. To maintain the imposed variable ordering the nodes in
the function graph have to be exchanged and it is not sufficient to just interpret row as column
designators and vice versa. Transposition can be done in O(jf
Matrix inversion is done by performing Gaussian elimination on the original matrix and the
identity matrix at the same time. In other words we solve the system of linear equations A ?
with the use of pivoting and row transformations. The steps required by Gaussian elimination
consist of [19]:
ffl selecting a partial pivot in every step j such that ja pj
ffl normalizing the selected row by multiplying the row by the inverse of the pivot 1
ffl swapping rows j and p according to above pivot selection
subtracting multiples of the pivot row j from all rows i ? j such that a
All of the above operations except for row swapping can be implemented efficiently in time O(jAj)
or O(jAj \Delta jRj) where R denotes the FEVBDD representing the pivot row. Row swapping is
performed by matrix multiplication of matrix A with a permutation matrix P and therefore is of
complexity Permutation matrices can be obtained by
denotes a permutation matrix swapping rows i and j, I represents the identity matrix and M ij
designates a matrix
rs
rs
In general, partial pivoting is done in order to improve the numerical accuracy of Gaussian elimi-
nation. Since our implementation relies on fractions of arbitrary precision we always use the exact
values and numerical stability is not an issue. In order to avoid unnecessary row swapping we only
perform the partial pivoting if it holds in step j that a
In addition to the basic matrix operations, fast search operations for specific matrix elements
have been implemented. Algorithms for searching both the value and position of the minimal,
maximal or absolute maximal element in a given matrix were developed. This approach makes use
of the min and max fields that can be associated with every node. The computational complexity
for finding both the value and position of the minimal or maximal element in a n \Theta n matrix is
O(log 2 (dne)). We will now explain the basic idea behind the algorithms in the case of searching
for the maximal element. Given a FEVBDD node f and its two successors f t
and f e
we can easily
determine which edge leads to the maximal element. Based on the values of the max and min
fields of f t
and f e
we simply recompute the max field of f and select the successor that originally
generated the max field of f. If only the value of the maximal or minimal element is of interest,
it can be computed directly from the min and max field of the top node f without any further
computation.
value EVBDD FEVBDD
range GCD RATIONAL
integer 12 bytes 20 bytes 24 bytes
fractions

Table

5: Memory requirement per node
4.3 Experimental Results
We have applied our FEVBDD based matrix package to the problem of solving the Chapman-Kolmogorov
equations [18] that arise when computing the global state probabilities of FSMs.
Though the memory consumption of our inversion routine is relatively low (8M for inverting a
64x64 matrix), the run time is very high. This is due to several factors. First, the algorithm for Gaussian
elimination is purely sequential whereas FEVBDDs are recursively defined. Consequently,
computation caching for matrix inversion does not exist. A recursive algorithm for matrix inversion
will perform much better on FEVBDDs. Secondly, when using fractions of arbitrary length all
operations need substantially more time than is necessary for ordinary integers. We
therefore use the obtained inverses primarily as examples of real life non-sparse matrices that can
be represented compactly using FEVBDDs and compare them with their EVBDD representations.
As can be seen from the table below using FEVBDDs gives savings of up to 50% compared to
EVBDDs in the number of nodes required to represent the non-sparse inverse. Of course, one has
to consider that the storage requirement per node is higher for FEVBDDs than for EVBDDs. An
overview of the memory usage per node in the various modes available for EVBDDs and FEVB-
DDs is given in table 5. We assume that every EVBDD node consists of an integer or fractional
edge value and two pointers to the children. Every FEVBDD node consists of two fractional edge
weights and two pointers in the RATIONAL mode or three integer edge weights and two pointers
in the GCD mode.
The total memory consumption for storing the matrices using EVBDDs and FEVBDDs is shown
in tables 6 and 7, respectively. The given memory usage is based on EVBDDs and FEVBDDs using
fractions. The FEVBDDs have been generated using the RATIONAL rule. In the case of CK-
Equations we have to use fractions for the edge weights since the matrix elements are fractions. As
can be seen from the tables, FEVBDDs do better for the inverses but lose for the original matrices
in terms of total memory consumption. This is due to the fact that the original matrices are sparse
whereas the inverses are non-sparse. In the case of sparse matrices the additional properties of
FEVBDDs are not exploited so that EVBDDs and FEVBDDs perform similarly in the number of
nodes. FEVBDDs, however, lose in terms of memory requirement because of the higher cost per
FEVBDD node. Since EVBDDs do at least as good as MTBDDs this also gives an idea of the
performance of FEVBDDs compared to MTBDDs.
5 Conclusion
We showed that by associating both an additive and a multiplicative weight with the edges of
an Edge-Valued Binary Decision Diagram, EVBDDs could successfully be extended to Factored
Edge-Valued Binary Decision Diagrams. The new data structure preserves the canonical property
of the EVBDD and allows efficient caching of operational results. All properties that have been
defined for EVBDDs could be adapted to FEVBDDs. The additive property was extended to the
affine property. It was shown that FEVBDDs provide a more compact representation of arithmetic
functions than EVBDDs. Additionally, the complexity of certain operations could be reduced
significantly. We showed that FEVBDDs representing boolean functions allow us to incorporate
the concept of complement edges that has originally been proposed for OBDDs. Furthermore,
we showed that the EVBDD based Integer Linear Programming solver FGILP benefits from using
FEVBDDs instead of EVBDDs.
In combination with the FEVBDD package we also implemented an arithmetic package which
supplies arithmetic operations on both integers and fractions of arbitrary precision. A complete
matrix package based on FEVBDDs was introduced. We applied the package to solving the
Chapman-Kolmogorov equations. The experimental results show that in the majority of cases
FEVBDDs win over the corresponding EVBDD representation of the matrices in terms of number
of nodes and memory consumption.

Acknowledgement

The authors like to thank Y.-T. Lai for supplying them with the EVBDD package and many helpful
discussions.



--R

"Binary decision diagrams,"
"Al- gebraic Decision Diagrams and their Applications"
"On the relation between BDDs and FDDs"
"Efficient Implementation of a BDD Package,"
"Graph-Based Algorithms for Boolean Function Manipulation,"
"Symbolic Boolean Manipulation with Ordered Binary-Decision Diagrams,"
"Verification of Arithmetic Functions with Binary Moment Diagrams,"
"Spectral transforms for large Boolean functions with application to technology mapping"
"Multi-terminal binary decision diagrams: an efficient data structure for matrix representation,"
"Efficient Representation and Manipulation of Switching Functions Based on Ordered Kronecker Functional Decisiond Diagrams"
"The Art of Computer Programming Volume 2: Seminumerical Algorithms"
"Edge-valued binary decision diagrams for multi-level hierarchical verification"
Vrudhula, "EVBDD-based algorithms for integer linear programming, spectral transformation and function decomposition"
"Edge-valued binary decision diagrams"
Vrudhula, "FGILP: An integer linear program solver based on function graphs"
"Representation of switching circuits by binary-decision-programs"
"Fast Transforms. Algorithms, Analyses, Applications"
"A First Course in Probability"
"Introduction to Numerical Analysis"
"Factored Edge-Valued Binary Decision Diagrams and their Application to Matrix Representation and Manipulation"
--TR
Graph-based algorithms for Boolean function manipulation
Efficient implementation of a BDD package
Symbolic Boolean manipulation with ordered binary-decision diagrams
Edge-valued binary decision diagrams for multi-level hierarchical verification
Spectral transforms for large boolean functions with applications to technology mapping
Algebraic decision diagrams and their applications
The art of computer programming, volume 2 (3rd ed.)
Fast Transforms
Formal Verification Using Edge-Valued Binary Decision Diagrams
Verification of Arithmetic Functions with Binary Moment Diagrams

--CTR
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
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
logic verification;Ordered Binary Decision Diagrams;integer linear programming;pseudo-boolean functions;matrix operations;affine property