引言

软 错 误 是 一 种 对 硬 件 本 身 没 有 破 坏 性 的 瞬 态逻辑错误 与 设 计 制 造 过 程 中 引 入 的 硬 错误相比软错误 具 有 瞬 态 可 恢 复发 生 时 间 任 意性和发生位置 任 意 性 的 特 点 能够引发软错误的环境 因 素 很 多 例 如电 源 噪 声电 磁 干 扰空 间 辐射等其中最主要的是辐射 辐射主要来源于芯片封装材料中的粒子以及宇宙射线中的中子 这些高能粒子轰击半导体器件生成电子 空 穴 对生 成的自由电荷在被轰击器件的源极和漏极聚集 当电荷量积累到一定程度就将改变逻辑器件 锁 存 器静态随机存储单 元 或 者 组 合 门正常的逻辑状态从而使得电路 的 操 作 发 生 逻 辑 错 误 随 着 设 计 工艺的 不 断 提 高 尤 其 是 进 入 工 艺 之 后芯 片的阈值电压进一步降低 集成的晶体管数目呈指数增长超大规 模 集 成 电 路设计对辐射越来越敏感软 错 误 率 急剧上升可靠性 受 到 严 重 威 胁 这 就 是 所 谓 的 软错误墙 它是继存储墙和功耗墙之后半导体工业遭遇的又一大技术难题

系 统 中 的 组 件 组 合 门时 序 单 元 或 者功能块一旦发生软错误 就可能引发系统失效 而容错技术则可以保证系统在发生软错误的情况下仍然能够正常运行或者降级运行 已 有 的 容 错 机制通常利用 硬 件 软 件时 间 以 及 信 息 冗 余 来 实现因此如果对整个系统施加全面的软错误保护机制代价十分高 昂 这对于主流的商业应用来说很难接受 然而并非所有的软错误都会导致系统级失效 因此为了同时满足设计的性能 面积功耗以及可靠性等多目标需求 通常都对系统进行有选择的软错误保护对于有选择性的软错误保护来说首要的问题在于评价分析发生在系统中的软错误可能造成的影响以指导容 错 机 制 的 有 效 部 署也 就 是 软 错 误可靠性分析 在 设计 过 程 中越 早 进 行 软 错误可靠性分析软错误保护所需要的代价越小 然而 设计流程是自顶向下分层次进行的不同抽象层次的设计模型包含的设计细节不同 因此为了方便与已有的 设 计 流 程 融 合 软 错误可靠性分析也按照自顶向下分层次进行 软 错误系统级可靠性评价位于整个可靠性评价流程的最顶 层它 主 要 以 寄 存 器 传 输 级模 型体 系 结 构 微体系结构级模型以及更高层模型为分析对象 对由软故障引发的错误导致系统失效的可能性进行评估 由 于 它 在集成电路 设 计 的 早 期 就 展开可靠性分析一方面其分析的对象为系统的高层模型抽象层次高不涉及复杂的设计细节 因此分析效率也更高另一方面它能够更早地指导容错机制的规划和部署 减 少 返 工 造 成 的 开 销 缩 短 芯 片上市时间 目前软错误的系统级可靠性评价已经成为了学术界的研究热点

软错误系统级可靠性评价

基础系统 受 到 空 间 辐 射 之 后 发 生 的 瞬 态 故障分为三类单事件瞬态单事件翻转 以及多位翻转组合逻辑门受到高能粒子轰击 在输出产生一个宽 到 的 短 时 脉 冲 这 就是 由于 在 电 路 的 组 合 逻 辑 部 分 传 播的过程中受到三种组合逻辑掩盖效应 的削 弱并不一定会对下游时序单元产生影响 电 子 掩 盖当 短时脉冲在组合逻辑部分传播时 由于它所经过的逻辑门所具有的电子属性脉冲强度会在传播过程中被逐渐削弱当削弱到一定程度时 将无法对下游的时序单元产生影响 逻 辑 掩 盖 在的传播 路 径 上 如 果 下 游 某 个 组 合 门 的 输 出结果与其位于故障传播路径上的引脚输入值无关而仅仅取决于 其 他 输 入 引 脚 的 取 值 那 么 将会被 逻 辑 掩 盖 锁 存 窗 口 掩 盖如 果 短 时 脉 冲 不 能 在 下游时序单元采样输入的时间窗口内到达那 么的错误逻辑信号就不会被该时序单元采样从而不会对下一级逻辑产生影响单个时序单元受到高能粒子轰击时逻辑值将发生翻转这就是单事件翻转 在以往的集成电路制造工艺下单个高能粒子轰击最多只能导致一个时序单元发生翻转 即 但 是随 着 设 计 特 征尺寸的不断缩小以及集成度的不断提高单个高能粒子将有可能导致多个相邻的时序单元同时发生翻转这就是多 位 翻 转 通 常 发 生 在 时 序 单元比较密集的 以及寄存器文件中除了 时 序 单 元 直 接 受 到 粒 子 轰 击 可 能 引 发或 者 之 外如 果 能 够 顺 利 通 过 电路中的组合逻辑部分 传播到下游的一个或者多个时序单元也将引发 或者上述 三 类 瞬 态 故 障 也 称 为 原 始 软 错 误 事 件简 称 原 始 软 错 误 原 始软错误导致电路中时序单元发生的位翻转称为错误 错误是原始软错误在系统内部的表征只有错误才能在之后的若干个周期内对系统的操作产生影响 因 此发 生 在 时 序 单 元 中 的 和本身就是错误 当错误能够传播到系统输出时就会导致系统失效 失效是能够被系统用户感知的错误 对于普通的设计来说 错误是否会引发失效取决于逻辑掩盖效应 然而对于处理器类的体系结构设计来说除了上述三种逻辑掩盖效应之外 还需要考虑如下的体系结构和微体系结构掩盖效应高性能微处理器中资源利用率相对较低发生在空闲单元中的软错误不会引发系统失效部分体系结构资源仅为处理器性能服务不对系统功能造成影响 发生在这类组件中的软错误也不会导致系统失效计算机工程与科学由 于 逻 辑 掩 盖 效 应 以 及 体 系 结 构 与 微 体 系 结构掩盖效应的共同作用 并非所有的错误都会引发系统级失效图 展示了软错误可靠性分析的分层模型 软错误系统级可靠性评价位于整个可靠性分析流程最顶层通常在寄存器传输级以及更高层模型中展开分析评价由原始软错误引发的错误在逻辑掩盖与体系结构微体系结构掩盖效应下可能对系统功能产生的影响即量 化 错 误 导 致 系 统 失 效 的 可 能 性 从概率论的角 度 出 发 就 是 计 算 条 件 概 率其下一层为逻辑层可靠性评价 也称为门级软错误率分析 它们综合分析组合路径上的三种掩盖效应电子 掩 盖逻 辑 掩 盖锁 存 窗 口 掩 盖 以 估算 引发错 误即 下 游 时 序 单 元 发 生 位 翻 转的可能性 最 底 层 为 物 理 层 可 靠 性 分析它 们 通 常 通 过 模拟来分析被粒子轰击的静态逻辑器件 发 生 原 始 软 错 误 的 可 能 性条 件 概 率以 及 随 机 逻 辑 器 件 发 生 原 始 软错误的可能性即 条 件 概 率 ＿因此也称为物理层软错误率 简 称分析 综合上面各个层次的分析结果 高能粒子辐射引发错误的可能性计算如下＿因此系统失效的可能性计算为其中 表 示 应 用 环 境 中 发 生 粒 子 辐 射的概率图 软错误可靠性评价自 顶 向 下 的 可 靠 性 分 析 过 程 是 一 个 逐 步 精 化的分析过程每一层的可靠性分析对于整个系统的可靠性分析都 是 必 不 可 少 的 这 种 分 层 的 可 靠 性分析过程的目的就是在 设计过程中尽早地识别由软错误引发的不可接受的错误行为从而方便设计者尽早地修改设计方案或者部署容错机制 使得最终的设计满足可靠性需求 与整个 设计流程结束之后再进行可靠性分析和容错相比这种分层的可靠性分析过程能够极大地减少返工所需的代价缩短产品面市时间

软错误系统级可靠性评价方法概况

错误模型系统 级 软 错 误 可 靠 性 评 价 对 原 始 软 错误引发的错误可能对系统功能正确性产生的影响进行量化分析因此采用的错误模型为 或 者正 如 前 面 所 介 绍 的 能 够 引 发 和的因素有两种一 是 时 序 单 元 直 接 被 粒 子 轰击二是 顺利通过组合逻辑部分导 致 下 游 的一个或 者 多 个 时 序 单 元 发 生 位 翻 转 然 而由 于的产生受器件 布 局 入 射 粒 子 的 能 量 以 及 入射角度等因 素 的 限 制 因 此除 了 在 时 序 单 元 密集的存储器部分以及寄存器文件部分之外粒子轰击时序单元引发 的概率远远大于 此外在进入 工 艺 之 前 发 生 在 组 合 逻 辑 单 元中的 由于受到各种掩盖效应的影响 能 够 引发 或者 的 概 率 都 较 小 因 此过 去 的研究一直认为时序单元对软错误的敏感度远远高于组合逻辑单 元 所以大多数方法都以 为 错误模型针对电路中的时序逻辑部分进行分析 然而随着 制 造 工 艺 的 进 步 设 计 特 征 尺 寸 的 缩小信号传输延迟减小以及时钟频率增加 组 合 逻辑部分的三种掩盖效应都不同程度地被削弱了 这使得 被其下游的时序逻辑单元锁住的可能性急剧增加 据估计到 年组合逻辑部分的软错误对 系 统 失 效 率 的 贡 献 将 与 时 序 逻 辑 部 分 相当 因此 也 成 为 了 系 统 级 可 靠 性 评 价领域不 得 不 考 虑 的 问 题 目 前已 有 部 分 研 究 工作 开始以 为错误模型展开分析难点理想情况下要 获 得 完 备 的 可 靠 性 评 价 结 果就必须遍历目标系统的整个输入空间 状 态 空 间以及故障空间分析任意情况下软错误可能对系统造 成 的 影 响 然 而对 于 规 模 较 大 的 系 统 来 说要得到这种完备的分析结果是非常困难的 首 先大朱 丹 等 系统级软错误可靠性评价 综 述型系统的输入空间和状态空间都很大 难 以 穷 尽其次软错误具有多维不确定性 即 时间维可能发生在系统操作的任意时刻 空间维可能发生在设计中的任意一个逻辑结点上 数据维可能在处理任意 数 据 时 发 生 即使可靠性评价选择作为错 误 模 型 软错误的这种多维不确定性也会导致软错误可靠性评价需要处理的问题空间巨大计 算 复 杂 度 极 高 如 果 以 为 错 误 模型情况将更加复杂分类及概况除了采用的错误模型不同之外 各种已有的方法进行可靠性评价的目的也不尽相同 例如有的方法是为了从电路中或者系统中筛选需要软错误保护的关键组件 指导容错代价与可靠性间的有效权衡有的方法是为了识别详细的错误传播路径以确定电路中进行软错误保护的最佳位置 还 有的方法是为了评估容错设计的有效性 出 于 不 同的目的各种方法采用的核心技术也不同 本文从技术实现的角度将已有的软错误系统级可靠性评价方法分为三类 基 于 故 障 模 拟 的 方 法 无 故 障 模拟方法以及基于形式化技术的方法基于故障模拟的方法基于故障 模 拟 的 方 法 是目前业界应用最广泛的可靠性 评 价 方 法 图 展示了这类方法的基本框架图 基于故障模拟的可靠性分析框架该 框 架 在 系 统 的 模 型 中 注 入 故 障然后在相同的基 准 测 试 输 入 下同时对注入故障后的 模型 和 原 来 的 模 型 进 行 模 拟 比 较两个模型每个周期的输出结果是否相同 经 过 若干个模拟周期之后 如果注入的故障仍然没有导致两个模型输出不匹配 那么说明故障仍然隐藏在电路中或者已经 被 掩 盖 了 这时就需要比较电路的状态元素如果状态元素不匹配 则 说 明 故 障 仍 然隐 藏 在 电 路 中 需 要 继 续 模 拟 实 验 结 束 后 被 分析组件发生软错误后导致系统失效的可能性就等于导致两个模型输出不匹配的故障注入数在故障注入总数中所占的比例故 障 注 入 的 关 键 在 于 如 何 在 目 标 系 统 中 模 仿故障错误 的 发 生 精 确 地 体 现 故 障 错 误 的 特 征例如故障错误的行为特征以及在时间空间上的分布特点 以便于可靠性评价结果能够准确地反映系统的可靠性 例如系统中最脆弱的组件 容错机制的有效性 等 等 具体的实现方式有很多种其中适用于在高层描述中注入故障的方式主要包含两类变 异 生 成 即 对 目 标 系 统通 常 是代码进行行为上 的 修 改 改 变 系 统 运 行 时行为 修改后得到的系统描述称为原有模型的一个变异结构上 的 修 改 即在原有系统中增加一个专门负责故障注入的模块 或者软件实现的 故 障 注 入 进 程 与第一种方式相比这种方式实现起来更加容易存在的问题及改进通常每注入一次故障就需要对整个系统进行大量的模拟模拟速度是这类方法的瓶颈 为了提高效率已有的方法主要从三个方面对基本框架进行了改进利 用 硬 件 仿 真 取 代 模 拟 这 类 方 法首先 将 系 统 的 模 型 综 合 到 然 后 利 用仿真快速 高 效 的 特 点 来 提 高 可 靠 性 分 析 的 效 率在基于仿 真 的 方 法 中 故 障 注 入 的 实 现 方 式 也 不同例 如附 加 故 障 注 入 器 即 修 改 系 统 的 高 层 描述增加专门的注入逻辑和用于控制故障注入的额外输入端然 后 与 系 统 的 描 述 一 起 综 合 到在仿真的过程中 通过控制附加逻辑的输入端就可以实现对硬 件 原 型 的 故 障 注 入 或 者 进 行 运行时 重 配 置 即在运行过程中对硬件原型进行部分重配置以实现故障注入 利用仿真取代模拟的好处在于一方面可以减少 了 实 验 所 需 的 时 间另 一 方 面 在实际应用环境下分析系统发生软错误后的行为变化比采用模拟方法得到的结果更精确 其缺点在于 代价昂贵 如果需要对实验运行时信息进行详细的分析例如分析故障传播路径 采用仿真的方法通常需要增加额外的初始输出才能观察到系统内部信 号 的 变 化 然 而 数 目 决 定 需 要 的 仿计算机工程与科学真器的大小因此增加初始输出将进一步增加仿真的代价 灵 活 性 差 需要对得到的内部信号进行复杂的后处理 因此基于仿真的方法灵活性不如基于模拟的方法统计故障注入 即基于一个随机选择的故障错 误 集 合 对 系 统 进 行 部 分 分 析以 实 现 故 障 的快速分类或者系统可靠性的快速估计 目前大多数的基于故障模拟的方法都采用统计故障注入的方式来实现 然 而如 何 确 定 待 注 入 的 故 障错 误集合包括故障 注 入 的 位 置 时间以及故障集合大小才能体现故 障 空 间 的 特 征并保证可靠性评价结果有 意 义 是 一 个 值 得 研 究 的 问 题 目 前除 了实验室 对 这 个 问 题 进 行 了 探 讨 之 外 这类方法对于故障 错误集合的选择都是任意的利用故 障 剪 枝 技 术 缩 小 问 题 空 间 减 少 模拟次数 这类方法的基本思想是在整个故障空间中故障在某些情况注入不会对系统产生影响例如当某个时序单元空闲时 即使发生故障也不会影响输出 避免在这些情况下注入故障既可以缩短实验时间 提 高 实 验 效 率 又不会影响可靠性分析结果 这类方法通常需要跟踪系统的模拟过程通 过 区 分 每 个 变 量 的 活 跃 时 间来判断故障注入的时机 然而在并行 体系结构的系统中 系统组件的操作并不一定都是有效的例如寄存器的操作经常都与最终结果的计算无关这就使得变量活跃时间的计算非常困难因此为 了 进 一 步 剪 枝 故 障 空 间 实 验 室 开发了一种 动 态 的 故 障 剪 枝 方 法 他 们 为 目 标 系统建 立 模 型以 追 踪 模 拟 有 用 数据和指令在寄存器中的传播 识别寄存器中数据真正有效的时间优点与缺点基于故障模拟方法的优点在于 它们对于可靠性分析的对象没有限制 而且原理简单直观易用不需要工程师预先理解系统的详细设计 缺 点 在于 不完备很难实现整个故障空间和输入空间的完全覆盖因此只能证明被分析的组件是不可靠的却不能证明它 们 是 可 靠 的 严 重 依 赖 于 测试基准程序的选择和故障注入 要合理而充分地注入故障以及选择测试向量 达到高覆盖率非常困难 虽然利用仿真取代模拟可以提高效率 但是由于仿 真 平 台 的 接 口 有 限 不 能 很 好 地 追踪运行时的系统 内 部 信 息 因 此很难对故障传播路径进行分析以确定电路中进行软错误保护的最佳位置 非常耗时 虽然各种对基本框架的改进都能够 在 一 定 程 度 上 减 少 分 析 所 需 的 时间但 是 能 够 带 来 的 好 处 都 比 较 有 限 例 如仿 真的速度极大程度上依赖于实验设置仿真平台与主机间的通讯带宽 因此采用仿真替换模拟对分析效率的提高有限 基于体系结构模型的故障剪枝方法应用对象受限 而 基 于 网 的 故 障 剪 枝 方 法又需要专门为可靠性分析建立新的 模 型而且分析结果依赖于模型的正确性无故障模拟的方法无 故 障 模 拟 的 方 法 专 门 针 对 处 理 器 等 大 型 体系结构类设计 的 系 统 级 可 靠 性 分 析 由 于 不 需 要进行故障注入而是直接采用体系结构时间模拟器或者性能模拟器对基准程序进行模拟通过分析各个系统组件的运行情况 例如占用率来估计它们发生软错误后导致系统失效的可能性因此被称为无故障模拟的 方 法 最 早 的 无 故 障 模 拟 方 法 是 由等 提 出 的 其 出 发 点 在 于 研究 发 现大 部 分 发 生 在 处 理 器 中 的 软 错 误并不会引发系 统 级 失 效 这主要是由于处理器的体系结构与微体系结构掩盖效应削弱了软错误对系统功能的影响 实验 表明发生在处理器 状 态位上的所有 软 错 误 中 大 于 都 可 能 被 体 系 结构级和微体系结构级的掩盖效应掩盖 因此为了量化体系结构和微体系结构掩盖因素等引入体系结构脆弱因子来表示某个 处 理 器 结 构 发 生 软错误后系统失效的可能性 因此无故障模拟方法也被称为 估计方法在基本的 估计方法 中根 据 发 生 软 错误后是否会造成系统级失效 处理器中的体系结构和微体系结构状态位被分为两类影响体系结构正确执 行 的 状 态 位 位和不影响体系 结 构 正 确 执 行 的 状 态位非 位 它 周 期 精 确 地 模 拟 处 理 器 体 系结构性能模型并 跟 踪 统 计 位 在 流 水 线 各 个结构中的驻留 时 间 或 者 操 作 时 间 某 个 处 理 器 结构的 就 等 于 该 结 构 中 驻 留操 作 位 的总时间在整个系统操作过程中所占的比例也就是说存 储 单 元 的 等于该单元保存 位 的总时间 所 占 的 比 例 功 能 单 元 的 等 于 处 理位的总时间所占的比例 该 方 法 可 以 用 于 处理器指令队列执行单 元数 据 存 储 单 元 以及存储缓冲等结构的 估计朱 丹 等 系统级软错误可靠性评价 综 述存在的问题及改进在 估计方法 中最 关 键 的 问 题 在 于 如 何区分 位与非 位 是否能够准确地识别位 关 系 到 分 析 结 果 的 精 度 基 本 的估计方法基于指令来识别 位即对每 条指令进行模拟并跟踪每个处理器结构对指令的操作情况然后找出模拟过程中不影响系统输出的指令例如动态死指令分支预测错误路径上的指令等这些指令流过的状态位都是非 位其 他的状态位 则 被 默 认 为 位 已有的基于指令的 位识别方法存在以下两个问题只 跟 踪 指 令 而 忽 略 了 数 据 因 此对 存 储数据的结构例 如寄 存 器 文 件 它并不区分其中的 位与 非 位而是将其中所有的状态位都默 认 为 位这将使得计算出的 大于实际的分析粒度太粗 只要某个处理器结构参与了指定类型指令 即 不 影 响 系 统 输 出 的 指 令的 操作基于指令的方法就会将其中的相关状态位都归为非 位然 而事实上某些状态位也可能导致系 统 失 效 应 该 为 位 例 如当 某 条 动 态死指令执行完毕后 该指令的目标寄存器号将会通过唤醒表 向指令窗口中那些正在等待该指令执行结果的指令进行广播通知它们该目标寄存器的 数 值 准 备 好 了 如果唤醒表发生软错误就会唤醒不应该唤醒的指令 引发死锁导致系统失效 因此唤醒表中与动态死指令相关的状态位也是 位针对以上两个问题 已有的方法进行了如下改进将流水线中流过的数据与指令统一看作数值基于数值来区 分 位 与 非 位 例 如等 构 建 的 估 计 框 架 该 框 架根据基本概率理论 为处理器中的软错误生成和错误传播过程建立概率分析模型 利用集成的体系结构时间模拟器或者性能模拟器 模拟跟踪处理器流水 线 中 流 过 的 指 令 数 据并 获 取 它 们 在 各 个 流 水线结构中参与读 写计算等操作的时间信息 最后根据错误概率以及时间信息 计算出每个结构对处理器系统级失效率的贡 献 以 及 平 均 失 效 时 间对每个处理器结构采用更细粒度的可靠性分析 例如 等 构 建 的 估 计 框 架该框架专门针对高性 能 乱 序 超 标 量 处 理 器进行可 靠 性 分 析 它 对 的 计 算 方 法 与 文 献相同不同 之 处 在 于 它对每个处理器结构采用更细 粒 度 的 分 析 仍然以指令窗口为例对唤醒表进行独立的分析 将唤醒表中每个状态位的操作分阶段讨论 根据状态位在每个阶段发生软错误后是否可能导致系统失效来确定它在哪些阶段为 位基本的 估 计 方 法 都 基 于 一 个 潜 在 的 假设即假设在任 意 情 况 下 处理器结构在任意时刻发生软错误导 致 系 统 级 失 效 的 可 能 性 都 相 同 然而大量研 究 表 明处理器及其结构的是与应用相关的 对于不同的应用 甚 至 同 一 应 用的不同运行阶 段 同一处理器中各个结构的以及同 一 处 理 器 的 都 存 在 很 大 的 差 异 因此仅仅根据基准测试程序的模拟分析结果来确定处 理器中各个结构的 而不考虑 与具体应用 之 间 的 关 系 的 估 计 方 法 统 称 为 离 线估计方 法 离 线 估 计 得 到 的 可靠性分析结果不能完全真实地反映实际应用中体系结构掩盖情况的变化 因此在实际应用中由离线方法指导部署的容错机制并不能很好地满足容错需求 为了解决这个问题 新的研究试图在处理器运行过程中动态估计每个处理器结构的以便于 更 好 地 指 导 容 错 这 类 动 态 估 计 方法也称为在线 估计方法目前已有的在 线 估 计 方 法 主 要 有 以 下两种一种是根据处理器结构的运行时利用率动态评估 例如根据运行时处理器结构的利用率动态评价 即 在 处 理 器 运 行 程 序 的 过 程中动态统计当前周 期 内 分 派 写 回确认以及撤离 的 指 令 数以 估 计 指 令 队 列 的实时占用 情 况 从 而 动 态 确 定 重 定 序 缓 冲 结 构 的二是基于统 计 学 的 方 法 例 如以 离 线 方 法为基 础通过对大量的应用程序进行离线 分析获取经验数 据 然后采用统计学中的回归分析技术 为 建 立 严 格 的 统 计 特 征 并 根 据 统 计 特征建立 预测 模 型 在 处 理 器 实 际 运 行 时 根据预测模型动态估计每个处理器结构的优点与缺点无故障模拟的方法的优点在于它们在体系结构级或者微体系结构级对可靠性展开分析而体系结构模型 一 般 在 处 理 器 设 计 初 期 就 已 经 构 建 因此与基于故障模拟的方法相比可 以 更 早 地 对 设计的可靠性进行分析 此外由于它们模拟的对象通常是体系结构模型 而不是包含了详细设计信息的 模型因 此 模 拟 速 度 更 快非 常 适 合 大 型计算机工程与科学系统的分析 再次由于它们只需要一次实验就可以得到所有处理器结构的可靠性分析结果因此比基于故障模拟的方法效率更高 缺 点 在 于 首 先不通用 它们以体系结构性能模 型为模拟分析对象因此不适用 于 非 体 系 结 构 类 设 计例 如 网 络 结点 其 次以 模 拟 作 为 核 心 技 术 因 此 仍 然 受 模 拟技术本身缺点的限制 例如不完备最后以体系结构模型为 对 象 而这类模型不包含系统的实现细节因此只能量化体系结构与微体系结构级掩盖效应对软错误的影响 而不能量化逻辑掩盖效应基于形式化技术的方法由于 软 错 误 具 有 多 维 不 确 定 性 即 使 选 择错误模 型 作 为 研 究 对 象基于故障注入的方法也很难穷尽 整 个 问 题 空 间 而基于无故障模拟的方法虽然不需要进行故障注入但是也需要模拟大量应用程序才能得到有意义的分析结果然而在可接受的时间内 能够模拟的程序总是有限的 因此以上两类基于模拟的可靠性分析方法都是不完备的 形式化技术的应用范围非常广泛几乎涵盖了软硬件设计整个生命周期中各个阶段的模型分析与验证 它 们 采 用 严 格 的 数 学 方 法 完 备 地 证明系统的功能是否满足设计者的意图是模拟方法的有效补充 因此自从 将形式化技术引入到可靠性分析领域之后 基于形式化技术的系统级软错误可靠性评价方法就成为了该领域的研究热点基 于 形 式 化 技 术 的 可 靠 性 分 析 方 法 通 常 从 目标系统的原始设计中提取形式化模型通常是有限自动状态机 并采用形式化语义描述故障模型然后通过两个模型的乘积实现故障注入最后利用形式化技术验证系统的某些可靠性属性在注入故障后的系统模型中是否仍然保持 从基本原理上来说基于形式化技术的方法所采用的故障注入方式与基于故障模拟的方法所采用的故障注入方式类似也分为行为上 的 修 改 和 结 构 上 的 修 改 即 附 加一个专门的故障注入模块 两种行为上的修改 使用特定的形式化语义描述故障特征 与 执 行 规 则例 如谓 词 符 号 执 行规则 属 性 描 述 以 及 非 确 定 性 有 限 状 态机 大多数基于形式化技 术 的 方 法 所 采 用 的 故障注入方式都属于行为上的修改结构上 的 修 改 即增加专门的故障注入模块例如采用 专 门 的 拓 展 程 序 即 故 障 注入模块来 实 现 故 障 注 入 具 体 的 注 入 点 由 故障向量控制 故障向量中的位与电路中的锁存器一一对应当某一 位 为 时表 示 向 该 位 对 应 的 锁存器注入故障 多位同时为 时表示需要注入多位故障针对不同的可靠性分析目标已有的研究选择不同的形式化验证技术进行可靠性分析符号模拟 符号模拟与传统模拟的原理相同不同之处在于它利用布尔变量取代基准测试集中的布尔常量能够在一个模拟周期内完成传统模拟多个周期才能完成的分析 同时保证了完备的覆盖率 因此文献 利用符号模拟取代图 框架中的传统模拟技术 这是将形式化技术引入可靠性分析领域最直接的方法 其目的是确定电路中错误检测与校正逻辑的容错能力模型检验 模型检验从原始设计中提取有限状态机将待验证的属性用时态逻辑描述然后遍历有限状态机以检验属性是否存在 目前采用模型检验进行可靠性分析的方法分为两种 以原始设计的有限状态机模型作为故障注入对象 然后利用模型检验验证设计者关心的属性在注入故障后的有限状态机 中 是 否 保 持 例 如文 献 在 设计早期采用模型检验识别错误检测和校正逻辑是否对 有效 文 献 依次在每个锁存器中注入 错 误并 利 用 模 型 检 验 工 具 验 证注入故障后的系统有限状态机模型是否仍然满足原有的设计属性 以识别时序电路中必须进行软错误保护的关键 锁 存 器 以系统的设计属性作为故障注入的对象 采用这 种 方 式 的 优 点 在 于 故障注入不需要修改系统的设计模型等价性检查 等价性检查采用自动机理论与数学逻辑的方法来形式化地证明同一设计的两种不同表示可相互替换 而不会影响全局设计的正确性 文献 将注入故障后的电路模型与原电路按周期展开采 用 基 于 的 时 序 等 价 性 检 查技术判断电路中任意组件发生软错误后是否影响电路输出并根据验证结果将电路中的组件细分为可靠的不可靠的以及未分类的三种然 后 根 据 各类组件所占的比例来确定电路的可靠性上下界定理证明 基于定理证明的可靠性分析方法只需要将故障模型和原始设计的模型都表示为形式 逻 辑 的 命 题 谓 词定 理推 理 规 则 等 并 将 待验证的属性表 示 为 定 理 然后在验证者的引导下不断对公理和已证明的定理施加推理规则得到新的定理直至推导出要证明的定理 例如文献朱 丹 等 系统级软错误可靠性评价 综 述利用定理证明器 来验证数字系统设计的容错能力存在的问题及改进目前各种常用的形式化验证技术都被初步地应用到了系统级可靠性分析当中虽然与基于模拟的方法相比这类方法可以提供更加完备的可靠性分析但是还存在若干待解决的问题受限于形式化技术的问题可处理规模除了基于定理证 明 的 方 法 之 外大 多 数已有的方法都对系统中每个组件发生软错误的情况进行枚举然后应用相同的过程来分析每一个组件发生软错误后对系统功能的影响 虽 然 基 于 形式化技术的方法只需要一次分析就可以得到基于模拟的方法需要对大量测试程序进行模拟才能得到的结果但是 从 原 理 来 说 这种好处是形式化验证以遍历状态空间的复杂度来换取的 因此对每个组件发生软错误的情况进行枚举实质上就是按照组件来分解系统状态空间 然后依次对与每个组件相关的状态子空间进行遍历 然而按照组件来划分状态空间并不是一种好的分解方式它将导致大量状态空间的重复遍历 从而降低可靠性分析的效率大多数已有的方法都基于相同的基本思路即利用形式化技术来判断在发生软错误后 设计属性是否能够保持 而不能进一步对属性保持或者被违反的可能性进行量化分析 因此这些方法只能用于区分每个组件是否可靠以及容错设计是否有效最多给出部分导致容错机制失效的反例对于不可靠的组件以及容错设计不完全有效的情况它们并不能为使用者提供更多的指导例如哪些不可靠组件更脆弱 故障检测逻辑在哪些情况下会失效等等为了减少计算时间 提高问题可处理规模已有的方法也引入了各种优化技术例 如层 次 化分解 部 分 可 达 技 术 子 句 重 用 等 虽 然这类方法无法处理规模较大的复杂系统但是可以为系统中的关键模块提供完备的可靠性分析上 面 的 第 二 个 问 题 是 由 于 问 题 分 析 角 度 不 同造成的 从 可 靠 性 分 析 的 角 度 来 看 枚 举 每 个 组件分析它们发生软错误后对系统产生的影响是一种很自然的方式 然而从状态空间的角度来看由于电路中的组件相互关联 因此与每个组件相关的状态子空间之间必然存在大量交集而可靠性分析在枚举每个组件的过程中必然会重复多次遍历交集部分的状 态 电 路 规 模 越 大 包含的组件越多状态空间中每个状态被重复遍历的次数也就越多这将极大地降低可靠性分析效率限制问题可处理规模 为了提 高 效 率 我们考虑一种折衷的方法即根据组件间的相互关联对组件进行分组然后将可靠性分析分 为 全 局 和 局 部 分 析 两 个 部 分 在 全局分析过程中以组为单位进行枚举 分 析 每 组 中任意组件发生软错误的情况 然后再在每一组内进行局部分析这样既减少了状态空间的重复遍历次数同时又保持可靠性分析过程的自然合理性优点与缺点基 于 形 式 化 技 术 的 可 靠 性 分 析 方 法 主 要 的 优点在于其完备性 它们可以断定系统中每个组件的可靠性也可以判断容错逻辑的有效性 主要的缺点是受限于形式化验证技术本身存在的问题形式化验证需要从原始设计中抽取模型以模型为对象展开分析 模型抽取过程本身是一个很复杂的转换过程保证抽取无误是比较困难的而 且 模型抽取的精细程度也将影响可靠性分析结果软错误的多维不确定性将导致形式化分析的状态空间爆炸问题将更加严重目前基于形式化技术的方法并不能取代前两类方法而是它们的有效补充

结束语

软 错 误 系 统 级 可 靠 性 分 析 在 设 计 的 早 期 为 设计者提供可靠性方面的量化分析结果指导容错设计尽早地 展 开 有 助 于 平 衡 可 靠 性 需 求 与 容 错 开销降 低 设 计 返 工 的 成 本 缩 短 上 市 时 间 按 照 各种方法所采用的核心技术 本文将已有的方法分为基于故障模拟的方法 基于无故障模拟的方法以及基于形式化技 术 的 方 法 三 类 这 三 类 方 法 各 有 优势互 为 补 充 目 前学 术 界 对 于 这 三 类 方 法 的 研究已经逐渐形成了若干个新的子方向未来的研究将主要集中在以下几个方面

    与 非 位 的 区 分 在 处 理 器 运 行过程中状 态 位 的 角 色 是 在 和 非 之 间不断转换的 要 精 确 地 计 算 需 要 能 够 精 确追踪状态位变化情况的新技术

    无故障模拟的方法的通用化无 故 障 模 拟方法仅适用于处理器的可靠性分析的主要原因在于它们采用体系结构性能或者时间模型为对象展开分析 然而随着设计工艺的进步非处理器类设计的结构也日趋复杂 基于无故障模拟的方法的通用化是一个值得研究的新方向计算机工程与科学

    动态可靠性评估 结合应用特点精确地分析系统运行过程中组件软错误脆弱度的变化有效指导软错误保护机制的动态自适应将极大地降低功 耗提 升 系 统 性 能 目 前学 术 界 对 于 动 态 可 靠性评估方法的研究才刚刚起步 需要进一步深入

    针对可 靠 性 分 析 特 点 提高形式化技术的问题处理规模基于形式化技术的软错误可靠性评价是一个新兴的研究领域 目前已有的工作只是将各种形式化技术初步应用到该领域虽然也有少数研究做了优化但是这些优化技术都是从形式化验证领域直接引入的 并不是专门针对可靠性分析特点而提出的不能有效地解决形式化技术在可靠性分析领域应用中遇到的新问题例 如本 文 分 析 过的状态空间的 重 复 遍 历 问 题 专门针对该领域应用特点对形式化验证过程进行优化将成为该领域的研究热点

    参考文献 朱 丹 等 系统级软错误可靠性评价 综 述附中文参考文献唐 明张 国 平张 焕 国基于汉明纠错编码的 硬 件容 错 设 计 与 实 现 电 子 学 报作者简介朱 丹 女重 庆 人博 士 生研究方向为集成电路 硬 件 形 式 化 验 证和 自 动 向 量 测 试 生 成计算机工程与科学