Computing subsets of equivalence classes for large FSMs

Computing equivalence classes for FSMs has several applications to synthesis and verification problems. Symbolic traversal techniques are applicable to medium-small circuits. This paper extends their use to large FSMs by means of cofactor-based enhancements to the state-of-the-art approaches and of underestimations of equivalence classes. The key to success is pruning the search space by constraining it. Experimental results on some of the larger ISCAS´89 and MCNC circuits show its applicability