Evolutionary algorithm approach for symbolic FSM traversals
Mitchell Aaron Thornton, Rolf Drechsler · 2002
State space traversal algorithms for finite state machine (FSM) models of synchronous sequential circuitry are used extensively in various formal verification approaches such as equivalence checking (EC) and model checking. Symbolic binary decision diagram (BDD) based approaches have allowed many FSM models to be verified due to the compact representations they provide. However, there still remain circuits for which the traversal cannot be carried out due to the size of the transition relation (TR) BDD becoming too large. Pruning algorithms designed to reduce the size of a BDD while maintaining as much functionality as possible are examined for here. These techniques are based upon evolutionary algorithms that have been shown to significantly reduce the size of BDD while retaining a large amount of functionality.