An extended OBDD representation for extended FSMs

This paper presents a subset of the predicate calculus, called the case calculus, which is suitable for describing Extended Finite State Machines (EFSMs). EFSMs can be used as abstract models of combined datapath and control systems. Case expressions can be represented using Extended Ordered Binary Decision Diagrams (EOBDDs) that are compact, allow an efficient implementation of logical operations on expressions, and have a unique form for many semantically equivalent expressions. Operations for formal verification and synthesis based on EFSM models, such as the “pre” and “post"” operations on sets of states, can be efficiently implemented. We illustrate the usefulness of EOBDDs in design verification and microcode synthesis