Verification of Systolic Architecture Designs

[[abstract]]We present a Prolog-based verifier, VSTA, for formal specification and verification of systolic architectures. This specific CAD tool is developed to produce sound and efficient verification process and provide short-cuts to justify systolic array designs. Our tool allows users to represent systolic array architectures in Systolic Temporal Arithmetic specification language and to justify the design semi-automatically using the system. STA is developed earlier by Ling [18] for formal description and reasoning of systolic array designs. We briefly review the STA formalism and discuss the realization of STA verifier which is an interpreter with induction and rewriting mechanisms built in. The induction technique is adopted to exploit the regularity and locality nature of systolic array architectures. Prolog is adopted for mechanical verification due to its power and its closeness in representing STA notatio