A formal process for systolic array design using recurrences
Jonathan Puddicombe · ERA · 1992
A systolic array is essentially a parallel processor which consists of a grid of locallyconnected sub-processors which receive, process and pump out data synchronously in such a way that the pattern of data-flow to and from each processor is identical to the flow to and from the other processors.Such arrays are repetitive and modular and require little length of communication interconnection, so that they are relatively simple to design and are amenable to efficient VLSI implementation.The systolic architecture has been found suitable for implementing many of the algorithms used in the field of signal-and image-processing.A formal design method is a well-defined process for constructing, given a well-defined function from a certain class, a well-defined object (e.g. a design) which performs that function.When proven correct, such methods are useful for designing equipment which is safety-critical or where a design fault discovered after manufacture would be expensive.This thesis presents a formal design method for producing high-level implementations for certain signal-processing and other algorithms.These high-level implementations can themselves usually be easily implemented as systolic arrays.As a necessary preliminary to the method, a calculus is defined.The basic concept, that of a "computation", is powerful enough to express both abstract algorithms and those whose suboperations have been assigned a place and a time to execute.Computations may be composed or abstracted (by having their variables hidden) or may have their variables renamed.The "simulation" of one computation by another is defined.Using this calculus it is possible to formalise concepts like "dependency" (of data or control)and "system of recurrence equations", which often appear in the literature on systolic array design.The design method is then presented.It consists of five stages: pipelining of data dependencies, scheduling, pipelining of the control variables, allocation of subprocessors to the subcomputations, and the final stage (in which the design is constructed).The main concepts are not new, but here they have been formalised, Terminology Lx GeneralThe hand symbol "to " signifies that what follows is a reference to a proposition and its proof in the appendices.The symbol ""is used to express the composition of two functions. So (v'RENAME)var v(RENAME(var)).The symbol "" signifies that the term or bracketed expression immediately following it is to be read as being a subscript of the one preceding it.The symbol ")" is to be read as "I" followed by ... dQLzI(F) denotes the domain of a function F, and n(F) denotes its range.The domain of a function written "p -e", where e is an expression in p, will often not be stated when it is implied by the context.Let be a function from S to and let S' be asubset of S. Then AS , is the function from S' to T such that vIa' (s') v(s') for all s' in S'.IfFisa function then F[x -+ y] is defined to be the function with the same range as F and domain dom(F)L){x} which satisfies the following equations: F[x -y](x)y F[x -* y](x') = F(x') when x' * x for running on them had been studied previously [Karp67].In [HTKun78], Kung and Leiserson concisely describe a "systolic system" as "a set of processors which rhythmically compute and pass data through the system".The synchronised "pumping" of data through such a system resembles the action of the heart on blood within the circulatory system, hence the term "systolic".Regarding uses of the systolic architecture, Kung and Leiserson themselves showed that systolic arrays could be built which would perform certain important tasks in the field of linear algebra, such as band-matrix multiplication, triangularisation and backsubstitution [HTKun78].In the last decade systolic arrays have been designed which implement many of the algorithms used in radar-, sonar-, image-, signal-and speechprocessing [SYKun88, McW921.Also over the last decade much work has been done to develop mathematically-based languages which can be used to encapsulate hardware design specifications formally and precisely, and to develop mathematical techniques for proving that hardware designs meet those specifications.These languages and techniques are known as "formal methods" or "formal verification".To have a proof of design-correctness is particularly desirable for safety-critical hardware.It is possible to integrate the tasks of design and verification so that each step of the design process is verified as it is taken.This benefits the designer by alerting him to design errors at an early stage, avoiding costly redesign, and it also benefits the verifier since he is not fed with an uncommented, unstructured, design which he must verify without knowing the rationale behind it.Though a validated design process will warn the designer off incorrect designs, it may still be hard for him to find a correct one, due to the plethora of red-herring options.However, if he is willing to forego some freedom, e.g. by restricting himself to a certain architecture, then he can use a specialized formal design method in which some of the steps have been frozen, leaving fewer steps to choose and verify, thereby simplifying his task.(Of course the architecture must be appropriate to the algorithm to be implemented, otherwise the task of finding a correct design may be made more difficult or impossible.)This thesis presents one such specialized method -to be used in the design of systolic arrays. Systolic Arrays 1.2.1 What is a systolic array?Several researchers have given more or less precise definitions of the set of systolic arrays (SAs) [HTKun78, U1184, Rao85, SYKun88].In this thesis the following definition is adopted:A systolic array contains a set of processors.(locality) The interconnections between these processors, and between the then the value-estimate of its pixel is updated; otherwise it is left unchanged.This means that when a processing element is updating its nearest neighbours are resting and vice-versa.The 5096 1 processing element utilization can be increased by "processing element sharing".Similar arrays may be used to implement other algorithms such as the Jacobi method, the Gauss-Siedel algorithm and the Successive Over-relaxation algorithms for solving elliptical partial differential equations (see [SYKun88] p. 598). Formal Design Methods What are formal design methods and their advantages over informal methods?AfQrmal design method is a well-defined process for constructing a well-defined object Advantage 2If the designer is human, a formal design method may clarify his thoughts and lead him to solutions which he would not otherwise have thought of.As was noted earlier, it is a good idea for each choice to be checked for correctness as soon as it is made. Computations and Recurrences 54 Computations and Recurrences 62Compuwiions and Recurrences 72