Structure-Based Deadlock Checking of Asynchronous Circuits

Abstract It is important to verify the absence of deadlocks in asynchronous circuits. Much previous work relies on a reachability analysis of the circuits ’ states, with the use of binary decision diagrams (BDDs) or Petri nets to model the behaviors of circuits. This paper presents an alternative approach focusing on the structural properties of well-formed asynchronous circuits that will never suffer deadlocks. A class of data-driven asynchronous pipelines is targeted in this paper, which can be viewed as a network of basic components connected by handshake channels. The sufficient and necessary conditions for a component network consisting of Steer, Merge, Fork and Join are given. The slack elasticity of the channels is analyzed in order to introduce pipelining. As an application, a deadlock checking method is implemented in a syntax-directed asynchronous design tool — Teak. The proposed method shows a great runtime advantage when compared against previous Petri net based verification tools