• DocumentCode
    2067636
  • Title

    Verification of a Data Synchronization Circuit For All Time

  • Author

    Brown, Geoffrey M.

  • Author_Institution
    Indiana Univ., IN
  • fYear
    2006
  • fDate
    28-30 June 2006
  • Firstpage
    217
  • Lastpage
    228
  • Abstract
    This paper presents a model and automated proof for a synchronizer circuit that is commonly used to reliably transfer data across clock domains. In contrast with previous work, this paper describes a proof that is valid for all clock rates and phases meeting modest constraints. Furthermore, the proof was realized with an existing model checker - SAL
  • Keywords
    clocks; formal verification; logic circuits; logic design; synchronisation; SAL model checker; clock domain; data synchronization circuit verification; synchronizer circuit automated proof; Analytical models; Bridge circuits; Circuit analysis; Clocks; Flip-flops; Metastasis; Protocols; Synchronization; Timing; Transmitters;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Application of Concurrency to System Design, 2006. ACSD 2006. Sixth International Conference on
  • Conference_Location
    Turku
  • ISSN
    1550-4808
  • Print_ISBN
    0-7695-2556-3
  • Type

    conf

  • DOI
    10.1109/ACSD.2006.35
  • Filename
    1640239