Abstract
A mathematical model for systolic networks is generalized and applied to a class of VLSI cellular networks which is defined to include both systolic and self-timed networks. The general model is kept simple by assuming that a computation does not deadlock, that is by separating the verification of liveness from the the verification of the results. The main contribution of this paper concerns the study of deadlock in self-timed computational networks. More specifically, an algebra of events is developed and used to prove that the liveness of any self-timed network is determined uniquely by its initial state. Moreover, a method is presented for the verification of liveness in networks preset to given initial states.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
S. Brookes, C. Hoare and A. Roscoe,A theory of communicating sequential processes, J. of ACM, vol. 31, 3, 1984.
P. Caspi and N. Halbwachs,Algebra of events: A model for parallel and real time systems. Proc. of the 1982 International Conf. on Parallel Preocessing, pp. 150–159.
K. Chandy and J. Misra,Deadlock absence proofs for networks of communicating processes, Information Processing Letters, vol. 9, 4, pp. 185–189, 1979.
M. Chen,Space-time algorithms: semantics and methodology, Ph.D. Thesis, California Institute of Technology, (1983).
M. Chen and C. Mead,Formal Specification of Concurrent Systems, USC workshop on VLSI and Modern Signal Processing, (Nov. 1982).
N. Francez,Fairness, Springer Verlag, 1986.
G. Kahn,The semantics of a simple language for parallel programming, IFIP 74, pp. 471–475.
H. T. Kung,Why systolic architecture, Computer, vol. 15, pp. 37–46, 1982.
S. Y. Kung, K. Arun, R. Gal-Ezer and B. Rao,Wavefront array processor: language, architecture and applications, IEEE Trans. on Computers, vol. 31, 11, pp. 1054–1066, 1982.
L. Lamport,Time, clocks and ordering of events in a distributed system, CACM, vol. 21, 7, pp. 558–565, 1978.
M. McFarland and C. Parker,An abstract model of behavior for hardware descriptions, IEEE Trans. on Computers, vol. 32, 7, pp. 621–637, 1983.
R. Melhem,The application of a sequence notation to the design of systolic computations, Technical Report ICMA-85-87, The University of Pittsburgh.
R. G. Melhem and W. C. Rheinboldt,A mathematical model for the verification of systolic networks, SIAM J. on Computing, vol. 13, no. 3, pp. 541–565, Aug. 1984.
R. G. Melhem,Formal analysis of a systolic system for finite element stiffness matrices, Journal of Computer and System Sciences, vol. 31-1, pp. 1–27, 1985.
R. G. Melhem,A language for the simulation of systolic architectures, Proc. of the 12th International Symposium on Computer Architecture - Boston - Massachusetts, June 1985.
B. Mishra and E. Clarke,Automatic and hierarchical verification of asynchronous circuits using temporal logic, Tech. Report CMU-CS-83, Dept. of Computer Science, Carnegie-Mellon University, 1983.
C. Seitz,System timing, inIntroduction to VLSI Systems, ed. C. Mead and L. Conway, pp. 218–262, 1980.
W. Wadge,An extensional treatment of dataflow deadlock, Theoretical Computer Science, vol. 13, pp. 3–15, 1981.
U. Weiser and A. Davis,A wavefront notation tool for VLSI array design, inVLSI Systems and Computations, ed. H. T. Kung, B. Sproull and G. Steele, pp. 226–234, 1981.
Author information
Authors and Affiliations
Additional information
This work was supported in part under ONR contract N00014-80-C-0455.
Rights and permissions
About this article
Cite this article
Melhem, R. Verification of a class of self-timed computational networks. BIT 27, 480–500 (1987). https://doi.org/10.1007/BF01937273
Received:
Revised:
Issue Date:
DOI: https://doi.org/10.1007/BF01937273