Abstract specification of synchronous data types for VLSI and proving the correctness of systolic network implementations
- 1 June 1988
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. 37 (6) , 710-720
- https://doi.org/10.1109/12.2209
Abstract
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 for implementation in VLSI. Associated systematic proof techniques are presented, and the correctness of several novel systolic network implementations of familiar data types is established. The methodology appears to be naturally suited to systolic network implementations with their associated rippling of control flow and data flow. The important distinction between systolic control-flow networks and systolic data-flow networks is presented.Keywords
This publication has 17 references indexed in Scilit:
- A Generalized Dictionary Machine for VLSIIEEE Transactions on Computers, 1985
- A Mathematical Model for the Verification of Systolic NetworksSIAM Journal on Computing, 1984
- The ``Hoare Logic'' of CSP, and All ThatACM Transactions on Programming Languages and Systems, 1984
- A Dictionary Machine (for VLSI)IEEE Transactions on Computers, 1982
- A Systolic (VLSI) Array for Processing Simple Relational QueriesPublished by Springer Nature ,1981
- A Wavefront Notation Tool for VLSI Array DesignPublished by Springer Nature ,1981
- Systolic (VLSI) arrays for relational database operationsPublished by Association for Computing Machinery (ACM) ,1980
- The Design of Special-Purpose VLSI ChipsComputer, 1980
- Notes on Type Abstraction (Version 2)IEEE Transactions on Software Engineering, 1980
- Abstract data types and software validationCommunications of the ACM, 1978