The course is a systematic study of Finite State Machine synthesis and verification methods. Presented are two new practical approaches to specification and design of state machines. The first one starts with the FSM represented on a high (functional) level as a set of boolean constraints describing relations between the input and output signals. The second one is a user-friendly adaptation of the known state-transition graph representation of FSMs. Both approaches can be used interchangably. They allow the designer to capture subtle behavioral properties of FSMs and influence the results of synthesis at the initial stages of the design process.
Along with the "classical" algorithms for state minimization and state encoding of FSM starting from state transition graphs, a number of new approaches to FSM design are discussed, in particular those that do not require sophisticated computation yet allow for a variety of encoding strategies, flip-flop types, and clocking schemes. The presented material includes recent advances in FSM decomposition and a number of approaches to FSM verification. Presentation of all synthesis and verification algorithms is based on Binary Decision Diagrams, a state-of-the-art data structure for discrete function manipulation widely used in modern CAD tool.
Specification and algorithms, applicable to industrial
benchmarks, are first illustrated with simple examples. Experimental visual
software is used to demostrate new synthesis methods.