SML - A High Level Language for the Design and Verification of Finite State Machines

CMU-CS-85-179

Michael C. Browne, Edmund M. Clarke

November 1985

Finite state machines are common components of VLSI circuits. Because they occur so frequently, many design tools have been written to layout finite state machines as PALs, PLAs, etc. Unfortunately, most of these tools require the user to enter the complete state transition table of the machine. If the number of states is large, this can be a difficult and error-prone process. Furthermore, large state transition tables are not easy for others to understand.

In order to assist with the design of finite state machines, we have designed a programming language named SML State Machine Language . In addition to being useful for design, SML can also be a documentation aid, since it provides a succinct notation for describing complicated finite state machines. A program written in SML can be compiled into a state transition table that can then be implemented in hardware using an appropriate design tool. The resulting state transition table can also be given to a temporal logic model checker that allows certain properties of the state machine to be automatically verified. This is discussed extensively in some of our other papers, and will not be mentioned here.

17 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by reports@cs.cmu.edu