Verification of a class of self-timed computational networks (Q1102099)

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 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.