Verification of a Class of Deadlock-Free, Self-Timed, Computational Arrays.
Abstract
A special class of self-timed networks is defined and two steps are suggested for the verification of any computation performed on networks in this class. First, a proof that the network is deadlock-free, and second, a verification of the results of the computation. In relation to the first step, 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. In order to verify the results of deadlock-free self-timed computations, general VLSI cellular networks are defined to include both systolic and self-timed computational arrays. A model for the verification of computations on these networks is then obtained by the generalization of a previous model that was suggested for systolic computations. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Aug 01, 1984
- Accession Number
- ADA146272
Entities
People
- R. G. Melhem
Organizations
- University of Pittsburgh