Browse Theses

The discipline of applicative program design style is adapted to the design of synchronous systems. The result is a powerful and natural methodology for engineering correct hardware implementations. This dissertation makes a formal connection between functional recursion and component connectivity that is pleasantly direct, suggesting that applicative notation is the appropriate basis for digital design.

Synthesis is a theory for constructing concretely descriptive realizations from abstractly descriptive specifications. Functional recursion equations serve here as specifications; the realization language uses signal equations to describe circuit connectivity. A semantics for realizations assigns an infinite value sequence to each signal. The register equation X = a ! t, where t is an applicative term, defines signal X to be the output a register initialized to a. Synchronous systems are characterized by iterative specifications over a single function symbol (simple while-loops). Moreover, the transcription from F(x(,1),..., x(,n)) p (--->) r, F(t(,1),..., t(,n)) to the canonical realization {X(,i) = a(,i) ! t(,i)} is immediate and correct. Realizations can be compiled from arbitrary iterative specifications by a familiar construction. In non-iterative cases synthesis of iterative form is the main tactic used here for deriving realizations. This subgoal formalizes the conventional technique of decomposing a circuit into an architecture and a finite state controller.

This approach suggests yet another way to implement "function recursion" with "data recursion." An interpreter has been implemented for Daisy, a demand-driven list processing language. By representing signals as infinite lists, expressed realizations can be directly interpreted, resulting in a simulation of logical behavior. Thus, the engineering notation serves also as a vehicle for experimentation.

A non-trivial exercise in language-driven design reveals that global design factorization techniques, such as hierarchical decomposition and data abstraction, are inherited from the functional description style. Next, a specialized transformation system is defined to address a typical local refinement problem: serialization of inputs.