FSM Decomposition and Functional Verification of FSM Networks

Here we present a new method for the decomposition of a Finite State Machine (FSM) into a network of interacting FSMsand a framework for the functional verification of the FSM network at different levels of abstraction. The problem ofdecomposition is solved by output partitioning and state space decomposition using a multiway graph partitioningtechnique. The number of submachines is determined dynamically during the partitioning process. The verificationalgorithm can be used to verify (a) the result of FSM decomposition on a behavioral level, (b) the encoded FSM network,and (c) the FSM network after logic optimization. Our verification technique is based on an efficient enumeration-simulationmethod which involves traversal of the state transition graph of the prototype machine and simulation of the decomposedmachine network. Both the decomposition and verification/simulation algorithms have been implemented as part of aninteractive FSM synthesis system and tested on a set of benchmark examples