›› 2011, Vol. 26 ›› Issue (6): 1031-1040.doi: 10.1007/s11390-011-1199-3

Special Issue: Computer Architecture and Systems

• Formal Methods • Previous Articles     Next Articles

Structure-Based Deadlock Checking of Asynchronous Circuits

Hong-Guang Ren1 (任洪广), Zhi-Ying Wang1 (王志英), Senior Member, CCF, Member, ACM, IEEE and Doug Edwards2, Member, ACM, IEEE   

  1. 1. School of Computer, National University of Defense Technology, Changsha 410073, China;
    2. School of Computer Science, University of Manchester, Manchester, M13 9PL, U.K.
  • Received:2011-04-18 Revised:2011-09-12 Online:2011-11-05 Published:2011-11-05
  • About author:Hong-Guang Ren received the B.S. degree in computer science and technology from the National Univer-sity of Defense Technology, China in 2007. He was admitted as a Ph.D. student ahead of graduation time due to his excellent performance in his master study in Feb. 2009. Now, he is a Ph.D. candidate in the School of Computer, National University of Defense Technology. His research interests include computer architecture, asynchronous circuit design, optimization and verification.
    Zhi-Ying Wang received the Ph.D. degree in computer science and technology from the National University of Defense Technology, China, in 1989. He is currently deputy dean and professor of the School of Computer, National Uni-versity of Defense Technology, Hu-nan, China. He has contributed 10 invited chapters to book volumes, published 140 papers in archival journals and refereed con-ference proceedings, and delivered over 30 keynotes. His current research projects include asynchronous micropro-cessor design, nanotechnology circuits and systems based on optoelectronic technology and virtual computer system. Prof. Wang became a member of the IEEE and ACM in 2002 and 2003 respectively. His main research fields include computer architecture, asynchronous circuit, computer se-curity, VLSI design, reliable architecture and multi-core memory system.
    Doug Edwards is a reader in the School of Computer Science, Univer-sity of Manchester, UK. He gained a William Kirtley Entrance Scholar-ship to study physics and electronic engineering at Manchester University in 1965. After graduating, he re-ceived M.Sc. and Ph.D. degrees for studies of Zinc Sulphide —— CSilicon Heterojunctions. He spent 2 years as a lecturer in the Electrical Engineering Department at the University of Manchester before moving to Ferranti work-ing yield improvement of bipolar integrated circuits. He was appointed to the staff of the Computer Science Department in 1975. His research tools includes Balsa and Teak.
  • Supported by:

    This work was 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 —— Teak. The proposed method shows a great runtime advantage when compared against previous Petri net based verification tools.

[1] Edwards D, Bardsley A. Balsa: An asynchronous hardwaresynthesis language. The Computer Journal, 2002, 45(1): 12-18.

[2] van Berkel K. Handshake Circuits: An Asynchronous Archi-tecture for VLSI Programming. 1st edition, Cambridge Uni-versity Press, 1993.

[3] Brunvand E, Sproull R F. Translating concurrent programsinto delay-insensitive circuits. In Proc. the 7th InternationalConference on Computer-Aided Design, Santa Clara, USA,November 5-9, 1989, pp.262-265.

[4] Queille J P, Sifakis J. Specification and verification of con-current systems in CESAR. In Proc. the 5th InternationalSymposium on Programming, Turin, Italy, April 6-8, 1982,pp.337-350.

[5] Clarke E M, Emerson E A. Design and synthesis of synchro-nization skeletons using branching time temporal logic. Logicsof Programs, 1982, 131(3): 52-71.

[6] Burch J R, Clarke E M, Long D E, McMillan K L, Dill DL. Symbolic model checking for sequential circuit verification.IEEE Trans. Computer-Aided Design of Integrated Circuitsand Systems, 1994, 13(4): 401-424.

[7] Bryant R E. Graph-based algorithms for boolean functionmanipulation. IEEE Trans. Computers, 1986, 35(8): 677-691.

[8] McMillan K L. Using unfoldings to avoid the state explosionproblem in the verification of asynchronous circuits. In Proc.the 4th Workshop on Computer Aided Verification, Montreal,Canada, June 29-July 1, 1992, pp.164-177.

[9] Murata T. Petri nets: Properties, analysis and applications.Proceedings of the IEEE, 1989, 77(4): 541-580.

[10] Roig O, Cortadella J, Pastor E. Verification of asynchronouscircuits by BDD-based model checking of Petri nets. In Proc.the 16th International Conference on Application and Theoryof Petri Nets, Turin, Italy, June 26-30, 1995, pp.374-391.

[11] Melzer S, Römer S. Deadlock checking using net unfoldings.In Proc. the 9th International Conference on Computer Ai-ded Verification, Haifa, Israel, June 22-25, 1997, pp.352-363.

[12] Khomenko V, Koutny M. LP deadlock checking using partialorder dependencies. In Proc. the 11th International Con-ference on Concurrency Theory, Pennsylvania, USA, August22-25, 2000, pp.410-425.

[13] Poliakov I, Mokhov A, Rafiev A, Sokolov D, Yakovlev A.Automated verification of asynchronous circuits using circuitPetri nets. In Proc. the 14th International Symposium onAsynchronous Circuits and Systems, Newcastle, UK, April7-10, 2008, pp.161-170.

[14] McMillan K L. A technique of state space search based onunfolding. Formal Methods in System Design, 1995, 6(1):45-65.

[15] Bruno J, Altman S M. A theory of asynchronous control net-works. IEEE Trans. Computers, 1971, 20(6): 629-638.

[16] Manohar R, Martin A J. Slack elasticity in concurrent com-puting. In Proc. the 4th International Conference on theMathematics of Program Construction, Marstrand, Sweden,June 15-17, 1998, pp.272-285.

[17] Bardsley A, Tarazona L, Edwards D. Teak: A token-flow im-plementation for the Balsa language. In Proc. the 9th Inter-national Conference on Application of Concurrency to Sys-tem Design, Augsburg, Germany, July 1-3, 2009, pp.23-31.

[18] SparsøJ, Furber S. Principles of Asynchronous Circuit De-sign —— A Systems Perspective, Kluwer Academic Publishers,2001.

[19] Beerel P A, Kim N H, Lines A, Davies M. Slack matchingasynchronous designs. In Proc. the 12th International Sym-posium on Asynchronous Circuits and Systems, Grenoble,France, March 13-15, 2006, pp.184-194.

[20] Prakash P, Martin A J. Slack matching quasi delay-insensitivecircuits. In Proc. the 12th International Symposiumon Asynchronous Circuits and Systems, Grenoble, France,March 13-15, 2006, pp.195-204.

[21] Gill G, Gupta V, Singh M. Performance estimation andslack matching for pipelined asynchronous architectures withchoice. In Proc. the 45th International Conference onComputer-Aided Design, San Jose, USA, November 10-13,2008, pp.449-456.

[22] Tarjan R E. Enumeration of the elementary circuits of a di-rected graph. SIAM Journal on Computing, 1973, 2: 211-216.

[23] Khomenko V. Punf documentation and user guide manual,Version 6.03, 2003.

[24] Khomenko V. A usable reachability analyser, CS-TR-1140,Newcastle Univ., http://homepages.cs.ncl.ac.uk/victorkhome-nko/tods/mpsat/CS-TR-1140.pdf, 2009.

[25] The SPARC architecture manual (Version 9), SPARCInternational, Inc., Weaver D L, Germond T (eds.),http://www.sparc.com/standards/SPARCV9.pdf, 1994.
No related articles found!
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed   
[1] Liu Mingye; Hong Enyu;. Some Covering Problems and Their Solutions in Automatic Logic Synthesis Systems[J]. , 1986, 1(2): 83 -92 .
[2] Chen Shihua;. On the Structure of (Weak) Inverses of an (Weakly) Invertible Finite Automaton[J]. , 1986, 1(3): 92 -100 .
[3] Gao Qingshi; Zhang Xiang; Yang Shufan; Chen Shuqing;. Vector Computer 757[J]. , 1986, 1(3): 1 -14 .
[4] Chen Zhaoxiong; Gao Qingshi;. A Substitution Based Model for the Implementation of PROLOG——The Design and Implementation of LPROLOG[J]. , 1986, 1(4): 17 -26 .
[5] Huang Heyan;. A Parallel Implementation Model of HPARLOG[J]. , 1986, 1(4): 27 -38 .
[6] Min Yinghua; Han Zhide;. A Built-in Test Pattern Generator[J]. , 1986, 1(4): 62 -74 .
[7] Tang Tonggao; Zhao Zhaokeng;. Stack Method in Program Semantics[J]. , 1987, 2(1): 51 -63 .
[8] Min Yinghua;. Easy Test Generation PLAs[J]. , 1987, 2(1): 72 -80 .
[9] Qiao Xiangzhen;. An Efficient Parallel Algorithm for FFT[J]. , 1987, 2(3): 174 -190 .
[10] Zhu Hong;. Some Mathematical Properties of the Functional Programming Language FP[J]. , 1987, 2(3): 202 -216 .

ISSN 1000-9000(Print)

         1860-4749(Online)
CN 11-2296/TP

Home
Editorial Board
Author Guidelines
Subscription
Journal of Computer Science and Technology
Institute of Computing Technology, Chinese Academy of Sciences
P.O. Box 2704, Beijing 100190 P.R. China
Tel.:86-10-62610746
E-mail: jcst@ict.ac.cn
 
  Copyright ©2015 JCST, All Rights Reserved