ISO 26262安全机制插入和验证的四个步骤

文/杨平，侯锦，维纳亚克·德赛，雅各布·威尔特根

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

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

汽车集成电路已经变得过于庞大和复杂，无法指望人类完全理解保护所有可能故障所需的安全机制。必须部署自动化工作流来协助专家处理随机故障。一种有效的方法是使用安全综合和正式验证将安全机制纳入设计。这最好在寄存器传输级别(RTL)完成，在那里可以有效地执行功能验证。这个过程包括以下几个主要步骤:

• 安全探索:探索需要更好的故障检测的设计领域
• 安全机制插入:使用安全综合引入对RTL结构有正确权衡的安全机制
• 设计变更验证:用正式的验证来验证设计变更
• 正式故障注入:执行正式故障注入，以衡量诊断覆盖率

安全开采

安全探索的目标是确定最佳的安全架构和安全机制。安全机制有很多种，每种机制在检测随机硬件故障时都有自己的有效性水平。在安全探索过程中，会执行一系列“假设”场景，以了解不同安全机制对设计的影响，特别是在功率、面积、性能、安全指标和诊断覆盖率方面。我们建议在不修改设计的情况下进行这种探索，以便能够快速有效地同时进行分析。如果这在设计过程的早期进行，安全探索将帮助设计团队在插入和验证后成功满足安全目标。

安全机构插入

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

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

图1．安全关键设计的安全机制示例

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

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

1. 奇偶校验生成和检查关键控制元素
2. 所选寄存器列表的双模块冗余
3. 为选定的寄存器列表提供三重模块冗余
4. 纠错，和单纠错与双错检测寄存器组
5. 协议检查确保有限状态机的有效状态转换

安全综合可以对模块中的所有或一个特殊寄存器列表添加奇偶校验。

图2．奇偶校验生成和检查控制寄存器

ECC也可用于寄存器库。在此模式下，安全综合根据名称对寄存器进行分组，并通过创建综合征添加ECC。稍后，将使用该综合征来确定是否存在错误并从中恢复错误。对于有限状态机，安全综合将详细描述有效状态空间和状态转换矩阵，构建协议检查安全机制。

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

1. 双模块冗余与锁步检查
2. 三重模块化冗余与同步检查和多数投票
3. 接口信号组的输入输出奇偶校验
4. 内存奇偶校验生成和检查

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

图3．双模块冗余与锁步检查。

设计变更验证

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

图4．顺序逻辑等价性检查

因此，SLEC可用于验证:

• 安全机构插入:确保原设计的功能不因安全机构的添加而改变
• 安全机构运行:确保所插入的功能安全机构正常工作

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

在图5中，使用三重模块化冗余(TMR)作为保护设计的安全机制。通过比较A设计(无安全机制)和B设计(有TMR)， SLEC可以从数学上证明TMR已经正确地插入设计中。这种方法给了我们更好的信心，因为函数模拟只能模拟有限数量的输入序列来验证TMR的操作。

图5．安全机制插入验证与SLEC

正式断层注入

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

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

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

有关此主题的更多信息以及在实际设计中使用此方法的结果，请下载白皮书你安全了吗?安全机制插入和验证．

杨平博士，西门子门拓(Mentor)功能验证部首席工程师。他在EDA行业拥有超过20年的应用、营销和产品开发经验，包括在0-In、Synopsys和Mentor Graphics的职位。他拥有CDC和正式验证领域的9项专利。

Jin Hou，博士，西门子Mentor公司Questa Formal产品工程师，拥有超过12年的正式和基于断言的验证经验。Hou曾担任过CAE和PE，在产品定义、客户支持、工具测试、客户培训、技术营销方面都有经验，目前是Questa正式应用程序的PE。她在加拿大蒙特利尔Université de Montréal获得博士学位。

Vinayak Desai是西门子Mentor公司的功能安全产品解决方案工程师。在EDA和半导体行业工作超过18年，Desai曾担任CAD工程师和FAE，为DFT, CDC, lint，电源，合成和实现工具提供静态工具。他目前专注于功能安全解决方案、产品定义、客户评估、工具测试、AE培训和技术营销。德赛在加州州立大学北岭分校获得了硕士学位。

Jacob Wiltgen是西门子Mentor业务部门的功能安全解决方案经理，负责定义和调整IC验证解决方案组合中的功能安全技术。在Mentor之前，Wiltgen在Xilinx, Micron和Broadcom担任过各种设计，验证和领导角色，执行IC和SOC开发。他持有科罗拉多大学博尔德分校的电气和计算机工程学士学位。