Refinement-Based Formal Verification of Asynchronous Wrappers for Independently Clocked Domains in Systems on Chip

  • Xiaohua Kong
  • Radu Negulescu
  • Larry Weidong Ying
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


In this paper we propose a novel refinement-based technique to formally verify data transfer in an asynchronous timing framework. Novel data transfer models are proposed to represent data communication between two locally independent clock domains. As a case study, we apply our technique to verify data transfer in a previously published architecture for globally asynchronous locally synchronous on-chip systems. In this case study, we find several race conditions, hazards, and other dangers that were not mentioned in the original publication, and we find additional delay constraints that avoid some of the detected dangers.


Boolean Function Data Transfer Clock Cycle Validity Event Race Condition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Bormann, D., Cheung, P.: “Asynchronous Wrapper for Heterogeneous Systems.” In Proc.Int. Conf. Computer Design (ICCD), Oct. 1996.Google Scholar
  2. 2.
    Brown, G., Luk, W., O’Leary, J.: “Retargeting a Hardware Compiler Proof Using Protocol Converters.” In Proc. Int. Symp. on Advanced Research in Asynchronous Circuits and Systems (ASYNC), pp: 54–64, 1994.Google Scholar
  3. 3.
    Calvert, K.L.; Lam, S.S.: “Formal methods for protocol conversion.” In IEEE Journal on Selected Areas in Communications, Jan. 1990, pp: 127–142.Google Scholar
  4. 4.
    Chapiro, D. M.: Globally-Asynchronous Locally-Synchronous Circuits. PhD thesis, Stanford University, U.S.A., Oct. 1984.Google Scholar
  5. 5.
    Dill, D.L.: Trace theory for Automatic Hierarchical Verification of Speed-Independent Circuits. (An ACM Distinguished Dissertation.) MIT press, 1989.Google Scholar
  6. 6.
    Hoare, C. A. R.: Communicating Sequential Processes. Prentice Hall, 1985.Google Scholar
  7. 7.
    Kong, X., Negulescu, R.: “Formal Verification of Pulse-Mode Asynchronous Circuits.” In Proc. Asia and South Pacific Design Automation Conference (ASP-DAC), Jan. 2001.Google Scholar
  8. 8.
    Muttersbach, J,. Villiger, T,. Fichtner, W.: “Practical Design of Globally-Asynchronous Locally-Synchronous Systems.” In Proc. Int. Symp. on Advanced Research in Asynchronous Circuits and Systems (ASYNC), Mar. 2000.Google Scholar
  9. 9.
    Muttersbach, J,. Villiger, T,. Kaeslin, H,. Felber, N,. Fichtner, W.: “Globally-Asynchronous Locally-Synchronous Architectures to Simplify the Design of On-Chip Systems.” In Proceedings of ASIC/SOC Conference, pp. 317–321, 1999.Google Scholar
  10. 10.
    Myers, C.J.; Rokicki, T.G.; Meng, T.H.-Y: “POSET timing and its application to the synthesis and verification of gate-level timed circuits.” IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Volume:20, pp: 769–786, June 1999.Google Scholar
  11. 11.
    Negulescu, R.: Process Spaces and Formal Verification of Asynchronous Circuits. PhD thesis, University of Waterloo, Canada, 1998.Google Scholar
  12. 12.
    Negulescu, R.: “Process spaces.” In Proc. Int. Conf. on Concurrency Theory (CONCUR), pp. 196–210, Aug. 2000.Google Scholar
  13. 13.
    Negulescu, R., Kong X.: “Semi-hiding Operators and the Analysis of Active-Edge Specifications for Digital Circuits.” In Proc. Int. Conf. on Application of Concurrency to System Design (ICACSD-2001), Apr. 2001.Google Scholar
  14. 14.
    Negulescu, R., Peeters, A.: “Verification of speed-dependences in single-rail handshake circuits.” In Proc. Int. Symp. on Advanced Research in Asynchronous Circuits and Systems, pp. 159–170, 1998.Google Scholar
  15. 15.
    Okumura, K.: “Generation of proper adapters and converters from a formal service specification.” In Proc. of Ninth Annual Joint Conference of the IEEE Computer and Communication Societies. The Multiple Facets of Integration, pp: 564–571, 1990.Google Scholar
  16. 16.
    Peeters, A. M. G.: Single-Rail Handshake Circuits. PhD thesis, Eindhoven Univ. of Technology, Eindhoven, The Netherlands, Jun. 1996.Google Scholar
  17. 17.
    Peña, M. A., Cortadella, J., Kondratyev, A. and Pasor, E.: “Formal verification of safety properties in timed circuits.” In Proc. Int. Symp. on Advanced Research in Asynchronous Circuits and Systems (ASYNC), pp 2–12, 2000.Google Scholar
  18. 18.
    Rowson, J.A., Sangiovanni-Vincentelli, A.: “Interface-Based Design.” In Proceedings of the 4th Design Automation Conference (DAC), pp.: 178–183, 1997.Google Scholar
  19. 19.
    Tao, Z.P., v. Bochmann G., Dssouli, R.: “An efficient method for protocol conversion.” In Proc. Int. Conf. on Computer Communications and Networks, pp. 40–47, 1995.Google Scholar
  20. 20.
    Yun, K. Y., Donohue, R. P.: “Pausible clocking: a first step toward heterogeneous systems.” In Proc. Int. Conf. Computer Design (ICCD), pp. 118–123, 1996.Google Scholar
  21. 21.
    Yun, K. Y., Dill, D. L.: “Automatic synthesis of extended burst-mode circuits: Part I and Part II.” IEEE Transactions on Computer-Aided Design, vol. 20, no. 2, pp. 101–132, 1999.CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Xiaohua Kong
    • 1
  • Radu Negulescu
    • 1
  • Larry Weidong Ying
    • 1
  1. 1.Microelectronics And Computer Systems Laboratory Dept. of ECEMcGill University MontrealCanada

Personalised recommendations