Formal Verification Tool for Variable Order Analysis Algorithm in Binary Decision Diagrams

Abstract

A number of problems in digital system design, combinatorial optimization, or mathematical logic can be formulated in terms of Boolean functions. A concise representation which can also provide fast manipulation is very •important for .\3oolean functions manipulation. Ordered Binary Decision Diagrams (OBDDs) provide a well known data structure for efficiel)t Boolean function manipulation and widely used in many fields..

The size of an OBDD and the complexity of its manipulation depends on the variable order. The OBDD size varies from linear to exponential in the number of input bits.Due to the strong dependence of the OBDD size upon the chosen variable order it is one of the most important problems in the use of OBDDs to construct good orders. However the pi'oblem to construct an optimal order of a given OBDD is NP-hard.

In this thesis, we focus on the variable ordering problem. We study the effect of variable ordering on the OBDD size, and implement static heuristics techniques, dynamic reordering, and genetic algorithms, and we compared their performance.

Based on this comparison, we proposed a novel dynamic reordering algorithm. The algorithm is based on finding the best variable ordering by swapping the order of two adjacent variables. Also, we proposed an enhancement to the genetic algorithm used in solving the problem of