Advertisement

Verification of systolic architecture designs

  • Fuyau Lin
  • Timothy Shih
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 605)

Abstract

We present a Prolog-based verifier, VSTA, for formal specification and verification of systolic architectures. This specific CAD tool is developed to produce sound and efficient verification process and provide short-cuts to justify systolic array designs. We describe how a systolic array for 2-D matrix multiplication and LU decomposition can be specified and verified with respect to its algorithm.

Keywords

Inference Rule Systolic Array Formal Verification Verification Tool Main Processor 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    H. G. Barrow, “VERIFY: A Program for Proving Correctness of Digital Hardware Design,” Art. Intell., Vol. 24, pp. 437–491, 1984.CrossRefGoogle Scholar
  2. [2]
    P. Camurati and P. Prinetto, “Formal Verification of Hardware Correctness: Introduction and Survey of Current Research,” IEEE Computer Magazine, July 1988.Google Scholar
  3. [3]
    M. C. Chen and C. A. Mead, “Concurrent Algorithms as Space-Time Recursion Equations,” USC Workshop on VLSI and Modern Signal Processing, 1982.Google Scholar
  4. [4]
    M. C. Chen, Space-Time Algorithms: Semantics and Methodology, Ph. D. Thesis, California Institute of Technology, Pasedena, CA, May 1983.Google Scholar
  5. [5]
    H. Eveking, “The Application of CHDL's to the Abstract Specification of Hardware,” CHDL'85: IFIP 7th Int. Conf. on Comp. Hardware Description Lang. and their Applications, Aug. 1985.Google Scholar
  6. [6]
    M. J. Gordon, A. J. Milner, and C. P. Wadsworth, Edinburgh LCF, Lecture Notes in Computer Science 78, 1979.Google Scholar
  7. [7]
    M. Hennessy, “Proving Systolic System Correct,” ACM Trans. on Prog. Lang. and Syst., July 1986.Google Scholar
  8. [8]
    W. A. Hunt, “The Mechanical Verification of a ‘Microprocessor Design,” in From HDL Descriptions to Guaranteed Correct Designs, D. Borrione, ed., Amsterdam, The Netherlands: North Holland, pp. 89–129, 1987.Google Scholar
  9. [9]
    J. M. Jover, and T. Kailath, “Design Framework for Systolic-Type Arrays,” Proc. of the 1984 IEEE Int. Conf. on Acoustics, Speech, and Signal Processing, San Diego, Mar. 1984.Google Scholar
  10. [10]
    H. T. Rung and C. E. Leiserson, “Systolic Arrays (for VLSI),” Sparse Matrix Symp., SIAM, 1978.Google Scholar
  11. [11]
    H. T. Kung, “Why Systolic Architectures¿ 'IEEE Computer Magazine, Jan. 1982.Google Scholar
  12. [12]
    H. T. Kung and W. T. Lin, “An Algebra for VLSI Algorithm Design,” Proc. of the Conf. on Elliptic Problem Solvers, Monterey, CA, Jan. 1983.Google Scholar
  13. [13]
    S. Y. Kung, “VLSI Array Processors,” IEEE ASSP Mag., July 1985.Google Scholar
  14. [14]
    S. Y. Kung, VLSI Array Processors, Prentice-Hall, Englewood Cliffs, New Jersey, 1988.Google Scholar
  15. [15]
    C. J. Kuo, B. C. Levy, and B. R. Musicus, “The Specification and Verification of Systolic Wave Algorithms,” 1984 IEEE Workshop on VLSI Signal Processing I, IEEE Press, 1984.Google Scholar
  16. [16]
    H. Lev-Ari, “Modular Computing Networks: A New Methodology for Analysis and Design of Parallel Algorithms / Architectures,” Integrated Systems Inc., Report No. 29, Palo Alto, CA, Dec. 1983.Google Scholar
  17. [17]
    F. Lin, T. Shih, and N. Ling “Axiomatic Approach for Systolic Array Design,” Proceeding of the Logic Programming Conference 91, Tokyo, Japan, July 8–11, 1991.Google Scholar
  18. [18]
    F. Lin and T. Shih, “Using Prolog as a Verification Tool for Systolic Designs,” forthcoming in the Proceeding of the ICPAP'92, London, U.K., April 1–3, 1992.Google Scholar
  19. [19]
    Nam Ling, Systolic Temporal Arithmetic: A New Formalism for for Specification, Verification, and Synthesis of Systolic Arrays, Ph. D. Dissertation, Univ. of Southwestern Louisiana, Summer 1989.Google Scholar
  20. [20]
    Nam Ling and M. A. Bayoumi, “Systematic Algorithm Mapping for Multidimensional Systolic Arrays,” Journal of Parallel and Distributed Computing, Vol. 7, No. 2, Academic Press, pp. 368–382, October 1989.Google Scholar
  21. [21]
    Nam Ling and M. A. Bayoumi, “Systolic Temporal Arithmetic: A New Formalism for Specification and Verification of Systolic Arrays,” IEEE Trans. on Computer-Aided Design, Vol. 9, No. 8, pp. 804–820, August 1990.CrossRefGoogle Scholar
  22. [22]
    R. G. Melhem and W. C. Rheinboldt, “A Mathematical Model for the Verification of Systolic Networks,” SIAM J. of Comput., Vol. 13, No. 3, Aug. 1984.Google Scholar
  23. [23]
    R. Milner, “A Calculus of Communicating Systems,” Lecture Notes in Computer Science, 92, Springer-Verlag, New York, 1980.Google Scholar
  24. [24]
    B. Moszkowski, “A Temporal Logic for Multilevel Reasoning about Hardware,” IEEE Computer Mag., Feb. 1985.Google Scholar
  25. [25]
    M. Ossefort, “Correctness Proofs of Communicating Processes-Three Illustrative Examples from the Literature,” TR-LCS-8201, Dept. of Computer Science, Univ. of Texas, Austin, TX, Jan. 1982.Google Scholar
  26. [26]
    D. K. Probst and H. F. Li, “Abstract Specification of Synchronous Data Types for VLSI and Proving the Correctness of Systolic Network Implementations,” IEEE Trans. on Computers, Vol. 37, No. 6, June 1988.Google Scholar
  27. [27]
    S. Purushothaman and P. A. Subrahmanyan, “Mechanical Certification of Systolic Algorithms,” Journal of Automated Reasoning, Kluwer Academic Pub., Mar. 1989.Google Scholar
  28. [28]
    S. V. Rajopadhye and P. Panagaden, “Verification of Systolic Arrays: A Stream Functional Approach,” UUCS-85-001, University of Utah, Salt Lake City, UT, Mar. 1985.Google Scholar
  29. [29]
    R. E. Shostak, “Verification of VLSI Designs,” in Proc. of Third Caltech Conf. on VLSI, pp. 185–206, 1983.Google Scholar
  30. [30]
    E. Tiden, “Verification of Systolic Arrays-A Case Study,” Technical Report TRITA-NA-8403, Dept. of Numerical Analysis and Computer Science, The Royal Institute of Technology (Sweden), 1984.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Fuyau Lin
    • 1
  • Timothy Shih
    • 1
  1. 1.Dept. of Computer EngineeringSanta Clara UniversitySanta Clara

Personalised recommendations