A genetic approach for conjunction scheduling in symbolic equivalence checking

A key issue in symbolic equivalence checking algorithms is image computation. Conjunction scheduling is a strategy to keep the size of BDDs small for the intermediate results of image computation. Conjunction scheduling consists of ordering bit transition relations, clustering subsets of them and ordering the clusters. We present a genetic algorithm (GA) approach for conjunction scheduling based on the dependency matrix of transition relations. Our GA approach offers improvement over existing algorithms by minimizing the active lifetime of variables at the same time. Our experimental results show the effectiveness of the algorithm.