内容提要：在本文中，我们提出了一种需要最少用户输入的双模形式故障传播分析（FPA）方法。我们展示了这种实用的方法如何补充基于仿真的故障分析，以提供改进的ISO 26262指标，同时节省工程工作量和仿真周期。

摘要

现代汽车片上系统(SoC)实现了众多安全关键功能。随机硬件故障，例如单事件闩锁，可能会导致电路行为错误，并最终导致危险的系统失效。安全机制可以减少失效的发生，但遵守ISO 26262需要对其有效性进行定量分析。形式化验证工具可以准确地在硬件模型中注入故障并严格分析其传播。然而，对于存在大量潜在故障的复杂汽车硬件来说，可扩展性和可用性具有挑战性。在本文中，我们提出了一种需要最少用户输入的双模形式故障传播分析（FPA）方法。我们展示了这种实用的方法如何补充基于仿真的故障分析，以提供改进的ISO 26262指标，同时节省工程工作量和仿真周期。此外，我们证明通过这种方法，形式化的FPA可以成功应用于现代汽车SoC。

一、简介

功能安全标准规范了许多工业领域的安全关键系统的开发，并包括对硬件组件的要求。ISO 26262是汽车行业的功能安全标准，适用于道路车辆中与安全相关的电气和电子 (E/E) 系统。汽车硬件必须满足对可能危及安全关键功能的随机硬件故障比例的严格期望。硬件和软件安全机制可以检测异常电路行为并预防或控制危险失效。安全机制是满足ISO 26262要求的关键，而故障仿真是提供证据的主要方法，证明只有一小部分故障可能会传播到安全关键功能而不被检测到。

A. 相关工作

形式化方法被广泛认为是发现设计错误和执行严格有效的功能验证的强大技术。形式化工具在汽车硬件功能验证中的应用在业界已经很成熟了。

形式化工具的另一个重要特征，特别是与安全关键型应用相关的特征，是能够精细控制故障注入并详尽分析其顺序影响。至关重要的是，就用户工作量和计算需求而言，形式化工具有可能非常有效地执行此任务，并且是非侵入性（不需要代码检测步骤）。（参考资料1，关注牛喀网公众号，后台咨询下载参考资料）中介绍了应用于汽车硬件的基于形式的故障注入和分析方法。

这些应用程序主要针对寄存器传输级（RTL）硬件模型的验证，并且需要对被测设计（DUT）有深入了解的专家用户提供大量输入。

B. 贡献

在本文中，我们提出了一种专门针对故障度量计算的形式化工具的应用。该方法需要最少的用户输入，适用于RTL和门级硬件模型，并可扩展到需要分析数百万个故障的大型设计。我们提出了一种双模式方法，在每种模式中，我们应用专用的形式算法来实现不同的中间目标。第一种模式称为快速故障传播分析(FPA)，针对大量故障群体，旨在为大多数检查的故障提供可用的结果。第二种模式称为深度FPA，使用针对难以分析的故障的形式化算法，因此仅适用于有限大小的断层群。在第二节中，我们设置了这项工作的背景，并介绍了符合ISO 26262的基本概念和术语。在第三节中介绍了两种FPA模式后，我们在第四节中展示了这种方法如何与基于仿真的故障分析相结合。在第五节中，我们报告了在RTL和门级设计上运行两种FPA模式所获得的结果。第六节总结了本文。

二、基本概念

A. 故障、错误和失效

当系统中的某个元素不再能够执行其所需的功能时，就会发生失效。失效是由错误引起的，例如硬件组件的输出不具有其指定值。错误是由故障引起的，例如DRAM内存被宇宙射线损坏。请注意，系统内某个层次结构级别的故障可能会成为下一个级别的故障：硬件组件的失效可能会被视为车辆级别的故障。ISO 26262定义了两类失效：系统失效和随机失效（见图1）。系统失效与某些原因或故障具有确定性关系，例如规范错误、软件或RTL中的编码错误，甚至制造缺陷。在硬件元件的使用寿命期间，随机硬件失效会按照概率分布不可预测地发生：例如由自然辐射或磨损引起的失效。

图1. 故障、错误和失效之间的关系

B.随机硬件故障

随机硬件故障可以根据其持续时间进行分类：永久性故障，例如由于磨损、间歇性故障和瞬态故障，网络永久停留在逻辑值0。单偶翻转(SEU)和单事件瞬态(SET)是瞬态故障。SEU的典型示例是DRAM存储器中由于自然辐射导致的位翻转。SET和SEU故障会导致软错误，因为与硬错误不同，不会对硬件造成永久性损坏。然而，值得注意的是，瞬时故障可能是潜在的且长期持续的。

C.安全机制和ISO 26262指标

ISO 26262规定使用检测随机故障的硬件和软件安全机制，以防止或控制硬件失效。现代汽车SoC可能包括各种软件和硬件安全机制（见图2），具体取决于其目标应用和相关的安全完整性级别。软件安全机制可以通过自检例程来实现，在系统加电时甚至在操作期间运行。另一方面，硬件安全机制通常涉及某种形式的冗余逻辑，负责检测并可能纠正错误，并向SoC中的其他模块报告，例如向安全管理单元（SMU）报告。

图2.安全机制示例

ISO 26262要求对安全机制的有效性进行定量分析，其中必须考虑安全逻辑本身发生的故障。例如，损害安全逻辑的错误检测和纠正能力的故障，可能不会被检测到并保持潜在状态。当另一个故障发生时，潜在故障的有害影响最终可能会变得明显。图3中定义的单点故障、残余故障和潜在故障对安全构成威胁，必须尽量减少。例如，对于ASIL D应用，工程师可能必须证明单点故障的比例低于1%。

图3. ISO 26262中的故障分类

D. 故障注入和故障分析

故障注入是一种成熟的技术，用于了解故障对容错系统的影响。ISO 26262强烈建议将故障注入作为一种方法，在硬件、软件和安全过程中根据安全要求验证安全机制的完整性和正确性。在分析RTL和门级设计时，验证环境应能够注入故障，并跟踪它们如何在设计中传播。主要挑战是实现一个易于使用和可扩展的环境，该环境能够快速提供证据证明设计实现了预期的故障覆盖目标，或者明确指出缺点。

故障仿真作为故障注入和分析的方法已得到广泛采用。仿真确实可以扩展到大型设计，但是，即使对于小型设计，它也无法详尽无遗，因此无法证明故障永远不会传播到关键设计的输出或寄存器。即使在使用大量且巧妙构造的输入激励集，新的测试总是有可能显示出完全相同的故障，从而导致危险的失效。此外，工程师可能必须检查数百万个故障，这对于仿真来说是不可行的。典型的解决方法是检查故障样本并为故障覆盖率指标提供统计证据。

三、形式化的故障传播分析

大多数用于基于断言的验证的形式化工具都经过了优化，可以在RTL模型上工作。现代工具可以对设计进行结构分析，包括对信号和断言的影响锥分析，让应用程序自动生成特定任务的断言，并依赖大量的证明引擎和策略，用户可以调整这些引擎和策略来减少证明运行时间，或将转向不确定的结果分为通过或失败。另一方面，用于综合验证的形式等效性检查工具通常应用于大型门级网表。近年来，顺序等价检查算法补充了传统的组合等价检查，使得高级综合优化的验证成为可能，包括在FPGA流程中。所有这些方法都可以在形式化的FPA中发挥作用。

将形式技术应用于故障传播分析需要将故障注入硬件模型并设置证明问题，以评估损坏设计中的一个或多个信号（通常称为观察点或安全关键信号）与原始无故障设计相比是否具有不同的功能行为。此外，如果故障影响观察点，了解故障检测信号是否被激活可能很重要。形式验证相对于仿真的一个关键优势是它不需要输入向量。形式分析相当于检查所有输入序列，使工程师能够提供严格的证据证明某个故障是安全的。

理想情况下，不了解形式化方法的工程师应该能够在任意复杂度的任何RTL或网表设计上应用相同的按钮形式化流程，并快速找到所有安全故障。在实践中，由于复杂性问题，这是不可能的，工程师可能必须根据设计和所分析的故障集，明确选择方法和证明策略。我们在本文中提出的务实方法包括定义两种形式化的FPA模式：快速和深度，针对两种通用应用场景。主要目标是通过两种高度自动化的解决方案实现最佳计算性能，涵盖先进汽车SoC开发的所有应用场景。

A. 快速模式

快速FPA模式需要输入观测点列表以及RTL或门级设计模型，并针对大量故障群体。检查整个故障群体的运行时间可能从几分钟到几个小时不等，对于复杂的情况，过夜运行是可接受的设计。在快速模式下，形式化工具应自动选择适当的证明方法和策略来发现大多数安全故障，同时尽快中止对难以证明的故障的分析，从而最大限度地减少在不确定结果上花费的精力。为了简化任务，可以删除可传播故障的调试信息的生成。

B. 深度模式

深度FPA模式需要输入观察点列表和一小部分故障列表。该模式中使用的方法和算法应针对难以证明的故障，并为已证明传播到观察点的故障生成详细的调试信息。每个故障可接受的运行时间范围可以从几秒到几小时不等。在深度模式下，还可以利用设计知识来实现性能改进。例如，对于具有长初始化序列的设计，用户可能会受益于在设计初始化后开始形式分析，这是大多数现代形式化工具都提供的功能。

四、与仿真集成

上一节中概述的两种模式形式化FPA方法的一个主要优点是它与故障模拟流程集成，提高了结果质量(QoR)和生产力。在仿真之前，工程师可以在整个故障群体上以快速模式运行形式化的FPA（见图4）。被证明安全的故障会立即影响故障覆盖率指标，不需要在仿真中进一步分析。然后将故障仿真应用于减少的故障数量，为将大多数故障分类为已检测故障和可传播故障提供证据。在花精力分析剩余的潜在可传播故障并尝试改进仿真测试台之前，工程师可以在深度模式下运行形式化FPA，以识别快速FPA遗漏的其他安全故障，并自动生成输入激励，以演示某些故障如何传播到安全-关键输出或寄存器。这种方法减少了仿真工作，并加速实现获得ISO 26262认证所需的故障覆盖结果。

图4. 形式化FPA与故障仿真的集成

五、结果

我们使用OneSpin安全关键验证解决方案组合中的故障传播分析应用程序(FPA™)应用了两种形式化的FPA模式。该应用程序通过简单的界面实现了两种模式方法，还允许用户调整高级校样设置。然而，该工具所采用的证明方法和策略的复杂性被隐藏起来。FPA应用程序接受用户定义的故障群，但也可以创建一个包含设计中所有潜在的卡在0和卡在1故障的故障群。对于每个设计，我们提供了作为故障传播分析目标的观察点列表。所选的观察点包括安全关键输出或寄存器。我们还提供了一小部分控制输入，这些输入在分析过程中与其非活动逻辑值相关联。该列表通常包括测试模式和调试模式输入。目标是识别快速FPA期间的大多数安全故障。对于深度FPA，目标是针对一小部分断层得出结论性结果。进一步研究了被证明可传播到观测点的故障子集，以分析其传播路径。表1和表2分别显示了快速和深度FPA模式的结果。值得注意的是，快速模式下的总体运行时间通常与故障群体的大小成正比。另一方面，在深度模式下，每个故障的运行时间可能会有很大差异。

表1. 形式化快速FPA结果

表2. 形式化的深度FPA结果

六、结论

现代汽车SoC包括复杂的安全关键功能和安全机制。为了符合ISO 26262要求并计算所需的故障指标，工程师可能必须在RTL和门级设计模型上注入并分析数百万个故障场景。形式化验证工具可以为故障注入和严格分析提供强大的手段。本文提出的方法需要最少的用户输入，采用务实的分治方法，并与基于仿真的方法集成。在任何仿真工作之前可以解决大量故障。专用的形式化算法可以快速得出结果，减少后续的仿真工作量。小故障群（通常代表仿真后无法分类的故障）可以使用一组不同的算法和证明策略来解决，这些算法和证明策略需要更长的运行时间，但更有可能提供结论性的结果。所给出的结果证明了该方法对于现代安全关键设计的适用性。

详询“牛小喀”微信：NewCarRen

详询“牛小喀”微信：NewCarRen

作者：牛喀网专栏作者
牛喀网文章，未经授权不得转载！