›› 2016, Vol. 31 ›› Issue (1): 77-106.doi: 10.1007/s11390-016-1613-y

Special Issue: Computer Architecture and Systems; Theory and Algorithms

• Computer Architectures and Systems • Previous Articles     Next Articles

Modular Timing Constraints for Delay-Insensitive Systems

Hoon Park1,2, Anping He3*, Marly Roncken1, Xiaoyu Song2, and Ivan Sutherland1   

  1. 1 Asynchronous Research Center, Portland State University, Portland, OR 97201, U.S.A.;
    2 Department of Electrical and Computer Engineering, Portland State University, Portland, OR 97201, U.S.A.;
    3 School of Information Science and Engineering, Lanzhou University, Lanzhou 730000, China
  • Received:2014-10-14 Revised:2015-07-11 Online:2016-01-05 Published:2016-01-05
  • Contact: Anping He E-mail:heap@lzu.edu.cn
  • About author:Hoon Park is a Ph.D. candidate in the Department of Electrical and Computer Engineering, Portland State University. Hoon was born in Seoul, Korea, and received his B.S. degree in mechanical engineering from Pukyong National University in 2004. He received his M.S. degree in electrical and computer engineering from Portland State University in 2007. He joined the Asynchronous Research Center in 2011 where he started focusing his research on verifying timing constraints for asynchronous circuits.
  • Supported by:

    This work was supported by the National Natural Science Foundation of China under Grant No. 61402121.

This paper introduces ARCtimer, a framework for modeling, generating, verifying, and enforcing timing constraints for individual self-timed handshake components. The constraints guarantee that the component's gate-level circuit implementation obeys the component's handshake protocol specification. Because the handshake protocols are delay insensitive, self-timed systems built using ARCtimer-verified components are also delay-insensitive. By carefully considering time locally, we can ignore time globally. ARCtimer comes early in the design process as part of building a library of verified components for later system use. The library also stores static timing analysis (STA) code to validate and enforce the component's constraints in any self-timed system built using the library. The library descriptions of a handshake component's circuit, protocol, timing constraints, and STA code are robust to circuit modifications applied later in the design process by technology mapping or layout tools. In addition to presenting new work and discussing related work, this paper identifies critical choices and explains what modular timing verification entails and how it works.

[1] Sawada J, Hunt W A Jr. Verification of FM9801:An out-oforder microprocessor model with speculative execution, exceptions, and program-modifying capability. Formal Methods in System Design, 2002, 20(2):187-222.

[2] Slobodová A, Davis J, Swords S, Hunt W A Jr. A flexible formal verification framework for industrial scale validation. In Proc. the 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), July 2011, pp.89-97.

[3] Yan C, Ouchet F, Fesquet L, Morin-Allory K. Formal verification of C-element circuits. In Proc. the 17th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC), April 2011, pp.55-64.

[4] Sutherland I, Sproull B, Harris D. Logical Effort:Designing Fast CMOS Circuits. San Francisco, CA, USA:Morgan Kaufmann Publishers, 1999.

[5] Sutherland I. Micropipelines. Communications of the ACM, 1989, 32(6):720-738.

[6] Sparsø J, Furber S (eds.). Principles of Asynchronous Circuit Design - A Systems Perspective. Dordrecht, The Netherlands:Kluwer Academic Publishers, 2001.

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

[8] Beerel P A, Ozdag R O, Ferretti M. A Designer's Guide to Asynchronous VLSI. New York, NY, USA:Cambridge University Press, 2010.

[9] Sutherland I, Fairbanks S. GasP:A minimal FIFO control. In Proc. the 7th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC), March 2001, pp.46-53.

[10] Sutherland I. GasP Circuits that Work. ECE 507 Research Seminar, Fall 2010. Asynchronous Research Center, Portland State University. http://arc.cecs.pdx.edu/fall10, Sept. 2015.

[11] Martin A J, Nyström M. Asynchronous techniques for system-on-chip design. Proceedings of the IEEE, 2006, 94(6):1089-1120.

[12] Sheikh B R, Manohar R. Energy-efficient pipeline templates for high-performance asynchronous circuits. ACM Journal on Emerging Technologies in Computing Systems, 2011, 7(4):19:1-19:26.

[13] Singh M, Nowick S M. MOUSETRAP:High-speed transition-signaling asynchronous pipelines. IEEE Transactions on Very Large Integration (VLSI) Systems, 2007, 15(6):684-698.

[14] Peeters A, te Beest F, de Wit M, Mallon W. Click elements:An implementation style for data-driven compilation. In Proc. the 16th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC), May 2010, pp.3-14.

[15] Scheffer L, Lavagno L, Martin G (eds.). Electronic Design Automation for Integrated Circuits Handbook, Volumes 1- 2. Boca Raton, FL, USA:CRC Press and Taylor & Francis, 2006.

[16] van Berkel K, Burgess R, Kessels J, Roncken M, Schalij F, Peeters A. Asynchronous circuits for low power:A DCC error corrector. IEEE Design & Test of Computers, 1994, 11(2):22-32.

[17] Kessels J, Marston P. Designing asynchronous standby circuits for a low-power pager. Proceedings of the IEEE, 1999, 87(2):257-267.

[18] Stevens K S, Rotem S, Ginosar R, Beerel P, Myers C J, Yun K Y, Kol R, Dike C, Roncken M. An asynchronous instruction length decoder. IEEE Journal of Solid-State Circuits, 2001, 36(2):217-228.

[19] Sheikh B R, Manohar R. An operand-optimized asynchronous IEEE 754 double-precision floating-point adder. In Proc. the 16th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC), May 2010, pp.151-162.

[20] Sheikh B R, Manohar R. An asynchronous floating-point multiplier. In Proc. the 18th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC), May 2012, pp.89-96.

[21] Sapatnekar S S. Chapter 6:Static timing analysis. In Electronic Design Automation for Integrated Circuits Handbook, Volume 2, Scheffer L, Lavagno L, Martin G (eds.), Boca Raton, FL, USA:CRC Press and Taylor & Francis, 2006.

[22] Prakash M, Beerel P A. Static Timing Analysis of Template-Based Asynchronous Circuits. US Patent US 2009/0210841 A1, University of Southern California, August 20, 2009.

[23] Stevens K S, Xu Y, Vij V. Characterization of asynchronous templates for integration into clocked CAD flows. In Proc. the 15th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC), May 2009, pp.151-161.

[24] Beerel P A, Dimou G D, Lines A M. Proteus:An ASIC flow for GHz asynchronous designs. IEEE Design & Test of Computers, 2011, 28(5):36-51.

[25] Vij V. Algorithms and methodology to design asynchronous circuits using synchronous CAD tools and flows[Ph.D. Thesis]. Electrical and Computer Engineering, The University of Utah, USA, 2013.

[26] Xu Y. Algorithms for automatic generation of relative timing constraints[Ph.D. Thesis]. Electrical and Computer Engineering, The University of Utah, USA, 2011.

[27] Meng T. Synchronization Design for Digital Systems. Norwell, MA, USA:Kluwer Academic Publishers, 1991.

[28] Lavagno L, Sangiovanni-Vincentelli A. Algorithms for Synthesis and Testing of Asynchronous Circuits. Norwell, MA, USA:Kluwer Academic Publishers, 1993.

[29] Cortadella J, Kishinevsky M, Kondratyev A, Lavagno L, Yakovlev A. Logic Synthesis of Asynchronous Controllers and Interfaces. Springer-Verlag, 2002.

[30] Josephs M B, Udding J T. An algebra for delay-insensitive circuits. In Proc. the 2nd Computer Aided Verification (CAV), July 1991, pp.343-352.

[31] Verhoeff T. A theory of delay-insensitive systems[Ph.D. Thesis]. Department of Mathematics and Computing Science, Eindhoven University of Technology, The Netherlands, 1994.

[32] Mallon W C. Theories and tools for the design of delayinsensitive communicating processes[Ph.D. Thesis]. Mathematics and Natural Sciences, University of Groningen, The Netherlands, 2000.

[33] Negulescu R. Process spaces and formal verification of asynchronous circuits[Ph.D. Thesis]. Computer Science, University of Waterloo, Canada, 1998.

[34] Clarke E M, Grumberg O, Peled D A. Model Checking. Cambridge, MA, USA:The MIT Press, 1999.

[35] Negulescu R, Peeters A. Verification of speed-dependences in single-rail handshake circuits. In Proc. the 4th IEEE International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC), March 30-April 2, 1998, pp.159-170.

[36] Cavada R, Cimatti A, Jochim C A, Keighren G, Olivetti E, Pistore M, Roveri M, Tchaltsev A. NuSMV 2.4 User Manual. 2013. http://nusmv.fbk.eu/NuSMV/userman/v24/nusmv.pdf, Sept. 2015.

[37] Desai K, Stevens K S, O'Leary J. Symbolic verification of timed asynchronous hardware protocols. In Proc. the IEEE Computer Society Annual Symposium on VLSI (ISVLSI), August 2013, pp.147-152.

[38] Muller D E, Bartky W S. A theory of asynchronous circuits. In Proc. International Symposium on the Theory of Switching, April 1959, pp.204-243.

[39] Miller R E. Chapters 9-10:Asynchronous switching networks & speed independent switching circuit theory. In Switching Theory Volume 2:Sequential Circuits and Machines, New York, USA:John Wiley & Sons, 1965.

[40] Beerel P A, Roncken M E. Low power and energy efficient asynchronous design. Journal of Low Power Electronics (JOLPE), 2007, 3(3):234-253.

[41] Stevens K S, Ginosar R, Rotem S. Relative timing. IEEE Transactions on Very Large Scale Integration (VLSI) Systems, 2003, 11(1):129-140.

[42] Park H, He A, Roncken M, Song X. Semi-modular delay model revisited in context of relative timing. Electronics Letters, 2015, 51(4):332-334.

[43] Alsayeg K, Morin-Allory K, Fesquet L. RAT-based formal verification of QDI asynchronous controllers. In Proc. Forum on Specification & Design Languages (FDL), September 2009, pp.1-6.

[44] Yoneda T, Kitai T, Myers C. Automatic derivation of timing constraints by failure analysis. In Proc. the 14th International Conference on Computer Aided Verification (CAV), July 2002, pp.195-208.

[45] Peña M A, Cortadella J, Kondratyev A, Pastor E. Formal verification of safety properties in timed circuits. In Proc. the 6th IEEE International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC), April 2000, pp.2-11.

[46] Kim H, Beerel P A, Stevens K. Relative timing based verification of timed circuits and systems. In Proc. the 8th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC), April 2002, pp.115-124.

[47] Xu Y, Stevens K S. Automatic synthesis of computation interference constraints for relative timing verification. In Proc. the 27th IEEE International Conference on Computer Design (ICCD), October 2009, pp.16-22.

[48] Fuhrer R M, Nowick S M. Sequential Optimization of Asynchronous and Synchronous Finite-State Machines:Algorithms and Tools. Norwell, MA, USA:Kluwer Academic Publishers, 2001.

[49] Prakash M. Library characterization and static timing analysis of asynchronous circuits[Master's Thesis]. Computer Engineering, University of Southern California, USA, December 2007.

[50] Joshi P. Static timing analysis of GasP[Master's Thesis]. Electrical Engineering, University of Southern California, USA, December 2008.

[51] Mettala Gilla S. Library characterization and static timing analysis of single-track circuits in GasP[Master's Thesis]. Electrical and Computer Engineering, Portland State University, USA, 2010.

[52] Roncken M, Mettala Gilla S, Park H, Jamadagni N, Cowan C, Sutherland I. Naturalized communication and testing. In Proc. the 21st IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC), May 2015, pp.77-84.

[53] Iizuka M, Hamada N, Saito H, Yamaguchi R, Yoshinaga M. A tool set for the design of asynchronous circuits with bundled-data implementation. In Proc. the 29th IEEE International Conference on Computer Design (ICCD), October 2011, pp.78-83.

[54] Seitz C L. Chapter 7:System timing. In Introduction to VLSI Systems, Mead C, Conway L (eds.), Boston, MA, USA:Addison-Wesley, 1980, pp.218-262.
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] Zhu Hong;. Some Mathematical Properties of the Functional Programming Language FP[J]. , 1987, 2(3): 202 -216 .
[10] Li Minghui;. CAD System of Microprogrammed Digital Systems[J]. , 1987, 2(3): 226 -235 .

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