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

Timothy Shih, Nam Ling,, Ruth Davis, Fuyau Lin

Research output: Contribution to journalArticlepeer-review

Abstract

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.

Original languageEnglish
Pages (from-to)172-221
Number of pages50
JournalComputational Intelligence
Volume11
Issue number1
DOIs
StatePublished - Feb 1995

Keywords

  • formal specification
  • Prolog
  • systolic array
  • theorem proving

Fingerprint

Dive into the research topics of 'ON THE CONSTRUCTION OF A PROLOG‐BASED VERIFIER FOR SYSTOLIC ARRAY DESIGNS'. Together they form a unique fingerprint.

Cite this