二乘二片上网络系统可靠性的概率验证
Probabilistic Verification for Reliability of a Two-by-Two Network-on-Chip System
摘要：
由于工艺和环境的变化，现代片上网络（NoC）系统面临着可靠性问题。NoC供电网络中的电源噪声（PSN）在确定可靠性方面起着关键作用。PSN导致电压下降，这可能导致NoC中的定时误差。本文对NoC系统中PSN的形式化分析做出了新的贡献。我们提出了一种概率模型检验的方法来观察PSN在一个通用的2x2网状片上网络具有均匀的随机流量负载。PSN的主要特征是在行为层面上测量的。为了解决状态爆炸，我们采用增量抽象技术，包括一种新的概率选择抽象，基于NoC行为的观察。Modest工具集用于概率建模和验证。结果得到几个微片注入模式，以揭示其对PSN的影响。我们的分析发现了一个最佳的微片模式生成PSN事件的概率为零，并建议分散微片，而不是释放他们在连续的周期，以尽量减少PSN。
英文摘要：
Modern network-on-chip (NoC) systems face reliability issues due to process and environmental variations. The power supply noise (PSN) in the power delivery network of a NoC plays a key role in determining reliability. PSN leads to voltage droop, which can cause timing errors in the NoC. This paper makes a novel contribution towards formally analyzing PSN in NoC systems. We present a probabilistic model checking approach to observe the PSN in a generic 2x2 mesh NoC with a uniform random traffic load. Key features of PSN are measured at the behavioral level. To tackle state explosion, we apply incremental abstraction techniques, including a novel probabilistic choice abstraction, based on observations of NoC behavior. The Modest Toolset is used for probabilistic modeling and verification. Results are obtained for several flit injection patterns to reveal their impacts on PSN. Our analysis finds an optimal flit pattern generation with zero probability of PSN events and suggests spreading flits rather than releasing them in consecutive cycles in order to minimize PSN.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
