Automata-based symbolic scheduling is a set of techniques for representing the high-level behavior of a digital subsystem as a collection of nondeterministic finite automata, NFA. Desired behavioral and implementation dynamics: dependencies, repetition, bounded resources, sequential character, and control state, can also be similarly modeled. All possible system execution sequences, obeying imposed constraints, are encapsulated in a composed NFA. Technology similar to that used in symbolic model checking enables implicit exploration and extraction of best-possible execution sequences. This provides a very general, systematic procedure to perform exact high-level synthesis of cyclic, control-dominated behaviors constrained by arbitrary sequential constraints. This dissertation further demonstrates that these techniques are scalable to practical problem sizes and complexities. Exact scheduling solutions are constructed for a variety of academic and industrial problems, including a pipelined RISC processor. The ability to represent and schedule sequential models with hundreds of tasks and one-half million control cases substantially raises the bar as to what is believed possible for exact scheduling models.
Keywords: Scheduling; Binary Decision Diagrams; High-Level Synthesis; Nondeterminism; Automata; Symbolic Model.
