• Publication
  • 1988
  • Issue No. 6 - June
  • Abstract - Abstract pecification of Synchronous Data Types for VLSI and Proving the Correctness of Systolic Network Implementations
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Abstract pecification of Synchronous Data Types for VLSI and Proving the Correctness of Systolic Network Implementations
June 1988 (vol. 37 no. 6)
pp. 710-720
A combined methodology is presented for specifying abstract synchronous data types and proving the correctness of systolic network implementations. It is shown that an extension of the Parnas trace method of specifying software modules containing distinct access programs yields a natural method of specifying abstract synchronous data types that possess distinct access operators and are intended

[1] W. Bartussek and D. L. Parnas, "Using assertions about traces to write abstract specifications for software modules," inProc. 2nd Conf. Euro. Cooperation Inform.Berlin, Germany: Springer-Verlag, 1978.
[2] H. T. Kung, "Why systolic architectures?,"IEEE Computer, vol. 15, pp. 37-46, Jan. 1982.
[3] H. F. Li and R. Jayakumar, "A characterization of VLSI systolic structures and algorithms," inProc. 1985 Canadian Conf. VLSI, Toronto, Ont., Canada, Nov. 1985.
[4] H. T. Kung and C. E. Leiserson, "Systolic arrays (for VLSI)," inProc. Symp. Sparse Matrix Comput. Appl., Nov. 1978, pp. 256- 282.
[5] W. M. Gentleman and H. T. Kung, "Matrix triangularization by systolic arrays," inProc. SPIE, Real-Time Signal Processing IV, vol. 298, 1981.
[6] A. Bojanczyk, R. P. Brent, and H. T. Kung, "Numerically stable solution of dense systems of linear equations using mesh connected processors," CMU Tech. Rep., May 1981.
[7] H. T. Kung, L. M. Ruane, and D. W. L. Yen, "A two-level pipelined systolic array for convolution," inVLSI Systems and Computations, H. T. Kung, R. F. Sproull, and G. L. Steele, Jr., Eds. Rockville, MD: Computer Science Press, Oct. 1981, pp. 255-264.
[8] J. Blackmer, P. Kuekes, and G. Frank, "A 200 MOPS systolic processor," inProc. SPIE, Real-Time Signal Processing IV, vol. 298, 1981.
[9] H. T. Kung, "Let's design algorithms for VLSI systems," inProc. Conf. VLSI: Architecture, Design, Fabrication, Caltech, Pasadena, CA, Jan. 1979, pp. 65-90.
[10] H. J. Foster and H. T. Kung, "The design of special purpose VLSI chips,"IEEE Computer, pp. 26-40, Jan. 1980.
[11] L. J. Guibas, H. T. Kung, and C. D. Thompson, "Direct VLSI implementation of combinatorial algorithms," inProc. Conf. VLSI: Architecture, Design, Fabrication, Caltech, Pasadena, CA, Jan. 1979.
[12] P. L. Lehman, "A systolic (VLSI) array for processing simple relational queries," inVLSI Systems and Computations, H. T. Kung, R. F. Sproull, and G. L. Steele, Jr., Eds. Rockville, MD: Computer Science Press, Oct. 1981, pp. 285-295.
[13] H. T. Kung and P. L. Lehman, "Systolic (VLSI) arrays for relational database operations," inProc. ACM Sigmod 1980 Int. Conf. Management Data, May 1980, pp. 105-116.
[14] T. A. Ottmann, A. L. Rosenberg, and L. J. Stockmeyer, "A dictionary machine (for VLSI),"IEEE Trans. Comput., vol. C-31, pp. 892- 897, Sept. 1982.
[15] M. Atallah and S. R. Kosaraju, "A generalized dictionary machine for VLSI,"IEEE Trans. Comput., vol. C-34, pp. 151-155, Feb. 1985.
[16] L. J. Guibas and F. M. Liang, "Systolic stacks, queues and counters," inProc. Conf. Adv. Res. VLSI, MIT, Cambridge, MA, Jan. 1982.
[17] D. K. Probst and H. F. Li, "Using assertions about traces for abstract specification and proof of correctness of VLSI dictionary machines," submitted for publication.
[18] J. V. Guttag, E. Horowitz, and D. R. Musser, "Abstract data types and software validation,"Commun. ACM, vol. 21, pp. 1048-1064, Dec. 1978.
[19] J. V. Guttag, "Notes on type abstraction,"IEEE Trans. Software Eng., vol. SE-6, pp. 13-23, Jan. 1980.
[20] C. E. Leiserson and J. B. Saxe, "Optimizing synchronous systems,"J. VLSI Comput. Syst., vol. 1, pp. 41-63, Jan. 1983.
[21] J. McLean, "A formal foundation for the abstract specification of software,"J. ACM, vol. 31, no. 3, pp. 600-627, July 1984.
[22] D. Hoffman, "The trace specification of communications protocols,"IEEE Trans. Comput., vol. C-34, pp. 1102-1114, Dec. 1985.
[23] D. K. Probst, "A systolic working set chip with real-time response and single-cycle reference pipelining," inProc. 1985 Canadian Conf. VLSI, Toronto, Ont., Canada, Nov. 1985.
[24] C. E. Leiserson, "Systolic priority queues," inProc. Conf. VLSI: Architecture, Design, Fabrication, Caltech, Pasadena, CA, 1979.
[25] J. Misra and K. M. Chandy, "Proofs of networks of processes,"IEEE Trans. Software Eng., vol. SE-7, pp. 417-426, 1981.
[26] J. Misra, K. M. Chandy, and T. Smith, "Proving safety and liveness of communicating processes with examples," inProc. 1st Symp. Principles Distributed Comput., Ottawa, Ont., Canada, Aug. 1982.
[27] L. Lamport and F. B. Schneider, "The 'Hoare logic' of CSP and all that,"ACM Trans. Programming Languages Syst., vol. 6, pp. 281- 296, Apr. 1984.
[28] G. Melhem and W. C. Rheinboldt, "A mathematical model for the verification of systolic networks,"SIAM J. Comput., vol. 13, pp. 541-565, Aug. 1984.
[29] S. Y. Kung, R. J. Gal-Eser, and K. S. Arun, "'Wavefront array processor: Architecture, language and applications," inProc. Conf. Adv. Res., VLSI, MIT, Cambridge, MA, Jan. 1982.
[30] U. Weiser and A. Davis, "A wavefront notation tool for VLSI array design," inVLSI Systems and Computations, H. T. Kung, B. Sproull, and G. L. Steele, Jr., Eds. Rockville, MD: Computer Science Press, Oct. 1981.

Index Terms:
correctness proving; abstract specification; synchronous data types; VLSI; systolic network implementations; Parnas trace method; software modules; control flow; data flow; cellular arrays; data structures; VLSI.
Citation:
D.K. Probst, H.F. Li, "Abstract pecification of Synchronous Data Types for VLSI and Proving the Correctness of Systolic Network Implementations," IEEE Transactions on Computers, vol. 37, no. 6, pp. 710-720, June 1988, doi:10.1109/12.2209
Usage of this product signifies your acceptance of the Terms of Use.