ON THE CONSTRUCTION OF A PROLOG‐BASED VERIFIER FOR SYSTOLIC ARRAY DESIGNS
作者:
Timothy Shih,
Nam Ling,1,
Ruth Davis, Fuyau Lin,
期刊:
Computational Intelligence
(WILEY Available online 1995)
卷期:
Volume 11,
issue 1
页码: 172-221
ISSN:0824-7935
年代: 1995
DOI:10.1111/j.1467-8640.1995.tb00027.x
出版商: Blackwell Publishing Ltd
关键词: formal specification;theorem proving;systolic array;Prolog
数据来源: WILEY
摘要:
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
点击下载:
PDF
(2093KB)
返 回