An Efficient Verifier for Finite-State Machines

Abstract

In the hierarchical design/verification paradigm, submodules of low level abstraction are often finite state machines. In this case, the verification problem is to check the correctness of the design with respect to the specification rather than to check the equivalence of two machines. Most previous work on finite state machine verification deals with equivalence checking and few of these techniques have been widely used in practice due to their low efficiency. In this paper, the concept of machine cover is revived and the verification problem of the design correctness of finite state machines is formulated based on the concept of machine cover. Since in general the state encoding information is not available for verification purposes, it is assumed that the encoding information is missing. An efficient algorithm for the verification problem is presented along with its implementation. Experimental results show that the approach is promising in terms of speed.