Probabilistic model checking of clock domain crossing interfaces

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

NEWCAS（2012）

引用 1|浏览4

暂无评分

摘要

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.

查看译文

关键词

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

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要