BDD-based conjunctive decomposition using a genetic algorithm and dependent variable affinity

Decomposition is an important strategy in synthesis and verification. BDD-based conjunctive decomposition has been successfully used in verification, especially in image computations for finite state machine (FSM) state-space traversals. Conjunction decomposition also has applications in other areas of CAD. A "two-step" algorithm for representing a large function as a conjunctive decomposition of BDDs is described where a genetic algorithm (GA) approach for ordering individual bit functions is given followed by an affinity-based clustering technique. Experimental results are given that show the effectiveness of the algorithm.