Automatic verification of a class of systolic circuits
Abstract
Systolic circuits have attracted considerable attention as a means of implementing parallel algorithms in areas such as linear algebra, signal processing, pattern matching, etc. A systolic circuit is composed of a number of computation cells which are connected in a regular pattern. Each cell can perform computations, store data and communicate with other cells in the circuit. We define a language to describe implementations and specifications of a class of systolic circuits whose cells compute over a commutative ring, and present a decision method to check whether or not a circuit implementation fulfils a specification. The main advantage of our approach, compared with earlier work in the field, is that the verification is performed automatically, without user interaction. We give an example of how the method may be applied to verify a convolution circuit.
References
References
[1]
Abdulla, P.: Decision Problems in Systolic Circuit Verification. Ph.D. Thesis, Department of Computer Systems, Uppsala University, 1990.
[2]
Aboulnasr T. and Steenaart W. Real-Time Systolic Processor for 2-D Spatial Filtering IEEE Transactions on Circuits and Systems 1988 35 4 451-455
[3]
Borosh I. and Treybig L. B. Bounds on positive integral solutions of linear diophantine equations Proc. American Mathematical Society 1976 55 299-304
[4]
Boyer, R. S. and Moore, J. S.:A Computational Logic. Academic Press, 1979.
[5]
Chen M. Space-Time Algorithms: Semantics and Methodology PhD Thesis 1983 Pasadena, California California Institute of Technology
[6]
Clarke, E. M., Grumberg, O. and Browne, M. C.: Reasoning about Networks with Many Identical Finite State Processes. InACM PoDC, 1986.
[7]
Davis M. Hilbert's Tenth Problem is Undecidable Amer. Math. Monthly 1973 80 233-269
[8]
Derrick, J., Lajos, G. and Tucker, J. V.: Specification and Verification of Synchronous Concurrent Algorithms using the Nuprl Proof Development System. Technical Report, Centre for Theoretical Computer Science, The University of Leeds, 1989.
[9]
Eker, S. M. and Tucker, J. V.: Specification, Derivation and Verification of Concurrent Line Drawing Algorithms and Architectures: a Case Study of Pixel Planes Architecture. In:Parallel Processing for Vision and Display, P. M. Dew, R. A. Earnshow and T. R. Heywood (eds), Addision Wesley, 1989.
[10]
Gordon M. Milne G. J. and Subrahmanyam P. A. Why Higher Order Logic is a Good Formalism for Specifying and Verifying Hardware Formal Aspects of VLSI Design, Proceedings of the 1985 Edinburgh Conference on VLSI 1986 Amsterdam North-Holland
[11]
Gordon M. Birtwistle G. M. and Subrahmanyam P. A. HOL: a Proof Generating System for Higher Order Logic Verification and Synthesis 1987 Amsterdam North-Holland
[12]
Hennessy M. Proving Systolic Systems Correct ACM TOPLAS 1986 8 3 344-387
[13]
Hobley, K. M., Thompson, B. C. and Tucker, J. V.: Specifiation and Verification of Synchronous Concurrent Algorithms: a Case Study of a Convolution Algorithm. InProc. of the IFIP International Working Conference on The Fusion of Hardware Design and Verification, 342–369, 1988.
[14]
Kung H. T. Why Systolic Architectures? IEEE Computer 1982 15 1 37-46
[15]
Kwan H. K. Systolic Realization of Linear Phase FIR Digital Filters IEEE Transactions on Circuits and Systems 1987 34 12 1604-1605
[16]
Martin, A. R. and Tucker, J. V.: The Concurrent Assignment Representation of Synchronous Systems. In:PARLE, LNCS 259, Springer-Verlag, 1987.
[17]
Mead, C. and Conway, L.:Introduction to VLSI Systems, pp. 263–332. Addison-Wesley, 1980.
[18]
Melhem R. G. and Rheinbold W. C. A Mathematical Model for the Verification of Systolic Networks SIAM J. Comput. 1984 13 3 541-565
[19]
O'leary D. P. Systolic Arrays for Matrix Transpose and Other Recordings IEEE Transactions on Computers 1987 36 1 117-122
[20]
Provence J. D. and Gupta S. C. Systolic Arrays for Viterbi Processing in Communication Systems with a Time-Dipersive Channel IEEE Transactions on Communications 1988 36 10 1148-1156
[21]
Purushothaman S. and Subrahmanyam P. A. Reasoning about Systolic Algorithms Journal of Parallel and Distributed Computing 1988 5 669-699
[22]
Purushothaman S. and Subrahmanyam P. A. Mechanical Certification of Systolic Algorithms Journal of Automated Reasoning 1989 5 1 67-95
[23]
Thompson, B. C. and Tucker, J. V.: Synchronous Concurrent Algorithms. Technical Report, Centre for Theoretical Computer Science, The University of Leeds, 1988.
[24]
Ullman, J. D.:Computational Aspects of VLSI, pp. 175–208, Computer Science Press, 1984.
Index Terms
- Automatic verification of a class of systolic circuits
Index terms have been assigned to the content through auto-classification.
Recommendations
Automatic Verification of Fault-Tolerant Register Emulations
The design and verification of fault-tolerant distributed algorithms is a complicated task. Usually, the proof of correctness is done manually, and thus depends on the skill of the prover. Using automated verification methods, such as model checking, ...
Monotonic Abstraction in Parameterized Verification
We present a tutorial on verification of safety properties for parameterized systems. Such a system consists of an arbitrary number of processes which are organized in a linear array. The aim is to prove correctness of the system regardless of the ...
Automatic verification of timed concurrent constraint programs
The language Timed Concurrent Constraint (tccp) is the extension over time of the Concurrent Constraint Programming (cc) paradigm that allows us to specify concurrent systems where timing is critical, for example reactive systems. Systems which may have ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
© BCS 1992.
Publisher
Springer-Verlag
Berlin, Heidelberg
Publication History
Published: 01 March 1992
Accepted: 15 December 1990
Received: 01 December 1989
Published in FAC Volume 4, Issue 2
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 40Total Downloads
- Downloads (Last 12 months)27
- Downloads (Last 6 weeks)3
Reflects downloads up to 20 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in