A language for compositional specification and verification of finite state hardware controllers

The authors consider the state machine language (SML) for describing complex finite state hardware controllers. It provides many of the standard control structures found in modern programming languages. The state tables produced by the SML compiler can be used as input to a temporal logic model checker that can automatically determine whether a specification in the logic CTL is satisfied. The authors describe extensions to SML for the design of modular controllers. These extensions allow a compositional approach to model checking which can substantially reduce its complexity. To demonstrate these methods, the authors discuss the specification and verification of a simple central-processing-unit (CPU) controller