• DocumentCode
    1723021
  • Title

    Probabilistic model checking of clock domain crossing interfaces

  • Author

    Al-bayati, Zaid ; Mohamed, O. Ait ; Savaria, Yvon ; Boukadoum, Mounir

  • Author_Institution
    ECE Dept., Concordia Univ., Montréal, QC, Canada
  • fYear
    2012
  • Firstpage
    193
  • Lastpage
    196
  • Abstract
    Clock domain crossing (CDC) interfaces constitute an increasingly essential part of large digital systems and Systems on Chip (SoCs). These interfaces are inherently difficult to design and debug. In this paper, we demonstrate how probabilistic model checking can be employed in the verification of CDC protocols. Popular CDC interfaces are modeled as Markov Decision Processes and verified using the PRISM model checker.
  • Keywords
    Markov processes; clocks; probability; protocols; CDC interface; CDC protocol; Markov decision processing; PRISM model checker; SoC; clock domain crossing interface; digital system; probabilistic model checking; system on chip; Clocks; Flip-flops; Probabilistic logic; Protocols; Receivers; Synchronization;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    New Circuits and Systems Conference (NEWCAS), 2012 IEEE 10th International
  • Conference_Location
    Montreal, QC
  • Print_ISBN
    978-1-4673-0857-1
  • Electronic_ISBN
    978-1-4673-0858-8
  • Type

    conf

  • DOI
    10.1109/NEWCAS.2012.6328989
  • Filename
    6328989
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=1723021