Automatic formal verification of systolic array designs

The authors have previously (1990) developed a new formalism, called systolic temporal arithmetic (STA), for formal specification and verification of systolic arrays at the array level. The formalism exploits systolic array attributes to produce elegant specification and effective formal design verification and is suitable to be combined 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 the authors developed recently to verify the correctness of different systolic architectures. The 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 the authors developed to automate the proofs. Prolog is adapted 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