Probabilistic model checking of clock domain crossing interfaces

摘要

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.