Functional verification and simulation of FSM networks

Presents a method to functionally verify a network of interacting finite state machines (FSMs) at any level of abstraction. The verification tool developed can verify the FSM network at various stages of the synthesis process. It can verify the result of FSM decomposition both in the symbolic and binary-coded form. The tool has various options to help the designer in the synthesis of a decomposed sequential machine system. It can generate the decomposed submachines for a given decomposition from the prototype specification. It can also be used to simulate the network. An efficient enumeration-simulation method is used to traverse the state transition graph of the prototype machine in a depth first fashion. The algorithm can be used to verify the decomposed system even if the decomposition information is not known, thus allowing it to verify any FSM network.<>