ISO 26262 规定，需要硬件架构指标来评估安全机制的充分性，以及它们检测和 / 或防止故障到达安全关键区域的能力。故障注入是确定安全机制在满足功能安全要求方面的完整性和正确性的基本方法。然而，随机故障注入耗时且效率低下，难以满足当今的产品发布周期。在本文中，我们提出了一个静态分析步骤，以提高故障注入的效率。此外，一种形式化方法被用于故障注入，以最大限度地提高安全故障的可观测性。

汽车安全标准 ISO 26262规定，对硬件设计的安全分析应包括失效模式与影响分析（FMEA）。需要硬件架构指标来评估安全机制的充分性，以及它们防止故障到达安全关键区域的能力。一个包含故障注入的失效分析过程，对于衡量和验证 FMEA 的假设至关重要。

在 ISO 26262 规范的第 5 部分中，硬件架构需要根据故障处理的要求进行评估。它要求通过一组客观指标对随机硬件故障的概率进行严格分析和量化。如果任何架构指标未能满足为产品的汽车安全完整性等级（ASIL）定义的标准，则必须重新评估组件安全概念、改进现有安全机制和 / 或引入新的安全机制。失效分析是一个旨在确定转化为影响硬件安全要求的故障所占百分比的过程。它在不同级别使用带有设计表示的故障注入，来计算和验证故障模式和诊断覆盖率的值。因此，故障注入是确定安全机制在满足硬件安全要求方面的完整性和正确性的基本方法。

传统上，故障注入包括在门级表示上运行功能仿真，在某个时间点翻转一个位，然后分析结果，看是否有任何被定义为安全关键的信号（如输出端口、状态机）发生了任何变化。要确定会转化为失效的失效百分比，需要在数百次测试中注入数万个故障，对它们进行仿真直至输出，并比较结果。然而，门级设计表示仅在设计周期的后期可用。在那个阶段，任何概念上的重新评估和 / 或架构上的更改都将对项目进度产生重大影响，并且执行成本高昂。因此，在寄存器传输级甚至事务级进行故障注入，是在设计周期早期进行失效分析和评估安全机制效率的重要替代方案。

即使在更高的抽象级别，随机故障注入仍然耗时且效率低下，难以满足当今的项目进度。硬件仿真或设计原型设计有助于解决基于仿真的失效分析中的性能瓶颈。然而，这些方法效率低下，因为注入的故障可能不会导致任何安全目标的失效（安全故障），或者故障可能被安全机制阻止。为了提高效率，我们希望关注那些不受任何安全机制保护并随后会导致安全目标失效的故障（单点故障、残余故障）。

这些因素促使我们采用形式化验证进行失效分析。在本文中，我们提出了一个静态分析步骤，以推导、优化和确定故障列表的优先级，以便能够尽可能高效地对其进行分析。此外，一种形式化方法被用于故障注入，以最大限度地提高故障结果的可观测性。

我们希望提高任何故障注入机制的效率。为此，提前进行静态分析，以确定应注入故障的关键设计元素集。同时，我们可以移除对安全机制不重要的设计元素。我们称这个过程为故障修剪。主要目标是跳过不会影响安全要求的元素，将故障注入集中在会影响安全要求的元素上。

A. 基于安全目标的故障修剪

作为 ISO 26262 安全分析的一部分，并基于安全要求，工程师为设计定义安全目标和安全关键元素。形式化工具能够从安全目标通过设计元素回溯，以确定影响锥（COI）中的内容，如图 1 所示。

图 1：形式化工具回溯影响锥以执行其分析

故障修剪过程的步骤可以总结为：

1. 识别设计中一组会对安全目标产生直接影响的安全关键元素。这些包括输出端口、状态机、计数器、配置 / 状态寄存器、FIFO 以及其他用户指定的元素。

2. 为模块创建约束列表。例如，调试模式、测试模式以及在特定实例中未使用的操作模式等。然而，为了使这组约束有效，这些约束必须有独立的安全机制。例如，每当设计发现这些模式处于活动状态时，就会生成一个错误标志。通常这些模式是全局的，其安全机制在更高层次上处理。

3. 计算这些安全关键元素的影响锥（COI），并基于这些扇入锥中的元素创建故障注入列表。不在影响锥中的设计元素被认为是安全的，不需要考虑。

4. 应用形式化技术来验证，注入这些元素中的故障将被观察到，并将影响安全目标和 / 或安全关键元素。

B. 基于安全目标和安全机制的故障修剪

下一步是查看安全要求的影响锥中的哪些设计元素与安全检测机制的影响锥重叠。例如，假设存储和传输单元的数据完整性被视为安全关键。如图 2 所示，每个数据包都带有用于检测任何错误的纠错码（ECC）位。只要 ECC 位能够标记任何瞬态故障，数据输出就会受到保护，因为错误可以在下游被检测和处理。然而，在双点故障情况下，错误也可能影响 ECC 检测逻辑。结果，安全机制无法检测到数据包中的坏数据。在这种情况下，安全机制中的第一个故障被视为掩盖条件，因此是潜在故障。双点故障场景中的第二个故障是一个实际错误，如果不是因为潜在故障，安全机制本可以检测到，从而导致双点故障。

图 2：检测逻辑影响锥之外的任何东西都被认为是潜在不安全的

此外，并非所有设计元素都在安全机制的影响锥内。在数据输出的影响锥内但不在 ECC 逻辑的影响锥内的设计元素，将不受安全机制的保护，因此必须被视为潜在不安全的。这些设计元素中的故障被视为不可检测的或潜在不安全的。因此，我们有：

1. 设计元素（在 ECC 的影响锥内），其故障可能被安全机制检测到（安全故障、残余故障或双点故障）

2. 设计元素（在 ECC 的影响锥外），其故障无法被安全机制检测到，且潜在不安全（残余故障）

由于能够测量这两个影响锥，改进设计（强化）的机会变得明显。两个锥的 “不可检测” 部分越大，意味着可能导致残余故障的元素比例越高，满足高 ASIL 等级的能力就会显著降低。此时，设计团队的目标是确定如何使安全关键功能和安全机制产生更多重叠。

一旦故障列表中的设计元素数量被修剪为高质量且有意义的子集，就可以将其传递给各种故障注入机制；例如故障仿真、硬件加速故障仿真、形式化故障验证和硬件原型设计。尽管基于仿真的故障注入方法，如软件和硬件加速故障仿真很常见，但它们已知效率低下。

A. 基于形式化的故障注入

尽管大多数仿真回归环境提供高功能覆盖率，但它们在将故障传播到输出端口方面表现不佳，并且功能检查不足以检测所有类型的故障。我们创建回归环境是为了验证功能规范，即设计的正向行为。它不是为了测试负向行为而设计的。我们对基于形式化的故障注入感兴趣，主要是因为这两个特性。

1. 故障传播：例如，一个随机故障被注入到 FIFO 寄存器中，导致其内容损坏。由于仿真环境没有反应性，该故障可能会被随后推入 FIFO 的数据覆盖。形式化验证则不同；它智能地注入故障。它善于引入它知道如何传播以影响设计的安全目标或输出的故障。

2. 故障检测：例如，即使损坏的 FIFO 内容已被读取，故障也可能未被检测到。FIFO 内容可能会被丢弃，因为功能仿真不在处理数据的模式下。大多数功能仿真测试规范中定义的场景，而故障检测需要一致地测试所有可能出错的场景（负向行为）。为了检查所有潜在的负向场景，我们依赖于形式化时序等价性检查。

B. 具有时序逻辑等价性检查的故障注入

形式化时序等价性检查（FSEC）比较两个设计或同一设计的两种表示的输出。只要输出始终相同，两个设计的实现可以不同。例如，FSEC 可用于比较已移植到 Verilog 的 VHDL 设计（或反之亦然），以查看两个 RTL 设计在功能上是否等价。从概念上讲，FSEC 工具是一种形式化工具，其中实例化了两个设计，约束输入相同，并使用断言指定输出对于所有可能的内部状态都应等价。

图 3：具有时序逻辑等价性检查的故障注入

虽然 FSEC 有许多用途，但故障注入是一个特别的优势所在。形式化工具能够将固定型和瞬态故障注入设计中，使故障通过设计的状态空间计时，并查看故障是被传播、掩盖还是被安全机制检测到。一旦注入故障，形式化工具会测试所有可能的输入组合，以将故障通过设计传播到安全机制 —— 这正是 FSEC 的用武之地。

如图 3 所示，使用黄金（无故障）模型和注入故障的模型来执行动态故障注入和结果分析。在没有完整的功能回归的设计周期早期，使用形式化 FSEC 进行故障注入非常方便。它可用于执行 FMEA并确定安全机制是否足够。设计师可以在 RTL 阶段快速试验和权衡不同的安全方法 —— 包括错误检测、纠错、冗余机制、寄存器强化等。

通过用自身的副本实例化一个设计，FSEC 会自动指定所有合法的输入值，就像仿真中的黄金参考模型预测任何输入激励的所有预期输出一样。唯一可能的输入是那些能够通过参考设计合法传播到相应输出的值。通过比较注入故障的设计与其无故障的副本，形式化工具检查是否存在任何可能的方式，使故障要么逃逸到输出，要么未被安全机制检测到。

使用 FSEC 进行故障注入的步骤可以总结为：

1. 为 FSEC 指定原始设计的两个副本。输入端口将被一起约束，输出比较将自动检查。

2. 运行 FSEC 以识别任何设计元素 —— 如内存黑盒、未连接的导线、不可复位的寄存器等 —— 这些元素会导致输出不同。添加约束以同步它们。

3. 使用故障列表自动指定故障设计中可能的注入点。通常，我们将重点放在单点故障上；即，注入一个故障以检查等价性。

4. 基于故障列表和比较点，FSEC 将自动识别并移除任何冗余块和逻辑。

5. 我们在多个服务器上并发运行 FSEC。多核方法具有显著的性能优势，因为可以在多个核上同时检查多个输出。

6. 我们使用一种技术在一次运行中编译所有故障，从而节省通常需要逐个编译故障的时间和空间资源。

7. 我们还在一次运行中执行数千个故障的 FSEC 验证步骤。

8. 如果注入的故障在比较点导致失效，可以生成一个捕获故障注入和传播序列的反例波形用于调试。

我们构建了一个用于形式化故障修剪和使用 FSEC 进行故障注入的环境，总结如图4所示。故障修剪步骤构建设计的网表表示。基于安全目标（可能只是输出端口）和安全机制，然后使用形式化方法来计算和检查影响锥。报告安全和不可达故障。使用 Questa® 形式化验证工具进行带有 FSEC 的故障注入。在运行故障注入之前，用户可以使用故障建模和约束来控制要注入的故障的位置和类型。此外，用户可以对设计进行分区，或配置工具在多核服务器集群环境中执行注入运行。

图4：故障修剪和注入环境

A. 形式化故障修剪的结果

案例 1：该设计是一个浮点单元，约有 530K 个门。目标是识别设计中的安全故障。这些故障在影响锥之外，或者无论输入激励如何都无法传播到功能输出。原始故障列表包含约 32K 个故障。经过编译和设置后，其中 868 个被识别为安全故障。有趣的是，由于操作模式，其中 690 个无法传播，不会影响设计的输出。

案例 2：该设计是一个内存管理单元，约有 1.3M 个门。目标是识别可以传播到内部状态寄存器的故障。这些寄存器由更高层次的安全机制检查。因此，这些可检测的故障可以被认为是安全的。在该设计中，有 71 个状态寄存器和目标故障列表中的 1524 个故障。经过编译和设置后，在一小时内有 720 个被识别为安全故障。

B. 形式化故障注入的结果

案例 1：该设计是一个时钟控制器模块，采用三重模块化冗余（TMR）实现安全机制。TMR 是一种昂贵但 robust 的动态安全机制。为了快速初步测试，允许将故障注入设计中的所有寄存器（案例 1a）。由于所有寄存器都在安全机制的影响锥内，因此不足为奇。形式化故障注入验证所有注入的故障都将被安全机制捕获。接下来，允许将故障注入设计中的所有节点（寄存器、门和导线）；故障数量明显更多（案例 1b）。同样，形式化故障注入验证所有注入的单点故障都将受到安全机制的保护。

案例 2：该设计是一个桥控制器，包含案例 1 中的时钟控制器模块。在这种情况下，形式化故障注入能够将一些故障注入并传播到设计的输出端口。观察到两种类型的故障场景：

· 不受任何安全机制保护的单点故障

· 受安全机制保护的残余故障；然而，安全机制未能正确检测到错误情况。

图5显示了案例 2 中的一个场景，其中注入的故障未被安全机制检测到，并违反了安全目标。在复位解除后不久注入了一个随机故障。该故障在设计中导致了多个错误，这些错误在五个时钟周期后到达设计的输出。不幸的是，安全机制未能检测到这些错误。结果，该故障导致了安全目标的违反。

图5：显示故障如何传播到安全机制外部的波形

在本文中，我们讨论了形式化故障修剪和使用形式化时序等价性检查的故障注入。通过利用形式化技术，我们可以通过识别不可达的设计元素、影响锥（COI）之外的元素，或者不影响输出（或被安全机制门控）的元素，来确定安全故障的数量。故障修剪后，优化后的故障列表可用于通过各种机制进行故障注入；例如故障仿真、硬件加速故障仿真、形式化故障验证和硬件原型设计。基于仿真的故障注入在将故障传播到输出端口方面效率不高，并且传统的功能检查不足以检测所有类型的故障。对于仿真，永远不知道设计是否被充分仿真或是否给予了足够的输入场景。形式化验证可以确定性地确定故障是否安全，使得形式化分析的故障率比故障仿真更全面。