Finite state machine verification on MIMD machines

The authors present a parallel algorithm for finite state machine (FSM) verification on multiple instruction/multiple data (MIMD) machines. Given two FSMs, the verification process consists of dynamically constructing the product machine and investigating the reachability of the failure state (from the start state) of the product machine in a distributed fashion. The technique partitions one of the FSMs across a set of processors by distributing the states of the FSM among the processors. Experimental results on benchmark circuits demonstrate near linear speedup