Automatic formal verification of systolic array designs

We have already developed a new formalism, called Systolic Temporal Arithmetic (STA), for formal specification and verification of systolic arrays at the array level (see [Ling90]). The formalism exploits systolic array attributes to produce elegant specification and effective formal design verification and is suitable to be combated with interval temporal logic for multilevel reasoning for several abstraction levels of systolic architecture. Besides providing a brief review of the STA formalism, the paper concentrates on discussing and expanding several formal techniques that we developed recently to verify the correctness of different systolic architectures. This paper emphasizes two verification strategies: verification by different induction techniques and verification by solving STA difference equations. Verification techniques are developed to produce sound and efficient verification procedures and provide short-cuts to proofs. In addition, the paper also presents a Prolog-based verifier that we developed to automate the proofs. Prolog is adopted for automated verification due to its popularity and its closeness in representing STA predicate-type notations. This allows easy encoding and user control to improve efficiency. The automatic backtracking and pattern matching mechanisms of Prolog serve as a useful tool for implementing the proofs.