An automated design specification and verification tool for systolic architectures

Presents a Prolog-based verifier, VSTA, for formal specification and verification of systolic architectures. VSTA allows users to design systolic array architectures in the systolic temporal arithmetic (STA) specification language, and the designs can be semi-automatically verified by the system. In addition, the authors describe how a systolic array for LU decomposition can be specified and verified with respect to its algorithm. The proof techniques used are mathematical induction and rewriting. The induction technique is adopted to exploit the regularity and locality nature of systolic array architectures. A number of verification tactics are developed in the verifier and their operational rules are used in the verifier. Using the powerful symbolic computation ability of Prolog, particularly pattern matching, automatic backtracking, and the depth-first searching rules, the verifier performs efficiently in the construction of proofs