这不是我的错！如何使用形式验证更好地执行故障注入分析和仿真任务

ISO 26262 汽车安全标准

要求评估由于随机硬件故障引起的安全目标违背，以确定用于计算安全指标的诊断覆盖率 (DC)。 使用仿真注入故障可能非常耗时、繁琐，而且在某些情况下无法激活设计来传播所测试的故障。但有了形式验证，则可以按结构分析轻松地对故障进行分类，从而提供最坏情况下的 DC。此外，还可通过分析故障来验证传播、安全目标违背和故障检测，提供准确和高可信度的结果。本文详细介绍如何使用形式验证更好地执行故障注入分析和仿真任务。

ISO 指标

汽车功能安全标准 ISO 26262 定义了适用于汽车应用集成电路的两项验证要求 — 系统性失效验证和随机硬件失效验证。系统性失效是指使用常规的功能验证发现的设计缺陷。随机硬件失效验证是指将故障注入设计，以测试关于设计安全机制的假设，看看它们能否正常工作。同功能验证使用覆盖率来确定完成度一样，ISO 标准也定义了一种种类的随机硬件失效覆盖率，它被称为诊断覆盖率，表示了被安全机制覆盖的安全元素所占的百分比。 计算诊断覆盖率需要首先确定设计中不同故障类型的数量。如果注入故障并且对安全关键型目标（功能）或输出没有影响，则该故障被认为是安全的。同样地，任何注入的故障如果可以被检测到或通知汽车司机，则也被认为是安全的。我们真正需要寻找的是那些未受任何安全机制保护的故障（称为 “单点故障” ），或预期已覆盖但安全机制未能检测到的故障（称为 “残余故障” ）。该 ISO 标准还介绍了安全机制中的潜在故障。通常，汽车设计具有诸如 POST 之类的辅助安全机制，用于检查主要安全机制的行为。为了测试安全机制是否正确，必须向设计中注入故障，以激活主要安全机制，然后再将第二个故障注入主要安全机制，看看其是否仍能正常工作。这被称为双点故障，可归入多点故障类别（但除非由于架构原因需要增加测试，否则此标准只要求测试最多 2 个故障）。辅助安全机制未覆盖的任何双点故障都被视为潜在故障。

一旦设计中的所有故障都已分类，便可以轻松计算 ISO 26262 指标。通常，故障数会在 FMEDA [1] 中汇总到一起，以计算单点故障指标 (SPFM) 或潜在故障指标 (LFM)。或者，也可以按百分比计算诊断覆盖率，然后在 FMEDA 中与特定失效模式的工艺 FIT [2] 率 (λFIT) 结合使用 [3]。（参见 [1]，C.1-C.3 部分，了解有关 ISO 指标计算的详细信息）