Structure-Based Deadlock Checking of Asynchronous Circuits  

作　　者：任洪广 王志英 Doug Edwards 

机构地区：[1]School of Computer,National University of Defense Technology [2]CCF [3]ACM [4]IEEE [5]School of Computer Science,University of Manchester

出　　处：《Journal of Computer Science & Technology》2011年第6期1031-1040,共10页计算机科学技术学报（英文版）

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

摘　　要：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.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.

关 键 词：asynchronous pipeline DATA-DRIVEN DEADLOCK VERIFICATION 

分 类 号：TN402[电子电信—微电子学与固体电子学]