Binary decision diagrams and their applications to implicit enumeration techniques in logic synthesis
Seh-Woong Jeong · 1992
Logic synthesis is the process of deriving an implementation of logic gates and transistors from a specification of a desired function. Many problems in logic synthesis require that the solution space should be searched exhaustively to solve the problems exactly. It is infeasible to consider all possible solutions in the search space explicitly for such problems. For example, if the solution space is given $\{0,1\}\sp{n}$ (that is, an n Boolean space), there exist 2$\sp{n}$ possible solutions in the search space. Instead of the explicit search, if a subset of solutions of the search space has the common characteristic to the given problem so that we do not have to enumerate all solutions in the subset, then it is possible to reduce our search efforts significantly. We call this search technique implicit enumeration. In this thesis, we present efficient implicit enumeration algorithms based on binary decision diagrams (BDD) for the following basic problems: (1) Image Computation. (2) Pre-Image Computation. (3) Binate Covering Problem. We use our new implicit enumeration algorithms for the resettability analysis of finite state machines and the exact Boolean relation minimization, to demonstrate the efficiencies of the algorithms. BDD is a Boolean function representation. In addition to the fact that BDD is a canonical representation, BDD representations for many Boolean functions encountered in logic synthesis have reasonable sizes. One concern about BDD is the variable ordering problem. In this thesis, we present some theorems (called non-interleaving theorems) to provide the optimality criterion for n-composed functions as well as an intuition for some existing ordering heuristics. The theorems are also very useful for the problems where there are no circuits we can refer to for computing a good variable order. The exact Boolean relation minimization problem is such a problem that we do not have any reference circuit for computing a variable order. However, the non-interleaving theorems provide the strong theoretical background for the ordering heuristic used in the exact Boolean relation minimization problem.