Specification and Verification of Systolic Arrays

by Ling, Nam

• ISBN13: 9789810238674
• ISBN10: 9810238673
• Format: Hardcover
• Copyright: 1999-06-01
• Publisher: WORLD SCIENTIFIC PUB CO INC

Summary

This book presents a formal method for specifying and verifying the correctness of systolic array designs. Such architectures are commonly found in the form of accelerators for digital signal, image, and video processing. These arrays can be quite complicated in topology and data flow. In the book, a formalism called STA is defined for these kinds of dynamic environments, with a survey of related techniques. A framework for specification and verification is established. Formal verification techniques to check the correctness of the systolic networks with respect to the algorithmic level specifications are explained. The book also presents a Prolog-based formal design verifier (named VSTA), developed to automate the verification process, as using a general purpose theorem prover is usually extremely time-consuming. Several application examples are included in the book to illustrate how formal techniques and the verifier can be used to automate proofs.

Table of Contents

Preface	xi
Acknowledgements	xiii
Introduction	1	(8)
Introduction	1	(1)
Definition of Systolic Arrays	1	(1)
Systolic Array Abstraction Levels	2	(1)
The Design of Systolic Arrays	3	(2)
The Objective of the Book	5	(2)
An Overview of the Book	7	(2)
Specification and Verification of Systolic Arrays: Definitions and Related Work	9	(8)
Introduction	9	(1)
A Review of Related Work	10	(2)
Related Work in the Specification and Verification of Digital Circuits and Modules	10	(1)
Related Work in the Specification and Verification of Systolic Arrays	11	(1)
Motivation and Challenge	12	(1)
Research Direction	13	(1)
Abstraction Mechanisms	13	(4)
Systolic Temporal Arithmetic: A Formalism	17	(18)
Introduction	17	(1)
The Model of Time	17	(3)
Syntax of Sta	20	(6)
Semantics of Sta	26	(2)
Satisfiability and Validity	28	(1)
Sta Axioms, Rules and Theorems	28	(3)
Axioms	28	(1)
Rules	29	(1)
Theorems	30	(1)
Useful Constructs	31	(4)
Specification and Verification Framework	35	(8)
Systolic Array Specification	35	(2)
Systolic Array Verification	37	(1)
Verification by Output Derivation and Comparison	37	(1)
Verification by Induction	38	(2)
Verification by Solving Sta Difference Equations	40	(3)
Specification and Verification of Systolic Arrays: Application Examples	43	(18)
A 1-D Array For Matrix-Vector Multiplication	43	(6)
Array Specification using STA	43	(3)
Array Verification by STA	46	(1)
Output Derivation and Comparison	46	(1)
Mathematical Induction	47	(2)
A 2-D Array For Matrix-Matrix Multiplication	49	(5)
Array Specification by STA	51	(1)
Array Verification by STA	52	(2)
A BI-Directional Array For 1-D Convolution	54	(7)
Array Specification by STA	55	(2)
Array Verification by STA	57	(4)
Vsta: A Special Purpose Formal Verifier for Systolic Designs	61	(8)
Introduction	61	(1)
Inductive Design Verification Techniques	62	(1)
Vsta Automation Technique	62	(4)
Vsta Verifier Structure	66	(3)
Verifying The Correctness of a Systolic Array for Lu Decomposition	69	(12)
A Systolic Array for Lu Decomposition	69	(2)
Formal Specification of the Array	71	(3)
Proof of Correctness of the Array	74	(5)
Proofs of the Intermediate Specifications	74	(3)
Proofs of the Output Specifications	77	(2)
Conclusion	79	(2)
Conclusions	81	(2)
APPENDIX A VSTA USER INTERFACE AND SAMPLE OUTPUT	83	(16)
A.1 Vsta User Interface	83	(1)
A.2 Vsta Sample Specification	83	(6)
A.3 Sample Vsta Proof Output	89	(10)
Bibliography	99	(10)
Author Biographies	109	(2)
Index	111