Finite-state machine verification, test, and minimization

Finite-state machines (FSMs) have been widely used to model systems in various domains such as sequential circuits, lexical analysis and pattern matching programs, and more recently, communication protocols. Since FSMs are widely used to model hardware and software systems, their verification and test are important. This dissertation presents techniques for verification and state minimization of FSMs. Checking sequence construction and test suite generation based on a coverage metric are presented for both asynchronous FSMs (AFSMs) and synchronous FSMs (SFSMs). This coverage metric is extended for cascaded FSMs. Symbolic input based coverage metric is proposed for large FSMs. The coverage analysis is adopted for the verification of the AFSMs and a verification algorithm for AFSMs is presented. Finally, a technique for state minimization of incompletely specified FSMs is presented.