Structure-Based Deadlock Checking of Asynchronous Circuits

作     者：任洪广 王志英 Doug Edwards 

作者机构：School of ComputerNational University of Defense Technology CCF ACM IEEE School of Computer ScienceUniversity of Manchester 

出 版 物：《Journal of Computer Science & Technology》 (计算机科学技术学报（英文版）)

年 卷 期：2011年第26卷第6期

页      面：1031-1040页

核心收录：

学科分类：080903[工学-微电子学与固体电子学] 0809[工学-电子科学与技术（可授工学、理学学位）] 08[工学] 

基　　金：supported by the National Natural Science Foundation of China under Grant Nos.60873015 61070037 and 61103016 

主　　题：asynchronous pipeline data-driven deadlock verification 

摘      要：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 Team The proposed method shows a great runtime advantage when compared against previous Petri net based verification tools.