Boolean satisfiability with transitivity constraints.
We consider a variant of the Boolean satisfiability problem where a subset &epsiv; of the propositional variables appearing in formula Fsat encode a symmetric, transitive, binary relation over N elements. Each of these relational variables, ei,j, for 1  i < j  N, expresses whether or not the relation holds between elements j. The task is to either find a satisfying assignment to Fsat that also satisfies all transitivity constraints over the relational variables (e.g., e1,2 &wedge; e2,3  e1,3), or to prove that no such assignment exists. Solving this satisfiability problem is the final and most difficult step in our decision procedure for a logic of equality with uninterpreted functions. This procedure forms the core of our tool for verifying pipelined microprocessors.To use a conventional Boolean satisfiability checker, we augment the set of clauses expressing Fsat with clauses expressing the transitivity constraints. We consider methods to reduce the number of such clauses based on the sparse structure of the relational variables.To use Ordered Binary Decision Diagrams (OBDDs), we show that for some sets &epsiv;, the OBDD representation of the transitivity constraints has exponential size for all possible variable orderings. By considering only those relational variables that occur in the OBDD representation of Fsat, our experiments show that we can readily construct an OBDD representation of the relevant transitivity constraints and thus solve the constrained satisfiability problem.
Introduction
Consider the following variant of the Boolean satisfiability problem. We are given a Boolean
formula F sat over a set of variables V . A subset symbolically encodes a binary relation
over N elements that is reflexive, symmetric, and transitive. Each of these relational variables,
whether or not the relation holds between elements
j. Typically, E will be "sparse," containing much fewer than the N(N \Gamma 1)=2 possible variables.
Note that when e i;j 62 E for some value of i and of j, this does not imply that the relation does
not hold between elements i and j. It simply indicates that F sat does not directly depend on the
relation between elements i and j.
A transitivity constraint is a formula of the form
denote the set of
all transitivity constraints that can be formed from the relational variables. Our task is to find
an assignment -: V ! f0; 1g that satisfies F sat , as well as every constraint in Trans(E). Goel,
et al. [GSZAS98] have shown this problem is NP-hard, even when F sat is given as an Ordered
Binary Decision Diagram (OBDD) [Bry86]. Normally, Boolean satisfiability is trivial given an
OBDD representation of a formula.
We are motivated to solve this problem as part of a tool for verifying pipelined microprocessors
[VB99]. Our tool abstracts the operation of the datapath as a set of uninterpreted functions and
uninterpreted predicates operating on symbolic data. We prove that a pipelined processor has
behavior matching that of an unpipelined reference model using the symbolic flushing technique
developed by Burch and Dill [BD94]. The major computational task is to decide the validity
of a formula Fver in a logic of equality with uninterpreted functions [BGV99a, BGV99b]. Our
decision procedure transforms Fver first by replacing all function application terms with terms
over a set of domain variables fv i j1 - i - Ng. Similarly, all predicate applications are replaced
by formulas over a set of newly-generated propositional variables. The result is a formula F
ver
containing equations of the form v . Each of these equations is
then encoded by introducing a relational variable e i;j , similar to the method proposed by Goel, et
al. [GSZAS98]. The result of the translation is a propositional formula encf
ver ) expressing the
verification condition over both the relational variables and the propositional variables appearing
in F
ver . Let F sat denote :encf
ver ), the complement of the formula expressing the translated
verification condition. To capture the transitivity of equality, e.g., that v i
we have transitivity constraints of the form e [i;j] - e [j;k] ) e [i;k] . Finding a satisfying assignment
to F sat that also satisfies the transitivity constraints will give us a counterexample to the original
verification condition Fver . On the other hand, if we can prove that there are no such assignments,
then we have proved that Fver is universally valid.
We consider three methods to generate a Boolean formula F trans that encodes the transitivity
constraints. The direct method enumerates the set of chord-free cycles in the undirected graph
having an edge (i; for each relational variable e This method avoids introducing additional
relational variables but can lead to a formula of exponential size. The dense method uses
relational variables e i;j for all possible values of i and j such that 1 - . We can then
axiomatize transitivity by forming constraints of the form e [i;j] -e [j;k] ) e [i;k] for all distinct values
of i, j, and k. This will yield a formula that is cubic in N . The sparse method augments E with
additional relational variables to form a set of variables , such that the resulting graph is chordal
[Rose70]. We then only require transitivity constraints of the form e [i;j] - e [j;k] ) e [i;k] such that
. The sparse method is guaranteed to generate a smaller formula than the
dense method.
To use a conventional Boolean Satisfiability (SAT) procedure to solve our constrained satisfiability
problem, we run the checker over a set of clauses encoding both F sat and F trans . The latest
version of the FGRASP SAT checker [M99] was able to complete all of our benchmarks, although
the run times increase significantly when transitivity constraints are enforced.
When using Ordered Binary Decision Diagrams to evaluate satisfiability, we could generate
OBDD representations of F sat and F trans and use the APPLY algorithm to compute an OBDD
representation of their conjunction. From this OBDD, finding satisfying solutions would be trivial.
We show that this approach will not be feasible in general, because the OBDD representation of
F trans can be intractable. That is, for some sets of relational variables, the OBDD representation
of the transitivity constraint formula F trans will be of exponential size regardless of the variable
ordering. The NP-completeness result of Goel, et al. shows that the OBDD representation of
F trans may be of exponential size using the ordering previously selected for representing F sat
as an OBDD. This leaves open the possibility that there could be some other variable ordering
that would yield efficient OBDD representations of both F sat and F trans . Our result shows that
transitivity constraints can be intrinsically intractable to represent with OBDDs, independent of
the structure of F sat .
We present experimental results on the complexity of constructing OBDDs for the transitivity
constraints that arise in actual microprocessor verification. Our results show that the OBDDs can
indeed be quite large. We consider two techniques to avoid constructing the OBDD representation
of all transitivity constraints. The first of these, proposed by Goel, et al. [GSZAS98], generates
implicants (cubes) of F sat and rejects those that violate the transitivity constraints. Although this
method suffices for small benchmarks, we find that the number of implicants generated for our
larger benchmarks grows unacceptably large. The second method determines which relational
variables actually occur in the OBDD representation of F sat . We can then apply one of our three
techniques for encoding the transitivity constraints in order to generate a Boolean formula for the
transitivity constraints over this reduced set of relational variables. The OBDD representation of
this formula is generally tractable, even for the larger benchmarks.
Benchmarks
Our benchmarks [VB99] are based on applying our verifier to a set of high-level microprocessor
designs. Each is based on the DLX RISC processor described by Hennessy and Patterson [HP96]:
1\ThetaDLX-C: is a single-issue, five-stage pipeline capable of fetching up to one new instruction
every clock cycle. It implements six instruction types: register-register, register-immediate,
Circuit Domain Propositional Equations
Variables Variables
Buggy min. 22 56 89
2\ThetaDLX-CC avg. 25 69 124
max.

Table

1: Microprocessor Verification Benchmarks. Benchmarks with suffix "t" were modified
to require enforcing transitivity.
load, store, branch, and jump. The pipeline stages are: Fetch, Decode, Execute, Memory,
and Write-Back. An interlock causes the instruction following a load to stall one cycle if
it requires the loaded result. Branches and jumps are predicted as not-taken, with up to 3
instructions squashed when there is a misprediction. This example is comparable to the DLX
example first verified by Burch and Dill [BD94].
2\ThetaDLX-CA: has a complete first pipeline, capable of executing the six instruction types, and
a second pipeline capable of executing arithmetic instructions. Between 0 and 2 new
instructions are issued on each cycle, depending on their types and source registers, as well as
the types and destination registers of the preceding instructions. This example is comparable
to one verified by Burch [Bur96].
2\ThetaDLX-CC: has two complete pipelines, i.e., each can execute any of the six instruction types.
There are four load interlocks-between a load in Execute in either pipeline and an instruction
in Decode in either pipeline. On each cycle, between 0 and 2 instructions can be issued.
In all of these examples, the domain variables v i , with 1 - i - N , in F
ver encode register
identifiers. As described in [BGV99a, BGV99b], we can encode the symbolic terms representing
program data and addresses as distinct values, avoiding the need to have equations among these
variables. Equations arise in modeling the read and write operations of the register file, the bypass
logic implementing data forwarding, the load interlocks, and the pipeline issue logic.
Our original processor benchmarks can be verified without enforcing any transitivity con-
straints. The unconstrained formula F sat is unsatisfiable in every case. We are nonetheless motivated
to study the problem of constrained satisfiability for two reasons. First, other processor
designs might rely on transitivity, e.g., due to more sophisticated issue logic. Second, to aid designers
in debugging their pipelines, it is essential that we generate counterexamples that satisfy
all transitivity constraints. Otherwise the designer will be unable to determine whether the counterexample
represents a true bug or a weakness of our verifier.
To create more challenging benchmarks, we generated variants of the circuits that require enforcing
transitivity in the verification. For example, the normal forwarding logic in the Execute
stage of 1\ThetaDLX-C must determine whether to forward the result from the Memory stage instruction
as either one or both operand(s) for the Execute stage instruction. It does this by comparing the
two source registers ESrc1 and ESrc2 of the instruction in the Execute stage to the destination
register MDest of the instruction in the memory stage. In the modified circuit, we changed the by-pass
condition ESrc1=MDest to be ESrc1=MDest- (ESrc1=ESrc2-ESrc2=MDest).
Given transitivity, these two expressions are equivalent. For each pipeline, we introduced four
such modifications to the forwarding logic, with different combinations of source and destination
registers. These modified circuits are named 1\ThetaDLX-C-t, 2\ThetaDLX-CA-t, and 2\ThetaDLX-CC-t.
To study the problem of counterexample generation for buggy circuits, we generated 105 variants
of 2\ThetaDLX-CC, each containing a small modification to the control logic. Of these, 5 were
found to be functionally correct, e.g., because the modification caused the processor to stall un-
necessarily, yielding a total of 100 benchmark circuits for counterexample generation.

Table

1 gives some statistics for the benchmarks. The number of domain variables N ranges
between 13 and 25, while the number of equations ranges between 27 and 143. The verification
condition formulas F
ver also contain between 42 and 77 propositional variables expressing the
operation of the control logic. These variables plus the relational variables comprise the set of
variables V in the propositional formula F sat . The circuits with modifications that require enforcing
transitivity yield formulas containing up to 19 additional equations. The final three lines
summarize the complexity of the 100 buggy variants of 2\ThetaDLX-CC. We apply a number of simplifications
during the generation of formula F sat , and hence small changes in the circuit can yield
significant variations in the formula complexity.
3 Graph Formulation
Our definition of Trans(E) (Equation 1) places no restrictions on the length or form of the transitivity
constraints, and hence there can be an infinite number. We show that we can construct a
graph representation of the relational variables and identify a reduced set of transitivity constraints
that, when satisfied, guarantees that all possible transitivity constraints are satisfied. By introducing
more relational variables, we can alter this graph structure, further reducing the number of
transitivity constraints that must be considered.
For variable set E , define the undirected graph G(E) as containing a vertex i for
an edge (i; for each variable e . For an assignment - of Boolean values to the relational
variables, define the labeled graph G(E; -) to be the graph G(E) with each edge (i; labeled as a
1-edge when -(e i;j and as a 0-edge when -(e i;j
A path is a sequence of vertices having edges between successive elements.
That is, each element i p of the sequence (1 - p - while each
successive pair of elements forms an edge (i We consider each edge
to also be part of the path. A cycle is a path of the form [i
Proposition 1 An assignment - to the variables in E violates transitivity if and only if some cycle
in G(E; -) contains exactly one 0-edge.
Proof: If. Suppose there is such a cycle. Letting i 1 be the vertex at one end of the 0-edge, we
can trace around the cycle, giving a sequence of vertices is the vertex at
the other end of the 0-edge. The assignment has -(e [i j ;i j+1
and hence it violates Equation 1.
Only If. Suppose the assignment violates a transitivity constraint given by Equation 1. Then,
we construct a cycle [i of vertices such that only edge (i
A path [i is said to be acyclic when i
is said to be simple when its prefix [i
Proposition 2 An assignment - to the variables in E violates transitivity if and only if some simple
cycle in G(E; -) contains exactly one 0-edge.
Proof: The "if" portion of this proof is covered by Proposition 1. The "only if" portion is
proved by induction on the number of variables in the antecedent of the transitivity constraint
(Equation 1.) That is, assume a transitivity constraint containing k variables in the antecedent is
violated and that all other violated constraints have at least k variables in their antecedents. If there
are no values p and q such that 1 - then the cycle [i
If such values p and q exist, then we can form a transitivity constraint:
This transitivity constraint contains fewer than k variables in the antecedent, but it is also violated.
This contradicts our assumption that there is no violated transitivity constraint with fewer than k
variables in the antecedent. 2
Define a chord of a simple cycle to be an edge that connects two vertices that are not adjacent
in the cycle. More precisely, for a simple cycle [i a chord is an edge (i
G(E) such that 1 - cycle is said to be
chord-free if it is simple and has no chords.
Proposition 3 An assignment - to the variables in E violates transitivity if and only if some chord-
contains exactly one 0-edge.
Proof: The "if" portion of this proof is covered by Proposition 1. The "only if" portion is
proved by induction on the number of variables in the antecedent of the transitivity constraint
(Equation 1.) Assume a transitivity constraint with k variables is violated, and that no transitivity
constraint with fewer variables in the antecedent is violated. If there are no values of p and q such
that there is a variable e [i p ;i q then the corresponding
cycle is chord-free. If such values of p and q exist, then consider the two cases illustrated in Figure
1, where 0-edges are shown as dashed lines, 1-edges are shown as solid lines, and the wavy lines
0-Edge 1-Edge

Figure

1: Case Analysis for Proposition 3. 0-Edges are shown as dashed lines. When a cycle representing
a transitivity violation contains a chord, we can find a smaller cycle that also represents
a transitivity violation.
represent sequences of 1-edges. Case 1: Edge (i 0-edge (shown on the left). Then the
transitivity constraint:
is violated and has fewer than k variables in its antecedent. Case 2: Edge (i 1-edge (shown
on the right). Then the transitivity constraint:
is violated and has fewer than k variables. Both cases contradict our assumption that there is no
violated transitivity constraint with fewer than k variables in the antecedent. 2
Each length k cycle [i given by the following clauses. Each
clause is derived by expressing Equation 1 as a disjunction.
(2)
For a set of relational variables E , we define F trans (E) to be the conjunction of all transitivity
constraints for all chord-free cycles in the graph G(E).
Theorem 1 An assignment to the relational variables E will satisfy all of the transitivity constraints
given by Equation 1 if and only if it satisfies F trans (E).
This theorem follows directly from Proposition 3 and the encoding given by Equation 2.
3.1 Enumerating Chord-Free Cycles
To enumerate the chord-free cycles of a graph, we exploit the following properties. An acyclic path
is said to have a chord when there is an edge (i
We classify a chord-free path as terminal when (i
is in G(E), and as extensible otherwise.
Proposition 4 A path [i is chord-free and terminal if and only if the cycle [i
is chord-free.
This follows by noting that the conditions imposed on a chord-free path are identical to those for a
chord-free cycle, except that the latter includes a closing edge (i
A proper prefix of path [i
Proposition 5 Every proper prefix of a chord-free path is chord-free and extensible.
Clearly, any prefix of a chord-free path is also chord-free. If some prefix [i
were terminal, then any attempt to add the edge (i would yield either a simple cycle
(when or a path having (i
as a chord.
Given these properties, we can enumerate the set of all chord-free paths by breadth first expan-
sion. As we enumerate these paths, we also generate C , the set of all chord-free cycles. Define P k
to be the set of all extensible, chord-free paths having k vertices, for 1 - k - N .
Initially we have ;. Given set P k , we generate set P k+1 and
add some cycles of length k + 1 to C . For each path [i we consider the path
for each edge (i
classify the path as cyclic. When there is an edge (i
classify the path as having a chord. When there is an edge (i we add the cycle
to C . Otherwise, we add the path to P k+1 .
After generating all of these paths, we can use the set C to generate the set of all chord-free
cycles. For each terminal, chord-free cycle having k vertices, there will be 2k members of C-
each of the k edges of the cycle can serve as the closing edge, and a cycle can traverse the closing
edge in either direction. To generate the set of clauses given by Equation 2, we simply need to
choose one element of C for each closing edge, e.g., by considering only cycles [i
which
As

Figure

2 indicates, there can be an exponential number of chord-free cycles in a graph.
In particular, this figure illustrates a family of graphs with 3n vertices. Consider the cycles
passing through the n diamond-shaped faces as well as the edge along the bottom. For each
diamond-shaped face F i , a cycle can pass through either the upper vertex or the lower vertex. Thus
there are 2 n such cycles. In addition, the edges forming the perimeter of each face F i create a
chord-free cycle, giving a total of cycles.
The columns labeled "Direct" in Table 2 show results for enumerating the chord-free cycles for
our benchmarks. For each correct microprocessor, we have two graphs: one for which transitivity
constraints played no role in the verification, and one (indicated with a "t" at the end of the name)
modified to require enforcing transitivity constraints. We summarize the results for the transitivity
@
@
@
@
@
@
@
@
@
@
@
@
@
@
@
@
@
@
oe
ae

Figure

2: Class of Graphs with Many Chord-Free Cycles. For a graph with n diamond-shaped
faces, there are cycles.
Circuit Direct Dense Sparse
Edges Cycles Clauses Edges Cycles Clauses Edges Cycles Clauses
1\ThetaDLX-C-t 37 95 348 78 286 858 42 68 204
2\ThetaDLX-CC-t 143 2,136 8,364 300 2,300 6,900 193 858 2,574
Full min. 89 1,446 6,360 231 1,540 4,620 132 430 1,290
Buggy avg. 124 2,562 10,270 300 2,300 6,900 182 750 2,244

Table

2: Cycles in Original and Augmented Benchmark Graphs. Results are given for the three
different methods of encoding transitivity constraints.
constraints in our 100 buggy variants of 2\ThetaDLX-CC in terms of the minimum, the average, and
the maximum of each measurement. We also show results for five synthetic benchmarks consisting
of n \Theta n planar meshes M n , with n ranging from 4 to 8, where the mesh for
in

Figure

3. For all of the circuit benchmarks, the number of cycles, although large, appears to be
manageable. Moreover, the cycles have at most 4 edges. The synthetic benchmarks, on the other
hand, demonstrate the exponential growth predicted as worst case behavior. The number of cycles
grows quickly as the meshes grow larger. Furthermore, the cycles can be much longer, causing the
number of clauses to grow even more rapidly.
3.2 Adding More Relational Variables
Enumerating the transitivity constraints based on the variables in E runs the risk of generating a
Boolean formula of exponential size. We can guarantee polynomial growth by considering a larger
set of relational variables. In general, let E 0 be some set of relational variables such that
and let F trans be the transitivity constraint formula generated by enumerating the chord-free
cycles in the graph G(E 0 ).
Theorem 2 If E is the set of relational variables in F sat and
F trans (E) is satisfiable if and only if F sat - F trans
We introduce a series of lemmas to prove this theorem. For a propositional formula F over a
set of variables A and an assignment -: A ! f0; 1g, define the valuation of F under -, denoted
, to be the result of evaluating formula F according to assignment -. We first prove that we
can extend any assignment over a set of relational variables to one over a superset of these variables
yielding identical valuations for both transistivity constraint formulas.
Lemma 1 For any sets of relational variables E 1 and E 2 such that assignment
1g, such that [F trans
there is an assignment
[F trans
Proof: We consider the case where g. The general statement of the proposition
then holds by induction on jE
assignment - 2 to be:
Graph G(E 1 ; -) has a path of 1-edges from node i to node j.
We consider two cases:
1. If - 2 (e i;j any cycle in G(E must contain a 0-edge other than
e i;j . Hence adding this edge does not introduce any transitivity violations.
2. If - 2 (e i;j there must be some path P 1 of 1-edges between nodes i and j in
In order for the introduction of 1-edge e i;j to create a transitivity violation, there
must also be some path P 2 between nodes i and j in G(E exactly one 0-
edge. But then we could concatenate paths P 1 and P 2 to form a cycle in G(E
exactly one 0-edge, implying that [F trans
We conclude therefore that adding
1-edge e i;j does not introduce any transitivity violations.Lemma 2 For assignment such that [F trans
also have [F trans
Proof: We note that any cycle in G(E must be present in G(E have the same
edge labeling. Thus, if G(E cycle with a single 0-edge, then neither does G(E now return to the proof of Theorem 2.
Proof: Suppose that F sat - F trans (E) is satisfiable, i.e., there is some assignment - such
that [F sat 1. Then by Lemma 1 we can find an assignment - 0 such that
[F trans Furthermore, since the construction of - 0 by Lemma 1 preserves the values
assigned to all variables in E , and these are the only relational variables occurring in F sat , we can
conclude that [F sat
Suppose on the other hand that F sat - F trans there is some assignment
- 0 such that [F sat
hence F sat - F trans (E) is satisfiable. 2
Our goal then is to add as few relational variables as possible in order to reduce the size of
the transitivity formula. We will continue to use our path enumeration algorithm to generate the
transitivity formula.
3.3 Dense Enumeration
For the dense enumeration method, let EN denote the set of variables e i;j for all values of i and
j such that 1 - Graph G(EN ) is a complete, undirected graph. In this graph,
any cycle of length greater than three must have a chord. Hence our algorithm will enumerate
transitivity constraints of the form e [i;j] - e [j;k] ) e [i;k] , for all distinct values of i, j, and k.
The graph has yielding a total of
The columns labeled "Dense" in Table 2 show the complexity of this method for the benchmark
circuits. For the smaller graphs 1\ThetaDLX-C, 1\ThetaDLX-C-t, M 4 and M 5 , this method yields more
clauses than direct enumeration of the cycles in the original graph. For the larger graphs, however,
it yields fewer clauses. The advantage of the dense method is most evident for the mesh graphs,
where the cubic complexity is far superior to exponential.
3.4 Sparse Enumeration
We can improve on both of these methods by exploiting the sparse structure of G(E). Like the
dense method, we want to introduce additional relational variables to give a set of variables
such that the resulting graph That is, the graph has the property
that every cycle of length greater than three has a chord.
Chordal graphs have been studied extensively in the context of sparse Gaussian elimination. In
fact, the problem of finding a minimum set of additional variables to add to our set is identical to
the problem of finding an elimination ordering for Gaussian elimination that minimizes the amount
of fill-in. Although this problem is NP-complete [Yan81], there are good heuristic solutions. In
Satisfiable? Secs. Satisfiable? Secs.
Full min. Y
Buggy avg. Y 125 Y 1,517 2.3

Table

3: Performance of FGRASP on Benchmark Circuits. Results are given both without and
with transitivity constraints.
particular, our implementation proceeds as a series of elimination steps. On each step, we remove
some vertex i from the graph. For every pair of distinct, uneliminated vertices j and k such that
the graph contains edges (i; j) and (i; k), we add an edge (j; it does not already exist. The
original graph plus all of the added edges then forms a chordal graph. To choose which vertex to
eliminate on a given step, our implementation uses the simple heuristic of choosing the vertex with
minimum degree. If more than one vertex has minimum degree, we choose one that minimizes the
number of new edges added.
The columns in Table 2 labeled "Sparse" show the effect of making the benchmark graphs
chordal by this method. Observe that this method gives superior results to either of the other two
methods. In our implementation we have therefore used the sparse method to generate all of the
transitivity constraint formulas.
SAT-Based Decision Procedures
Most Boolean satisfiability (SAT) checkers take as input a formula expressed in clausal form.
Each clause is a set of literals, where a literal is either a variable or its complement. A clause
denotes the disjunction of its literals. The task of the checker is to either find an assignment to the
variables that satisfies all of the clauses or to determine that no such assignment exists. We can
solve the constrained satisfiability problem using a conventional SAT checker by generating a set
of clauses C trans representing F trans set of clauses C sat representing the formula F sat .
We then run the checker on the combined clause set C sat [ C trans to find satisfying solutions to
In experimenting with a number of Boolean satisfiability checkers, we have found that FGRASP
[MS99] has the best overall performance. The most recent version can be directed to periodically
restart the search using a randomly-generated variable assignment [M99]. This is the first SAT
checker we have tested that can complete all of our benchmarks. All of our experiments were
conducted on a 336 MHz Sun UltraSPARC II with 1.2GB of primary memory.
As indicated by Table 3, we ran FGRASP on clause sets C sat and C trans [C sat , i.e., both without
and with transitivity constraints. For benchmarks 1\ThetaDLX-C, 2\ThetaDLX-CA, and 2\ThetaDLX-CC,
the formula F sat is unsatisfiable. As can be seen, including transitivity constraints increases the
run time significantly. For benchmarks 1\ThetaDLX-C-t, 2\ThetaDLX-CA-t, and 2\ThetaDLX-CC-t, the formula
F sat is satisfiable, but only because transitivity is not enforced. When we add the clauses
for F trans , the formula becomes unsatisfiable. For the buggy circuits, the run times for C sat range
from under 1 second to over 36 minutes. The run times for C trans [ C sat range from less than
one second to over 12 hours. In some cases, adding transitivity constraints actually decreased the
time (by as much as a factor of 5), but in most cases the CPU time increased (by as much as a
factor of 69). On average (using the geometric mean) adding transitivity constraints increased the
time by a factor of 2.3. We therefore conclude that satisfiability checking with transitivity
constraints is more difficult than conventional satisfiability checking, but the added complexity is
not overwhelming.
5 OBDD-Based Decision Procedures
A simple-minded approach to solving satisfiability with transitivity constraints using OBDDs
would be to generate separate OBDD representations of F trans and F sat . We could then use
the APPLY operation to generate an OBDD for F trans - F sat , and then either find a satisfying
assignment or determine that the function is unsatisfiable. We show that for some sets of relational
variables E , the OBDD representation of F trans (E) can be too large to represent and manipulate. In
our experiments, we use the CUDD OBDD package with dynamic variable reordering by sifting.
5.1 Lower Bound on the OBDD Representation of F trans (E)
We prove that for some sets E , the OBDD representation of F trans (E) may be of exponential
size for all possible variable orderings. As mentioned earlier, the NP-completeness result proved
by Goel, et al. [GSZAS98] has implications for the complexity of representing F trans (E) as an
OBDD. They showed that given an OBDD G sat representing formula F sat , the task of finding
a satisfying assignment of F sat that also satisfies the transitivity constraints in Trans(E) is NP-complete
in the size of G sat . By this, assuming P 6= NP , we can infer that the OBDD representation
of F trans (E) may be of exponential size when using the same variable ordering as is used in
G sat . Our result extends this lower bound to arbitrary variable orderings and is independent of the
vs. NP problem.
Let M n denote a planar mesh consisting of a square array of n \Theta n vertices. For example,

Figure

3 shows the graph for Being a planar graph, the edges partition the plane into faces.
As shown in Figure 3 we label these F i;j for 1 - 1. There are a total of (n
such faces. One can see that the set of edges forming the border of each face forms a chord-free
cycle of M n . As shown in Table 2, many other cycles are also chord-free, e.g., the perimeter of
any rectangular region having height and width greater than 1, but we will consider only the cycles
F 1;1 F 1;2 F 1;3 F 1;4 F 1;5
F 3;1 F 3;2 F 3;3 F 3;4 F 3;5
F 4;1 F 4;2 F 4;3 F 4;4 F 4;5
F 5;1 F 5;2 F 5;3 F 5;4 F 5;5

Figure

3: Mesh Graph M 6 .
corresponding to single faces.
n\Thetan to be a set of relational variables corresponding to the edges in M n . F trans (E n\Thetan )
is then an encoding of the transitivity constraints for these variables.
Theorem 3 Any OBDD representation of F trans (E n\Thetan ) must
vertices.
To prove this theorem, consider any ordering of the variables representing the edges in M n .
Let A denote those in the first half of the ordering, and B denote those in the second half. We can
then classify each face according to the four edges forming its border:
A: All are in A.
B: All are in B.
C: Some are in A, while others are in B. These are called "split" faces.
Observe that we cannot have a type A face adjacent to a type B face, since their shared edge cannot
be in both A and B. Therefore there must be split faces separating any region of type A faces from
any region of type B faces.
For example, Figure 4 shows three possible partitionings of the edges of M 6 and the resulting
classification of the faces. If we let a, b, and c denote the number of faces of each respective type,
we see that we always have c - In particular, a minimum value for c is achieved
when the partitioning of the edges corresponds to a partitioning of the graph into a region of type
A faces and a region of type B faces, each having nearly equal size, with the split faces forming
the boundary between the two regions.
A
A A A A
A
A A A A
A
A A A
A
A A
A
A
A
A C
A
A A
A
A
A
A
A
A A

Figure

4: Partitioning Edges into Sets A (solid) and B (dashed). Each face can then be classified
as type A (all solid), B (all dashed), or C (mixed).
Lemma 3 For any partitioning of the edges of mesh graph M n into equally-sized sets A and B,
there must be at least (n \Gamma 3)=2 split faces.
Note that this lower bound is somewhat weak-it seems clear that we must have c - n \Gamma 1.
However, this weaker bound will suffice to prove an exponential lower bound on the OBDD size.
Proof: Our proof is an adaptation of a proof by Leighton [Lei92, Theorem 1.21] that M n has
a bisection bandwidth of at least n. That is, one would have to remove at least n edges to split the
graph into two parts of equal size.
Observe that M n has n 2 vertices and 2n(n \Gamma 1) edges. These edges are split so that n(n \Gamma 1)
are in A and n(n \Gamma 1) are in B.
Let M D
n denote the planar dual of M n . That is, it contains a vertex u i;j for each face F i;j of
M n , and edges between pairs of vertices such that the corresponding faces in M n have a common
edge. In fact, one can readily see that this graph is isomorphic to M n\Gamma1 .
Partition the vertices of M D
n into sets U a , U b , and U c according to the types of their corresponding
faces. Let a, b, and c denote the number of elements in each of these sets. Each face of M n has
four bordering edges, and each edge is the border of at most two faces. Thus, as an upper bound
on a, we must have 4a - 2n(n \Gamma 1), giving a - n(n \Gamma 1)=2, and similarly for b. In addition, since
a face of type A cannot be adjacent in M n to one of type B, no vertex in U a can be adjacent in M D
to one in U b .
Consider the complete, directed, bipartite graph having as edges the set (U a \Theta U b ) [ (U b \Theta U a ),
i.e., a total of 2ab edges. Given the bounds: a
1)=2, the minimum value of 2ab is achieved when either
giving a lower bound:
We can embed this bipartite graph in M D
n by forming a path from vertex u i;j to vertex
where either u i;j 2 U a and u vice-versa. By convention, we will use the path that first
follows vertical edges to u i 0 ;j and then follows horizontal edges to u i 0 ;j 0 . We must have at least
one vertex in U c along each such path, and therefore removing the vertices in U c would cut all 2ab
paths.
For each vertex u i;j 2 U c , we can bound the total number of paths passing through it by
separately considering paths that enter from the bottom, the top, the left, and the right. For those
entering from the bottom, there are at most vertices and i(n \Gamma 1) destination
vertices, giving at most i(n paths. This quantity is maximized for
giving an upper bound of (n \Gamma 1) 3 =4. A similar argument shows that there are at most (n \Gamma 1) 3 =4
paths entering from the top of any vertex. For the paths entering from the left, there are at most
(j vertices and (n \Gamma destinations, giving at most (j \Gamma 1)(n
paths. This quantity is maximized when giving an upper bound of (n \Gamma 1) 3 =4. This
bound also holds for those paths entering from the right. Thus, removing a single vertex would cut
at most (n \Gamma 1) 3 paths.
Combining the lower bound on the number of paths 2ab, the upper bound on the number of
paths cut by removing a single vertex, and the fact that we are removing c vertices, we have:
We can rewrite
for all values of n, we have:
set of faces is said to be edge independent when no two members of the set share an edge.
Lemma 4 For any partitioning of the edges of mesh graph M n into equally-sized sets A and B,
there must be an edge-independent set of split faces containing at least (n \Gamma 3)=4 elements.
Proof: Classify the parity of face F i;j as "even" when even, and as "odd" otherwise.
Observe that no two faces of the same parity can have a common edge. Divide the set of split
faces into two subsets: those with even parity and those with odd. Both of these subsets are edge
independent, and one of them must have at least 1/2 of the elements of the set of all split faces. 2
We can now complete the proof of Theorem 3 Proof: Suppose there is an edge-independent set
of k split faces. For each split face, choose one edge in A and one edge in B bordering that face.
For each value ~y 2 f0; 1g k , define assignment ff ~y (respectively, fi ~y ), to the variables representing
edges in A (resp., B) as follows. For an edge e that is not part of any of the k split faces, define
ff ~y 0). For an edge e that is part of a split face, but it was not one of the ones
chosen specially, let ff 1). For an edge e that is the chosen variable in face i,
let ff ~y This will give us an assignment ff ~y \Delta fi ~y to all of the variables
that evaluates to 1. That is, for each independent, split face F i , we will have two 1-edges when
cycles in the graph will have at least two 0-edges.
On the other hand, for any ~y; ~z 2 f0; 1g k such that ~y 6= ~z the assignment ff ~y \Delta fi ~z will cause an
evaluation to 0, because for any face i where y i 6= z i , all but one edge will be assigned value 1.
Thus, the set of assignments fff ~y j~y 2 f0; 1g k g forms an OBDD fooling set, as defined in [Bry91],
implying that the OBDD must have at least 2 k - 2 (n\Gamma3)=4
We have seen that adding relational variables can reduce the number of cycles and therefore
simplify the transitivity constraint formula. This raises the question of how adding relational variables
affects the BDD representation of the transitivity constraints. Unfortunately, the exponential
lower bound still holds.
Corollary 1 For any set of relational variables E such that E n\Thetan ' E , any OBDD representation
of F trans (E) must
vertices.
The extra edges in E introduce complications, because they create cycles containing edges
from different faces. As a result, our lower bound is weaker.
Define a set of faces as vertex independent if no two members share a vertex.
Lemma 5 For any partitioning of the edges of mesh graph M n into equal-sized sets A and B,
there must be a vertex-independent set of split faces containing at least (n \Gamma 3)=8 elements.
Proof: Partition the set of split faces into four sets: EE, EO, OE, and OO, where face F i;j is
assigned to a set according to the values of i and j:
EE: Both i and j are even.
EO: i is even and j is odd.
OE: i is odd and j is even.
OO: Both i and j are odd.
Each of these sets is vertex independent. At least one of the sets must contain at least 1=4 of
the elements. Since there are at least (n \Gamma 3)=2 split faces, one of the sets must contain at least
vertex-independent split faces. 2
We can now prove Corollary 1.
Proof: For any ordering of the variables in E , partition them into two sets A and B such
that those in A come before those in B, and such the number of variables that are in E n\Thetan are
equally split between A and B. Suppose there is a vertex-independent set of k split faces. For
each value ~y 2 f0; 1g k , we define assignments ff ~y to the variables in A and fi ~y to the variables
in B. These assignments are defined as they are in the proof of Theorem 3 with the addition that
each variable e i;j in n\Thetan is assigned value 0. Consider the set of assignments ff ~y \Delta fi ~z for
all values ~y; ~z 2 f0; 1g k . The only cycles in G(E; ff ~y \Delta fi ~z ) that can have less than two 0-edges
will be those corresponding to the perimeters of split faces. As in the proof of Theorem 3, the set
fff ~y j~y 2 f0; 1g k g forms an OBDD fooling set, as defined in [Bry91], implying that the OBDD
must have at least 2 k - 2 (n\Gamma3)=8
Our lower bounds are fairly weak, but this is more a reflection of the difficulty of proving
lower bounds. We have found in practice that the OBDD representations of the transitivity constraint
functions arising from benchmarks tend to be large relative to those encountered during the
evaluation of F sat . For example, although the OBDD representation of F trans
1\ThetaDLX-C-t is just 2,692 nodes (a function over 42 variables), we have been unable to construct the
OBDD representations of this function for either 2\ThetaDLX-CA-t (178 variables) or 2\ThetaDLX-CC-t
(193 variables) despite running for over 24 hours.
5.2 Enumerating and Eliminating Violations
Goel, et al. [GSZAS98] proposed a method that generates implicants (cubes) of the function F sat
from its OBDD representation. Each implicant is examined and discarded if it violates a transitivity
constraint. In our experiments, we have found this approach works well for the normal, correctly-
designed pipelines (i.e., circuits 1\ThetaDLX-C, 2\ThetaDLX-CA, and 2\ThetaDLX-CC) since the formula F sat
is unsatisfiable and hence has no implicants. For all 100 of our buggy circuits, the first implicant
generated contained no transitivity violation and hence was a valid counterexample.
For circuits that do require enforcing transitivity constraints, we have found this approach im-
practical. For example, in verifying 1\ThetaDLX-C-t by this means, we generated 253,216 implicants,
requiring a total of 35 seconds of CPU time (vs. 0.2 seconds for 1\ThetaDLX-C). For benchmarks
2\ThetaDLX-CA-t and 2\ThetaDLX-CC-t, our program ran for over 24 hours without having generated all
of the implicants. By contrast, circuits 2\ThetaDLX-CA and 2\ThetaDLX-CC can be verified in 11 and 29
seconds, respectively. Our implementation could be improved by making sure that we generate
only implicants that are irredundant and prime. In general, however, we believe that a verifier that
generates individual implicants will not be very robust. The complex control logic for a pipeline
can lead to formulas F sat containing very large numbers of implicants, even when transitivity plays
only a minor role in the correctness of the design.
5.3 Enforcing a Reduced Set of Transitivity Constraints
One advantage of OBDDs over other representations of Boolean functions is that we can readily
determine the true support of the function, i.e., the set of variables on which the function depends.
This leads to a strategy of computing an OBDD representation of F sat and intersecting its support
with E to give a set -
of relational variables that could potentially lead to transitivity violations.
We then augment these variables to make the graph chordal, yielding a set of variables -
Circuit Verts. Direct Dense Sparse
Edges Cycles Clauses Edges Cycles Clauses Edges Cycles Clauses
1\ThetaDLX-C-t 9
Reduced min. 3
Buggy avg. 12 17 19 75 73 303 910 21 14 42
2\ThetaDLX-CC max. 19 52 378 1,512 171 969 2,907 68 140 420

Table

4: Graphs for Reduced Transitivity Constraints. Results are given for the three different
methods of encoding transitivity constraints based on the variables in the true support of F sat .
Circuit OBDD Nodes CPU
Reduced min. 20 1 20 7
Buggy avg. 3,173 1,483 25,057 107
2\ThetaDLX-CC max. 15,784 93,937 438,870 2,466

Table

5: OBDD-based Verification. Transitivity constraints were generated for a reduced set of
variables -
generate an OBDD representation of F trans ( -
it is
satisfiable, generate a counterexample.

Table

4 shows the complexity of the graphs generated by this method for our benchmark cir-
cuits. Comparing these with the full graphs shown in Table 2, we see that we typically reduce the
number of relational vertices (i.e., edges) by a factor of 3 for the benchmarks modified to require
transitivity and by an even greater factor for the buggy circuit benchmarks. The resulting graphs
are also very sparse. For example, we can see that both the direct and sparse methods of encoding
transitivity constraints greatly outperform the dense method.

Table

5 shows the complexity of applying the OBDD-based method to all of our bench-
marks. The original circuits 1\ThetaDLX-C, 2\ThetaDLX-CA, and 2\ThetaDLX-CC yielded formulas F sat
that were unsatisfiable, and hence no transitivity constraints were required. The 3 modified circuits
1\ThetaDLX-C-t, 2\ThetaDLX-CA-t, and 2\ThetaDLX-CC-t are more interesting. The reduction in the
number of relational variables makes it feasible to generate an OBDD representation of the transitivity
constraints. Compared to benchmarks 1\ThetaDLX-C, 2\ThetaDLX-CA, and 2\ThetaDLX-CC, we see
there is a significant, although tolerable, increase in the computational requirement to verify the
modified circuits. This can be attributed to both the more complex control logic and to the need to
apply the transitivity constraints.
For the 100 buggy variants of 2\ThetaDLX-CC, F sat depends on up to 52 relational variables,
with an average of 17. This yielded OBDDs for F trans ( -
ranging up to 93,937 nodes, with
an average of 1,483. The OBDDs for F sat - F trans ( -
ranged up to 438,870 nodes (average
25,057), showing that adding transitivity constraints does significantly increase the complexity of
the OBDD representation. However, this is just one OBDD at the end of a sequence of OBDD
operations. In the worst case, imposing transitivity constraints increased the total CPU time by a
factor of 2, but on average it only increased by 2%. The memory required to generate F sat ranged
from 9.8 to 50.9 MB (average 15.5), but even in the worst case the total memory requirement
increased by only 2%.
6 Conclusion
By formulating a graphical interpretation of the relational variables, we have shown that we can
generate a set of clauses expressing the transitivity constraints that exploits the sparse structure
of the relation. Adding relational variables to make the graph chordal eliminates the theoretical
possibility of there being an exponential number of clauses and also works well in practice.
A conventional SAT checker can then solve constrained satisfiability problems, although the run
times increase significantly compared to unconstrained satisfiability. Our best results were obtained
using OBDDs. By considering only the relational variables in the true support of F sat , we
can enforce transitivity constraints with only a small increase in CPU time.



--R

"Graph-based algorithms for Boolean function manipulation"
"On the complexity of VLSI implementations and graph representations of Boolean functions with application to integer multiplication,"
"Exploiting positive equality in a logic of equality with uninterpreted functions,"
"Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic,"
"Automated verification of pipelined microprocessor control,"
"Techniques for verifying superscalar microprocessors,"
"BDD based procedures for a theory of equality with uninterpreted functions,"
Computer Architecture: A Quantitative Ap- proach
Introduction to Parallel Algorithms and Architectures: Arrays
"GRASP: A search algorithm for propositional satisfiability,"
"The impact of branching heuristics in propositional satisfiability algorithms,"
"Triangulated graphs and the elimination process,"
"Superscalar processor verification using efficient reductions of the logic of equality with uninterpreted functions,"
"Computing the minimum fill-in is NP-complete,"
--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
Introduction to parallel algorithms and architectures
Techniques for verifying superscalar microprocessors
Computer architecture (2nd ed.)
GRASP
Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic
Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW
Chaff
The Impact of Branching Heuristics in Propositional Satisfiability Algorithms
Superscalar Processor Verification Using Efficient Reductions of the Logic of Equality with Uninterpreted Functions to Propositional Logic
BDD Based Procedures for a Theory of Equality with Uninterpreted Functions
Automatic verification of Pipelined Microprocessor Control
Exploiting Positive Equality in a Logic of Equality with Uninterpreted Functions

--CTR
Miroslav N. Velev, Efficient formal verification of pipelined processors with instruction queues, Proceedings of the 14th ACM Great Lakes symposium on VLSI, April 26-28, 2004, Boston, MA, USA
Miroslav N. Velev, Using positive equality to prove liveness for pipelined microprocessors, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.316-321, January 27-30, 2004, Yokohama, Japan
Miroslav N. Velev, Using Abstraction for Efficient Formal Verification of Pipelined Processors with Value Prediction, Proceedings of the 7th International Symposium on Quality Electronic Design, p.51-56, March 27-29, 2006
Miroslav N. Velev, Efficient translation of boolean formulas to CNF in formal verification of microprocessors, Proceedings of the 2004 conference on Asia South Pacific design automation: electronic design and solution fair, p.310-315, January 27-30, 2004, Yokohama, Japan
Miroslav N. Velev , Randal E. Bryant, Effective use of boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors, Journal of Symbolic Computation, v.35 n.2, p.73-106, February
Miroslav N. Velev, Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors, Proceedings of the conference on Design, automation and test in Europe, p.10266, February 16-20, 2004
Robert Nieuwenhuis , Albert Oliveras , Cesare Tinelli, Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T), Journal of the ACM (JACM), v.53 n.6, p.937-977, November 2006
boolean satisfiability;formal verification;decision procedures