ABSTRACT A model of computation for the design of synchronous and systolic algorithms is presented. The model is hierarchically structured, and so can express the development of an algorithm through many levels of abstraction. The syntax of the model is based on the directed graph, and the synchronous semantics are state-transitional. A semantic representation of ripple-carries is included. The cells available in the data structure of a computation graph are defined by a graph signature. In order to develop two-level pipelining in the model, we need to express serial functions as primitives, and so a data structure may include history-sensitive functions.

A typical step in a hierarchical design is the substitution of a single data element by a string of data elements so as to refine an algorithm to a lower level of abstraction. Such a refinement is formalised through the definition of parallel and serial homomorphisms of data structures.

Central to recent work on synchronous algorithms has been the work of H. T. Kung and others on systolic design. The Retiming Lemma of Leiserson & Saxe [1981] has become an important optimisation tool in the automation of systolic design (for example, in the elimination of ripple-carries). This lemma and the Cut Theorem (Kung & Lam [1984]) are proved in the formal model.

The use of these tools is demonstrated in a design for the matrix multiplication algorithm presented in H. T. Kung [1984].