内容提要：在本文中，我们提出了对现有SoC故障分析方法的扩展，描述了（1）基于有界模型检查(BMC)的自动生成失效场景的算法；（2）一种用于自动执行SoC安全分析的方法和基于Simulink的工具；（3）所提出的分析流程在具体SoC用例中的应用。

摘要

随着工艺技术规模的缩小，测试困难以及电路对随机硬件故障的敏感性不断增加。当系统工程师必须量化其SoC设计所实现的可靠性，加上片上系统所执行功能的复杂性不断增加，引发了关键问题。在本文中，我们提出了对现有SoC故障分析方法的扩展，描述了（1）基于有界模型检查(BMC)的自动生成失效场景的算法；（2）一种用于自动执行SoC安全分析的方法和基于Simulink的工具；（3）所提出的分析流程在具体SoC用例中的应用。

一.简介

片上系统(SoC)设计和测试的复杂性似乎非常适合时间的单调非递减函数。一方面，技术尺度减小带来了相当大的缺陷，例如电路对辐射引起的软错误的敏感性更高。另一方面，随着SoC遍及汽车、航空航天、楼宇自动化、铁路和医疗等安全关键领域，SoC功能也变得越来越复杂。普遍使用SoC来控制与人类直接交互的物理系统的趋势，需要新的方法和工具来量化系统所实现的可靠性，特别是功能安全性。这需要提高SoC的测试技术和失效场景识别能力，也是工程师和国际认证机构最关心的问题之一。系统提供的服务是与其交互的另一个系统（人类或物理）所感知的行为。SoC提供的服务与指定服务的偏差称为服务失效。随机硬件故障会给SoC提供的服务带来不可预测性，并可能导致服务失效。控制服务失效并进而控制系统功能安全的典型设计方法是在空间、时间和信息域的系统设计中引入冗余。然而，即使受到控制，由辐射引起的软错误可能会因多种原因而导致残余服务失效：控制故障的技术(1)可能基于模型，其本质上抑制了一些信息，(2)可能涵盖发生的故障的总集合的子集，(3)可能仅涵盖假定在特定用例中发生的故障，(4)由于实施成本，可能有一些限制。综上所述，无论在技术上如何努力提高交付服务的可靠性，SoC服务都将不可避免地受到软错误导致的残余失效的影响。IEC 61508和ISO 26262等标准引入了指标并推荐了量化SoC安全完整性等级(SIL)的方法和工具；对于每个SIL级别，都定义了设计要实现的指标目标值，并且必须保证这一目标值。在此背景下，自动生成失效场景对于根据故障模型测试SoC设计并探索设计解决方案（包括评估容错机制的有效性和成本权衡）至关重要。相关文献中描述了几种技术和工具，提出了基于模型的安全分析方法。显示了基于模型的流程的应用，用于基于最小割集的生成来自动生成故障树。在（参考资料1中，关注牛喀网公众号，后台咨询下载），SCADE形式用于使用设计验证程序作为形式引擎执行演绎因果分析（DCCA）。在（参考资料2中，关注牛喀网公众号，后台咨询下载），Joshi等人描述了利用Simulink和SCADE进行基于Simulink模型的安全分析的一些结果。

在本文中，我们提出了现有方法的扩展，以在复杂片上系统架构的设计过程中执行自动失效场景生成。本文的主要贡献可概括如下：(1)描述了一种基于有界模型检查(BMC)的最小关键失效集 (MCFS) 生成算法；(2)一种基于Simulink的方法和工具描述了SoC失效场景的自动生成；(3)介绍并讨论了所提出的分析流程在具体SoC用例中的应用。我们的方法与前面描述的方法在几个方面不同。该算法不是建立在BDD的构造之上，而是依赖于有界模型检查(BMC)技术，充分利用并行SAT求解的最新进展。BDD的使用限制了现有技术对包含数百个布尔存储元素的模型的适用性，而并行SAT解算器与BMC结合使用则可以实现成功的算法，应用于处理包含数千个布尔变量的模型的行业级问题。该分析工具从SoC的功能模型开始自动探索所有最小关键失效集，并依赖于内部模型转换引擎来指定组件的失效模式，该引擎从SoC的功能形式化开始自动构建错误模型。SoC和失效模式功能列表使设计人员能够专注于SoC架构和容错机制设计方面。注入故障的最小性质直观地确保了在生成的场景中只考虑对分析有意义的失效，以下章节中我们会详细描述。最后，我们的分析过程支持MATLAB R Simulink/Stateflow框架作为建模和分析前端，代表系统设计的实际标准。

二.启发性案例

作为一个示例，我们引用了一个生成脉宽调制(PWM)波形的简单函数，其周期和活动时间由外部模块指定。该示例对eTPU IP上的功能实现进行建模。eTPU是一款可编程CPU协处理器，专为时序控制（实时输入捕获/分析和输出生成）而设计，提供并行运行的可配置硬件通道。之前的工作成功地将形式验证应用于基于System Verilog Assertions(SVA)语言和CadenceTMIFV工具的eTPU，以进行静态形式验证。如图1所示，在顶层，我们的模型采用三个主要输入：刻度的参考源（表示时间、角度或类似域中的参考）建模为计数器寄存器和几个值，表示所需的周期以及要生成的PWM波形的活动时间。我们可以将它们视为常数，而不失一般性。该功能被建模为两个主要FSM的组合：硬件FSM和软件FSM。硬件FSM（图1中的PWM OUT HW）表示配置为“任一匹配、非阻塞”模式的eTPU通道；它由两个并行运行的“动作单元”组成：每个动作单元配有一个比较器和三个锁存器。图3显示了Simulink/Stateflow中一个动作单元的有限状态机表示。比较器寻找刻度参考(TCRA)和软件定义值(MatchA)之间的值匹配。当两者匹配时，比较器触发通道引脚动作逻辑，驱动输出引脚。输出引脚上的建模动作为：设置引脚高电平（图3中的PinA=1）和设置引脚低电平（图3中的PinA=0）。有效输出引脚行为由另一个FSM（此处未显示）建模，该FSM考虑了来自两个操作单元的事件。三个锁存器的操作如下：一个锁存器通知发生了匹配事件，服务请求锁存器通知eTPU调度器通道需要服务，并且标志锁存器反映由软件设置的布尔变量；在我们的示例中，标志锁存器由eTPU软件设置以反映其在硬件中的状态。在匹配事件中，服务请求锁存器和运行单元的锁存器都会被触发。参考图3，用于表示这两个锁存器的变量分别是SR A和setMRLA。根据硬件锁存器的当前状态，eTPU调度程序会选择特定的eTPU软件例程并由eTPU引擎执行。这样的例程用下一个匹配时间值更新硬件通道的正确匹配寄存器，并（重新）设置相关的动作单元锁存器。eTPU软件FSM（图1中的PWM OUT SW）由三个状态组成：(1)设置初始硬件配置的初始化状态，(2)处理与活动时间结束相关的运行的状态，(3) 处理PWM周期结束的状态。为了简单起见，硬件和软件之间的交互被建模为有限的正延迟，目的是不对并行运行的整个通道以及管理其并发请求的调度程序进行显式建模。我们使用此示例通过我们的算法分析不需要的功能行为（顶级事件），以便自动生成失效场景。通常通过危害分析技术利用预定义的关键字集来识别不需要的功能行为。可能不需要的顶级事件的示例是：(1)生成周期的错误持续时间和(2)生成的活动时间的错误持续时间。我们将功能故障建模为硬件信号和变量发生的固定值（图1中的故障注入块）。图2描述了固定值故障的功能规范。在布尔SaV启用信号等于0之前，开关块让输入值直接流向输出（作为理想导线）。一旦SaV使能信号变为1（无论它停留在1的时间有多少），开关的控制使其隔离输入：输出保持在其上一个假设值，不能再改变（由图2中的Memory1块表示）。

图1. HW/SW组合的顶层视图

图2. 数值锁定的功能模型

图3. PWM OUT HW FSM中的两个运行单元之一在Simulink/Stateflow中以状态图表示

三.分析方法

我们提出了一种基于模型的方法来自动生成失效场景。图5总结了主要步骤，在本节中我们将简要回顾每项活动。需要强调的是，所开发的方法和算法也已应用于不同的应用环境，特别是作为在MBAT项目中利用形式分析和测试之间的协同作用，来验证复杂嵌入式系统的努力的一部分和作为DANSE项目中系统体系设计定义方法和工具的一部分。

A.误差模型构建

第一步是通过对其功能架构进行建模来形式化SoC架构的错误模型（图5中的活动1）。对于每个组件，标称行为均以Simulink/Statechart块的形式进行描述，并提供可能影响其的失效模式规范。此步骤应以先前执行的危害分析或设计人员的专业知识为指导。在一般情况下，失效模式表示为状态机（由设计者直接建模或从特定库中选择），并形式化在出现失效时如何修改组件的标称行为。在自动模型转换步骤之后，构建误差模型。在第五节中，将详细描述转换步骤的形式方面。

图4. 顶事件(TLE)的功能规范

图5.方法

B.顶事件规范

顶事件（TLE）是一种绝对不能发生的危害行为。它是一个不变的属性，当模型行为正确（如预期）时，它必须保持。TLE可以通过诸如故障树分析(FTA)之类的演绎安全分析来解决，也可以直接从系统需求规范中识别。顶事件是涉及子系统的输出和可能的输入的函数。对TLE建模的函数的评估应始终为FALSE，除非发生属性违规，此时它会切换为TRUE，并且TLE被称为已激活。整个系统发生的故障有可能激活TLE。例如，图4中建模的TLE形式化了以下属性：在没有故障的情况下，Pin Out的值（图1中PWM OUT HW的输出）延迟一步，Flag的值（图1的PWM Out SW的输出）不得同时等于1。

C.算法执行

错误模型由故障分析 (FA) 算法处理，该算法将顶事件规范作为附加输入。故障分析的目的是通过详尽地探索输入空间并注入失效来训练错误模型，以实现这种不安全的行为。此活动的结果有两个：一方面，生成最小失效集列表（最小关键失效集）。每组收集要注入的失效，以便断言TLE，其最小性质保证如果未注入任何收集到的（最小组）失效，则不会达到危害行为。另一方面，会生成一组执行跟踪，每个跟踪都会暴露一系列失效注入和输入值，这些失效注入和输入值会导致每个最小关键失效集的危害。这些痕迹可用于有效地运用错误模型，以显示SoC如何演变成危害状态，并帮助推理其预期和意外的不安全行为。

D.容错架构设计

安全工程师会对上一活动中收集的信息进行审核，以推动SoC的一个或多个容错版本的设计。在终止活动之前，可能需要在活动1、2和3之间进行迭代（图5），以达到功能设计的成熟描述。此活动的结果是作为可执行（并且可能是可综合的）模型生成的SoC的容错版本。

四.运行时验证

活动3期间生成的跟踪（图5）用于训练容错模型，以检查故障识别、检测和恢复(FDIR)机制的有效性。在此阶段，容错SoC设计中的缺陷可能会被发现，并且可能需要安全工程和SoC设计团队进行迭代。与传统的手动过程相比，使用基于模型的流程对复杂SoC进行安全分析具有多个优势。首先，可执行模型的使用有助于不同团队对系统的共享正式表示进行推理，这有助于最大限度地减少对需求的误解以及设计和安全工程师之间的沟通问题。然后，可以使用模型转换引擎自动处理模型，从而简化设计探索过程并减少设计错误的发生、成本和上市时间。最后，正式模型对于支持容错SoC资格所需的认证流程非常重要。

五.形式规范验证-故障分析工具

本节介绍用于故障分析的形式规范验证工具(FSV-FA)。首先将提供工具架构的概述，然后将详细描述底层探索算法。

A.工具概述

FormalSpecs Verifier (FSV) 是用于验证复杂嵌入式系统的框架。该工具的核心基于从Simulink模型到NuSMV工具本机语言的翻译器。考虑到转换步骤期间可能引入的非确定性分辨率，转换过程会生成输入模型的语义等效NuSMV表示。为了执行故障分析，FSV工具已添加了附加模块，这些模块实现了第三节中描述的部分流程。丰富内容特别涵盖了错误模型的自动生成和算法执行，总结如下：该工具将Simulink模型转换为内部格式，执行模型转换步骤。然后，该模型通过第二次转换进行处理，该转换会考虑用户提供的失效模式规范，从而丰富每个组件的错误行为，从而获得可由内部形式引擎处理的NuSMV模型。

图6.工具概述

B. 算法描述

该工具支持固定步长离散时间Simulink模型。标称模型被形式化为函数 F[u, x,f, k]，在每个离散时间k将输入u[k]和当前状态x[k]向量映射到输出y[k]和下一个的向量状态值x[k + 1]。误差模型是通过用失效模式函数丰富标称模型的行为来生成的：对于每个组件的失效模式，创建一个附加的输入变量，称为失效模式启用输入。令F={f1, . . . , fN }被定义为添加到模型中的所有失效的集合：失效使能输入是离散时间布尔函数fj[k]，如果失效fj在第k步处于活动状态，则为TRUE，否则为FALSE 。然后将误差模型建模为离散时间F[u, x,f, k]上的函数，其中f是失效模式启用输入的向量。如果后者是假值的常数向量（标识为0），我们有F[u, x, 0, k]=F[u, x,f, k]。换句话说，如果所有失效都被禁用，则标称模型和误差模型是等效的。最后，顶级事件被建模为离散时间H[k]上的布尔函数，如果TLE发生在时间步k，则为TRUE，否则为FALSE。为了执行失效场景生成算法，引入了称为监视器的附加变量。每个监视器都是离散时间mj [k]上的布尔函数，如果存在失效使能输入fj [i]为TRUE的步骤i∈[0, k]，则mj [k]为TRUE，否则为FALSE。换句话说，每个监视器都与一个失效启用输入相关联，如果相应的失效输入在过去或当前步骤中为TRUE，则该输入将变为TRUE并保持为TRUE。我们的故障分析算法（算法1）循环直到达到用户提供的给定离散时间限制（第2行）。在步骤3，形式引擎搜索一个反例，该反例在给定的时间步骤k都使监视器m1…的值之和最小化，mN，并验证危害谓词H[k]。考虑到SoC的动态行为，通过对误差模型应用有界模型检查来迭代获得反例。请注意，将BMC与并行SAT求解器结合使用，可以将该技术成功应用于现实生活中的工业规模模型。最小化过程确保仅注入最少数量的失效来触发TLE。如果找到计数器示例，则提取监控值配置并向模型添加新约束，以便从将来的搜索中排除找到的配置（第5行和第6行）。测试用例是从存储系统输入、输出和内部变量的反例中提取的（第7行和第9行）。再次执行循环以寻找其他最小可能的监视器配置，直到找不到更多配置。该算法确保(1)生成的每个失效使能集都是所分析的TLE的最小关键失效集，并且(2)通过构造，不存在暴露相同最小关键失效集的两条迹线。

六.参考例的应用

失效场景生成方法已使用FSV-FA工具集应用于第二节中描述的eTPU案例研究。使用预定义库在MATLAB Simulink中对总共45个故障进行了建模。对于周期p=100和活动时间a=25的波形，仿真时间限制为k=28步。经过60分钟的计算，使用基于Intel i7 2.4 GHz、8 GB内存的平台发现了5个失效场景。在时间步长k=2处观察到5个属性违反中的一个，而其他四个发生在时间步长k+28处。图7重现了生成的场景之一。TLE被建模为如图4所示的Simulink子系统；参考图7中所示的失效场景，当一个故障影响eTPU通道的输出引脚（pin-Out）时，这种TLE被激活。为了使属性受到侵犯，故障从一开始就处于活动状态（k=0）。图7的下部子图显示了输出引脚的值（图1中PWM OUT HW的输出）和标志信号的值（图1中PWM OUT SW的输出）。标志信号是PWM OUT SW机器的局部变量，当软件预期处理PWM OUT HW的硬件状态“引脚高”时，该信号设置为零；当软件预期处理该状态时，标志信号设置为1 PWM OUT HW的“引脚低”。在初始化时间 (k= 0)，eTPU软件将输出引脚值设置为零 (Flag=1)，在时间k=1时发生“下一次匹配”，并将与匹配事件相关的操作设置为“将引脚设置为高电平””。该引脚始终卡在1处，特别是从仿真开始时。预期的事件顺序如下：在时间k=1时，引脚应转换为1，在时间k=2时，Flag的值应转换为0，表示eTPU软件FSM（PWM OUT SW）的状态发生变化。由于卡在一个故障上会阻止引脚更改，因此会违反该属性并激活TLE。

图7.分析结果

七.结论

在本文中，我们提出了一种基于模型的方法来自动生成失效场景。该方法已应用于使用基于Simulink的工具分析SoC架构，该工具利用并行SAT求解的最新进展，实现了一种基于有界模型检查的新算法。已经提出了一个具体的SoC用例来显示所描述的方法的有效性。在未来的工作中，我们将把所提出的方法应用于更复杂的片上系统模型。特别是，我们对评估安全关键SoC中使用的跨层可靠性机制的有效性感兴趣。跨层可靠性机制允许在整个系统堆栈中分布故障/错误检测阶段以及诊断和处理阶段，从而降低生产成本。为此，将使用所提出的方法开发、运用和分析各种硬件和软件抽象的层次模型（如门、电路、硬件架构、固件、操作系统、中间件和应用程序）。

详询“牛小喀”微信：NewCarRen

详询“牛小喀”微信：NewCarRen

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