Article Preview
TopIntroduction
The checking of software and electrical circuit is crucial element to detect the errors which they contain or to show that they function well. One of the most used verification methods used is the model-checking (Clarke, 1994). However, the great difficulty encountered in the domain of formal verification is the combinatorial explosion problem. For example in the model checking, the number of states in the transition graphs can reach prohibitive level, which makes their manipulation difficult or impossible. Consequently, compression methods are used in order to reduce the size of the state graph. The compression is done by using data structures in order to represent in a concise manner the set of states. In this case, the operations are done so on set of states rather than on explicit states.
The representation by the Binary Decision Diagrams BDD is among the most known symbolic notations (Akers, 1978; Drechsler & Becker, 1998). The BDD is a data structure used to efficiently represent Boolean functions. Since they offer a canonical representation and an easy manipulation, the BDD is largely used in several fields such as the logic synthesis (Hachtel & Somenzi, 2006) and the formal verification (Hu, Dill, Drexler, & Yang, 1992). However, the BDD size depends strongly on the selected variable order. Therefore it is important to find a variable order which minimizes the number of nodes in a BDD. The BDD variable order is very important especially in the symbolic model checking, employed in the formal verification of digital circuits and other finite state systems (McMillan, 1992). The exact methods used to resolve this problem are based on dynamic programming with pruning to find the optimal order (Ishiura, Sawada, & Yajima, 1991; Drechsler, Drechsler, & Slobodova, 1998; Friedman & Supowit, 1987). Unfortunately, these methods are not practicable for large instances considering the fact that there are an exponential number of possible variable orders. Indeed, the problem of variable ordering has been shown to be Np-difficult (Bollig & Wegener, 2002). For that, several heuristics were proposed to find the best BDD variable order and which can be classified in two categories. The first class tries to extract the good order by inspecting the logical circuits (Fujii, Ootomo, & Hori, 1988; Fujita, Fujisawa, & Kawato, 1988), whereas, the second class is based on the dynamic optimization of a given order (Meinel & Slobodova, 1997; Ishiura, Sawada, & Yajima, 1991). The Sifting algorithm introduced by Rudell (1993) constitutes one of the most successful algorithms for dynamic reordering of variables. This algorithm is based on finding the best position of a variable in the order by moving the variable to all possible positions while preserving the other variables static. There are other methods based on metaheuristics like genetic algorithms (Drechsler, Becker, & Göckel, 1996; Costa, Déharbe, & Moreira, 2000), simulated annealing (Bollig, Löbbing, & Wegener, 1995), and scatter search algorithm (Hung & Song, 2001).