Exploiting functional dependencies in finite state machine verification
C.A.J. van Eijk, J.A.G. Jess · 1996
This paper proposes a novel verification method for finite state machines (FSMs), which automatically exploits the relation between the state encodings of the FSMs under consideration. It is based on the detection and utilization of functionally dependent state variables. This significantly extends the ability of the verification method to handle FSMs with similar state encodings. The effectiveness of the proposed method is illustrated by experimental results on well-known benchmarks. 1. Introduction During the design of digital circuits, several descriptions of a design are generated at various levels of detail. Verifying the consistency of these descriptions is an important aspect of the design process. At the logic level, a circuit is usually modeled as a finite state machine (FSM). Therefore, it is important to have algorithms which can efficiently verify the equivalence of FSMs. Impressive progress has been made in this area by the introduction of so-called symbolic techniques, w...