Under the auspices of the Computational Complexity Foundation (CCF)

ECCC BOOKS, LECTURES AND SURVEYS > RESTRICTED BRANCHING PROGRAMS AND HARDWARE VERIFICATION:

## Restricted Branching Programs and Hardware Verification

Abstract

This thesis concerns the complexity of branching programs with limitations on the way in which variables may be read.

Interest in such branching programs has been raised recently by a popular method for verifying hardware circuits. In particular, oblivious read-once branching programs (or OBDD's ), have been found very useful in this application. The major shortcoming of this method has been the lack of a class of branching programs that can both (1) be easily manipulated (combined and tested for equivalence) and (2) compute multiplication in polynomial size. Many types of oblivious branching programs have been considered, each requiring exponential size for multiplication.

We present a lower bound of 2^\Omega(\sqrt{n}) on the size of read-once branching programs computing multiplication. This is the first nontrivial lower bound for multiplication on branching programs that are not oblivious. By the appropriate problem reductions, we obtain the same lower bound for other arithmetic functions.

We also survey the various alternative models, describing the main techniques used for thinking about their computation and for proving lower bounds. These techniques are illustrated with two proofs that have not appeared in the literature. We summarize the structural results, comparing the complexity classes corresponding to the various models.


1.  Introduction............................................................9
1.1  The role of branching programs in hardware verification............9
1.2  Restricted branching programs.....................................11

2.  Related Models.........................................................15

2.1  Definitions.......................................................16
2.2  Manipulating branching programs...................................19
2.3  Previous lower bounds.............................................21
2.4  Comparing the models: classes and structural results..............23
2.5  Lower bound techniques............................................28
2.6  Integer multiplication............................................37
2.7  Related issues....................................................40

3.  A lower bound for multiplication with read-once programs...............45