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
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;
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
DOI :
10.1109/NEWCAS.2012.6328989
