Automatic verification of a class of systolic circuits

Systolic circuits have attracted considerable attention as a means of implementing parallel algorithms in areas such as linear algebra, signal processing, pattern matching, etc. A systolic circuit is composed of a number of computation cells which are connected in a regular pattern. Each cell can perform computations, store data and communicate with other cells in the circuit. We define a language to describe implementations and specifications of a class of systolic circuits whose cells compute over a commutative ring, and present a decision method to check whether or not a circuit implementation fulfils a specification. The main advantage of our approach, compared with earlier work in the field, is that the verification is performed automatically, without user interaction. We give an example of how the method may be applied to verify a convolution circuit.