MPSoC核协调可靠性和性能的形式化验证

发布时间：2017-09-17 06:03

  本文关键词：MPSoC核协调可靠性和性能的形式化验证

  更多相关文章： 片上多核处理器 核协调 混杂变迁系统 混杂马尔科夫决策过程 随机时序逻辑 PRISM模型检测器 数据脱敏

【摘要】：为了在早期发现片上多核处理器(MPSoC)设计缺陷,提出一种对核协调进行结构建模和性质刻画的形式化方法。在标记变迁系统中引入多项式函数替代动作表达核协调过程中对数据的改变,加入物理元器件发生故障的概率属性,形成用以描述核协调可靠性和性能的混杂马尔科夫决策过程模型。采用随机时序逻辑刻画系统性质,通过模型检测工具验证分析,以银行数据脱敏MPSoC为例,分析系统可靠性和时间延迟与能耗等性能指标。这些验证结果对于早期MPSoC设计人员具有较强的指导作用。
【作者单位】： 中国科学院成都计算机应用研究所;中国科学院大学;贵州银行博士后科研工作站;广西民族大学广西混杂计算与集成电路设计分析重点实验室;
【关键词】： 片上多核处理器 核协调 混杂变迁系统 混杂马尔科夫决策过程 随机时序逻辑 PRISM模型检测器 数据脱敏
【基金】：国家自然科学基金资助项目(11371003;11461006) 广西科技基金项目(10169-1) 广西自然科学基金项目(2012GXNSFGA060003) 广西教育厅科研项目(201012MS274)
【分类号】：TP332
【正文快照】： 网络通信、多媒体、信号处理、科学计算和信息安全等的蓬勃发展,使得基于数据运算的单一功能环境,转向基于操作的多任务、多功能和多制式化环境发展[1]。受时钟、功耗和尺寸等因素的制约,基于单任务的单核处理器集成已很难满足新型复杂应用的计算需求。MPSo C使用复杂的片上网，

本文编号：867665