Decidable and Undecidable Problems in Systolic Circuit Verification

We present a decision method for automatic verification of a nontrivial class of systolic circuits. A formal model for systolic circuits, and a formal definition of systolic circuit verification are provided. Using this model, we give a decision method for verification of a class of circuits, in which the cell operations of the circuits are regarded as uninterpreted function symbols. If a circuit is verified in this manner then the circuit is correctly implemented with respect to its specification regardless of the particular interpretation of the cell operations. Finally we show that simple generalizations of the class lead to undecidable verification problems. Examples of circuits which can be verified automatically by our method include circuits for: convolution algorithms, matrix operations (such as matrix multiplication and transposition), string comparisons (such as substring detection, approximate string matching, and palindrome recognition), and implementation of digital filter..