Abstract
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.
Chapter PDF
Similar content being viewed by others
References
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)
Dally, W.J., Poulton, J.W.: Digital System Engineering. Cambridge University Press, Cambridge (1998)
Kleeman, L., Cantoni, A.: Metastable behavior in digital systems. IEEE Design and Test of Computers, 4–19 (December 1987)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
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)
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)
Kapschitz, T., Ginosar, R.: Formal Verification of Synchronizers. CCIT Tech. Rep. 536, EE Dept., Technion (2005)
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)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kapschitz, T., Ginosar, R. (2005). Formal Verification of Synchronizers. In: Borrione, D., Paul, W. (eds) Correct Hardware Design and Verification Methods. CHARME 2005. Lecture Notes in Computer Science, vol 3725. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11560548_31
Download citation
DOI: https://doi.org/10.1007/11560548_31
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29105-3
Online ISBN: 978-3-540-32030-2
eBook Packages: Computer ScienceComputer Science (R0)