Automatic verification of finite state machines using temporal logic

Finite state machines are common components of VLSI circuits. Because they occur so frequently, much effort has been spent building tools to assist in their design and verification. Since the proper sequencing of events is of paramount importance to the correct operation of a finite state machine, it is not surprising that temporal logics have been applied to the verification problem. These logics were originally developed by philosophers specifically for reasoning about the ordering of events in time. One of the first applications was the CTL model checking procedure developed by Clarke and Emerson, in which the truth of a formula of a branching-time temporal logic in a labelled state transition graph could be determined in time that was linear in both the size of the structure and the length of the formula. Although this algorithm has been shown to be very useful in the verification of several hardware controllers, it suffers from a number of serious drawbacks. These deficiencies include a notion of a finite state machine that does not permit external events to effect transitions, a lack of compositionality, and an inability to generalize between similar systems of different sizes. In this thesis, a number of alternative techniques are proposed to solve these problems. In particular, a new model checking algorithm that can deal with conditional transitions is introduced and analyzed. A theory is presented concerning the equivalence of finite state machines with respect to the preservation of temporal logic properties. Finally, this theory is used to develop a method to generalize between systems composed of differing numbers of similar finite state machines.