Automatic Verification of a Class of Systolic Circuits

Systolic circuits have drawn 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 present a method for automatic verification of a class of these circuits. We define a language to describe implementations and specifications of our class of circuits, and present a method to automatically check whether a circuit implementation fulfills its specification. The main advantage of our approach, as compared to earlier work in the field, is that the verification is performed fully automatically. We give an example of how the method may be applied to verify a convolution circuit. 1 Introduction The advent of VLSI has increased the interest in designing highly-parallel computing architectures in order t..