Implicit computation of compatible sets for state minimization of ISFSMs

The computation of sets of compatibles of incompletely specified finite-state machines (ISFSMs) is a key step in sequential synthesis. This paper presents implicit computations to obtain sets of maximal compatibles, compatibles, prime compatibles, implied sets, and class sets. The computations are implemented by means of BDDs that realize the characteristic functions of these sets. We have demonstrated with experiments from a variety of benchmarks that implicit techniques allow us to handle examples exhibiting a number of compatibles up to 2¹⁵⁰⁰, an achievement outside the scope of programs based on explicit enumeration. We have shown, in practice, that ISFMSs with a very large number of compatibles may be produced as intermediate steps of logic synthesis algorithms, for instance, in the case of asynchronous synthesis. This shows that the proposed approach not only has a theoretical interest, but also practical relevance for current logic synthesis applications, as shown by its application to ISFSM state minimization