ON THE CONSTRUCTION OF A PROLOG-BASED VERIFIER FOR SYSTOLIC ARRAY DESIGNS

In this paper, we present VSTA, our Prolog-based verifier, for formal specification and verification of systolic architectures. VSTA allows users to design systolic array architectures in the STA specification language (STA was developed earlier by Ling for formal description and reasoning of systolic designs) and semi-automatically verifies these designs. The implementation of VSTA is based on a standard Prolog syst em. Its interface uses Motif system calls based on the X11 and UNIX en vironments. VSTA provides facilities to assist the user in the design of systolic array specifications. The system allows a formal proof to be derived interactively with suggestions from the user. The proof tec hniques used are mathematical induction and rewriting. The induction t echnique is adopted to exploit the regularity and locality nature of s ystolic array architectures. A number of verification tactics are deve loped and their operational rules are used in the verifier. Using the powerful symbolic computation ability of Prolog, particularly pattern matching, automatic backtracking, and depth-frst searching, the verifi er performs efficiently in the construction of proofs. We also describ e the strategies we used in proving a matrix multiplication systolic a rray and an LU decomposition systolic array.