A finitestate machine may have more reachable states than it needs to perform its observable function (n.b. onehot coding does not increase the reachable state space).
A Moore machine can be simplified by the following procedure:

Alternative algorithm: start with one partition per state and repeatedly conglomerate. The best algorithms use a mixture of the two approaches to meet in the middle.
»Wikipedia: Formal Equivalence Checking
Research example: CADP package: developed by the VASY team at INRIA.
Commercial products: Conformal by Cadence, Formality by Synopsys, SLEC by Calypto.
One future use of this sort of procedure might be to generate an instruction set simulator for a processor from its full RTL implementation. This sort of depipelining would give a noncycle accurate, higherlevel model that runs much faster in simulation.
29: (C) 201218, DJ Greaves, University of Cambridge, Computer Laboratory. 