Formal Verification of Synchronizers

  • Tsachy Kapschitz
  • Ran Ginosar
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3725)


Large Systems on Chips (SoC) comprise multiple clock domains, and inter-domain data transfers require synchronization. Synchronizers may fail due to metastability, but when using proper synchronization circuits the probability of such failures can be made negligible. Failures due to unexpected order of events (caused by interfacing multiple unrelated clocks) are more common. Correct synchronization is independent of event order, and can be verified by model checking. Given a synchronizer, a correct protocol is guessed, verification rules are generated out of the protocol specification, and the model checker applies these rules to the given synchronizer. An alternative method verifies correct data transfer and seeks potential data missing or duplication. Both approaches require specific modeling of multiple clocks, allowing for non-determinism in their relative ordering. These methods have been applied successfully to several synchronizers.


  1. 1.
    Iyer, A., Marculescu, D.: Power Efficiency of Voltage Scaling in Multiple Clock, Multiple Voltage Cores. In: IEEE/ACM Int. Conf. on Computer Aided Design (ICCAD), November 2002, pp. 379–386 (2002)Google Scholar
  2. 2.
    Dally, W.J., Poulton, J.W.: Digital System Engineering. Cambridge University Press, Cambridge (1998)Google Scholar
  3. 3.
    Kleeman, L., Cantoni, A.: Metastable behavior in digital systems. IEEE Design and Test of Computers, 4–19 (December 1987)Google Scholar
  4. 4.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)Google Scholar
  5. 5.
    Beer, I., Ben-David, S., Eisner, C., Landver, A.: RuleBase: an industry-oriented formal verification tool. In: Design Automation Conference, June 1996, pp. 665–660 (1996)Google Scholar
  6. 6.
    Gordon, M., Hurd, J., Slind, K.: Executing the formal semantics of the Accellera Property Specification Language by mechanised theorem proving. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 200–215. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. 7.
    Kapschitz, T., Ginosar, R.: Formal Verification of Synchronizers. CCIT Tech. Rep. 536, EE Dept., Technion (2005)Google Scholar
  8. 8.
    Frank, U., Ginosar, R.: A Predictive Synchronizer for Periodic Clock Domains. In: Macii, E., Paliouras, V., Koufopavlou, O. (eds.) PATMOS 2004. LNCS, vol. 3254, pp. 402–412. Springer, Heidelberg (2004)Google Scholar
  9. 9.
    Chu, T.A., Leung, C.K.C., Wanuga, T.S.: A Design Methodology for Concurrent VLSI Systems. In: Proc. of ICCD, pp. 407–410 (1985)Google Scholar
  10. 10.
    Cortadella, J., Kishinevsky, M., Kondratyev, A., Lavagno, L., Yakovlev, A.: Complete state encoding based on the theory of regions. In: 2nd Int. Symp. Asynchronous Circuits and Systems, March 1996, pp. 36–47 (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Tsachy Kapschitz
    • 1
  • Ran Ginosar
    • 1
  1. 1.VLSI Systems Research Center, Electrical Engineering DepartmentTechnion–Israel Institute of TechnologyHaifaIsrael

Personalised recommendations