ISO 26262安全机构插入和验证四步骤讲解

翻译自——semiengineering

随着先进的驾驶员辅助系统和自动驾驶技术的引入，汽车集成电路的复杂性呈指数级增长。与这种复杂性的增加直接相关的是，确保IC不受随机硬件故障(不可预测的功能故障)的影响所增加的负担。

历史上，汽车行业通过利用专家的判断来进行安全分析。最初的安全性分析通常采用自上而下的故障模式影响诊断分析(FMEDA)。随着IC复杂性的增加，主要由专家驱动的方法不再实用或有效。

汽车集成电路已经变得太大、太复杂，以至于人们无法完全理解保护所有可能的故障所需的安全机制。必须部署自动化工作流来帮助专家处理随机故障。有效的方法是使用安全综合和形式验证来将安全机制纳入设计。这最好在寄存器传输层(RTL)进行，在那里可以有效地执行功能验证。这个过程包括：

1.安全探测:探测设计中需要更好的故障探测的区域

2.安全机制插入:使用安全综合来引入正确权衡RTL结构的安全机制

3.设计变更验证:通过形式验证来验证设计变更

4.形式故障注入:执行形式故障注入以测量诊断覆盖率

安全探测

安全探测的目标是确定最佳的安全体系结构和安全机制。安全机制有很多种，每种机制在检测随机硬件故障方面都有自己的有效性。在安全探索期间，将执行一系列“假设”场景，以了解不同安全机制对设计的影响，特别是在电源、区域、性能、安全度量和诊断覆盖率方面。我们建议在不修改设计的情况下进行这种探索，以便能够快速有效地执行同步分析。如果在设计过程的早期就这样做，安全探索将有助于设计团队在插入和验证之后成功地达到安全目标。

安全机制插入

修改遗留设计以引入安全机制可能是一个容易出错的过程。如果最初的安全机制没有达到安全目标，则情况会变得更糟，必须使用不同的机制。因此，安全综合是一种改进设计结构以提高容错能力的新方法。为了创建遗留设计的安全体系结构，安全综合自动引入了两种类型的安全机制。一个用于注册级，另一个用于模块级。

对于每种安全机制，都需要在效率、故障检测延迟和区域开销方面进行权衡。下图显示了安全关键设计中可以使用哪些安全机制。

对于设计接口，可以执行奇偶校验，以确保在设计内部的接口模块和接口控制器之间进行准确的数据传输。一旦数据在设计中，就可以通过总线上的数据奇偶性和存储元素中的错误纠正代码(ECC)来保护它们。片上总线事务可以由专用总线监视器观察。关键控制组件，如功能安全机制和仲裁逻辑，将最好的保护三重模块冗余和多数表决。中央处理器和嵌入式处理器可以通过双模块冗余和锁步检查器来保护。

注册级的插入更像是外科手术。它在存储元素中插入安全机制，比如寄存器重复和奇偶校验。这种方法通常用于保护控制和状态机结构。一些寄存器级的安全机制包括:

奇偶校验产生和检查关键控制元件

一个选定的寄存器列表的双模冗余

一个选定的寄存器列表的三模冗余

错误校正，单错误校正与双错误检测的银行的寄存器

协议检查确保有限状态机的有效状态转换

安全合成可以将奇偶校验添加到模块中的所有或特殊寄存器列表中。

控制寄存器的奇偶校验和校验

ECC也可以用于银行的注册。在这种模式下，安全合成按名称对寄存器分组，并通过创建综合征添加ECC。之后，将使用综合症来确定是否存在错误并从中恢复错误。对于有限状态机，安全综合将阐述有效的状态空间和状态转换矩阵，建立协议检查安全机制。

在实例级插入创建基于冗余的安全机制。一些模块级安全机制包括:

双模块冗余与同步检查

三模冗余与同步检查和多数表决

接口信号组的输入和输出奇偶校验

内存奇偶校验的生成和检查

如图所示，安全合成创建模块的第二个实例，并为第一个和第二个实例之间的所有输出和输入以及lockstep检查器建立适当的连接。

双模块冗余与同步检查

设计变更验证

顺序逻辑等价检查(SLEC)使用形式验证技术来验证两个设计在功能上是等价的。只要输出总是相同的，两种设计的实现就可以不同。当SLEC证明两个信号的等价性时，每个设计一个，这两个信号对于所有输入和所有时间都是等价的。如果任何一对信号不相等，SLEC会自动生成一个错误跟踪，使用波形来显示问题的因果关系。当两种设计的所有输出都被证明是等价的，我们就可以确信这两种设计在功能上是等价的。

因此，可以用SLEC来验证:

安全机构插入:确保原始设计的功能不会因增加安全机构而改变

安全机构操作:确保插入的功能安全机构工作正常

安全机构插入后，必须确保插入前和插入后的设计在功能上是等同的。与使用模拟回归验证安全机构仪表化设计的功能不同，SLEC是一种更直接和全面的方法。

在下图中，使用三模冗余(TMR)[1]作为安全机制来保护设计。通过比较设计A(无安全机构)和设计B(有TMR)， SLEC可以从数学上证明TMR已经正确地插入到设计中。由于功能仿真只能模拟有限数量的输入序列来验证TMR的运行，因此该方法具有较高可信度。

安全机构插入验证与SLEC

形式故障注入

现在我们需要确保安全机制工作正常，以保护设计免受失败。在引入安全机制之后，可以使用基于形式的方法进行故障注入。失效模式和效果分析可以决定安全机制是否充分。正式方法的建立是为了将静态故障和瞬态故障注入到设计中，通过设计的状态空间记录故障，并查看故障是否被安全机制传播、掩盖或检测到。

如图所示，使用黄金(无故障)模型和故障注入模型执行动态故障注入和结果分析。通过使用自身的副本实例化设计，所有合法的输入值都会自动为SLEC指定，就像模拟中的黄金参考模型预测任何输入刺激的所有期望输出一样。将一个错误注入设计与一个本身没有错误的副本进行比较，正式的工具会检查是否有任何可能的方法可以使一个错误逸出输出或不被安全机构检测到。

基于形式的故障注入的安全机制运行验证 

[1] 三模冗余系统简称TMR(Triple Modular Redundancy)，是最常用的一种容错设计技术．三个模块同时执行相同的操作，以多数相同的输出作为表决系统的正确输出，通常称为三取二．三个模块中只要不同时出现两个相同的错误，就能掩蔽掉故障模块的错误，保证系统正确的输出．由于三个模块是互相独立的，两个模块同时出现错误是极小概率事件，故可以大大提高系统的可信性。