ALGORITHMS FOR APPROXIMATE FSM TRAVERSAL BASED ON STATE-SPACE DECOMPOSITION

This paper presents algorithms for approximate finite state machine tr aversal based on state space decomposition, The original finite state machine is partitioned in component submachines, and each of them is t raversed separately; the result of the computation is an over-estimati on of the set of reachable states of the original machine. Different t raversal strategies, which reduce the effects of the degrees of freedo m introduced by the decomposition, are discussed, Efficient partitioni ng is a key point for the performance of the traversal techniques; a m ethod to heuristically find a good decomposition of the overall finite state machine, based on the exploration of its state variable depende ncy graph, is proposed, Applications of the approximate traversal meth ods to logic optimization of sequential circuits and behavioral verifi cation of finite state machines are described; experimental results fo r such applications, together with data concerning pure traversal, are reported.