Premium
ON THE CONSTRUCTION OF A PROLOG‐BASED VERIFIER FOR SYSTOLIC ARRAY DESIGNS
Author(s) -
Shih Timothy,
Ling, Nam,
Lin Ruth Davis, Fuyau
Publication year - 1995
Publication title -
computational intelligence
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.353
H-Index - 52
eISSN - 1467-8640
pISSN - 0824-7935
DOI - 10.1111/j.1467-8640.1995.tb00027.x
Subject(s) - computer science , prolog , systolic array , backtracking , programming language , mathematical proof , matrix multiplication , theoretical computer science , algorithm , embedded system , mathematics , physics , geometry , quantum mechanics , very large scale integration , quantum
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 system. Its interface uses Motif system calls based on the X11 and UNIX environments. 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 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 and their operational rules are used in the verifier. Using the powerful symbolic computation ability of Prolog, particularly pattern matching, automatic backtracking, and depth‐first searching, the verifier performs efficiently in the construction of proofs. We also describe the strategies we used in proving a matrix multiplication systolic array and an LU decomposition systolic array.