FSM DECOMPOSITION AND FUNCTIONAL VERIFICATION OF FSM NETWORKS

Here we present a new method for the decomposition of a Finite State M achine (FSM) into a network of interacting FSMs and a framework for th e functional verification of the FSM network at different levels of ab straction. The problem of decomposition is solved by output partitioni ng and state space decomposition using a multiway graph partitioning t echnique. The number of submachines is determined dynamically during t he partitioning process. The verification algorithm can be used to ver ify (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-simu lation method which involves traversal of the state transition graph o f the prototype machine and simulation of the decomposed machine netwo rk. Both the decomposition and verification/simulation algorithms have been implemented as part of an interactive FSM synthesis system and t ested on a set of benchmark examples.