从移动设备到汽车乃至工业机械，越来越多的产品采用需要软硬件协同工作的高级处理技术来执行一系列艰巨的任务。不过，随着系统日趋复杂性，设计人员在验证软硬件是否能够协同工作方面也面临着日益严峻的挑战。过去数十年来，企业和研究人员已推出一系列相关方法。不过，要想验证软硬件是否能如愿协同工作，仍然困难重重。

10 多年来，形式验证技术一直是设计团队进行硬件准确性验证工作最具发展潜力的技术之一。最近据英特尔公司透露，该公司工程师正是采用了这种验证技术，才解决了上世纪 90 年代 Pentium I 微处理器浮点单元问题。[1] 形式验证技术随后备受英特尔及众多其它硬件设计公司推崇，不过这种技术仍是一种比较冷门的选择。软硬件协同验证的形式验证技术在业界仍未得到广泛采用。

OneSpin Solutions 公司、凯泽斯劳滕大学 (University of Kaiserslautern)和赛灵思的研究人员近期联合对如何采用形式验证技术全面验证赛灵思同时内含嵌入式固件和硬件组件的 IP 软核进行了一项调研。研究发现，在可扩展的形式验证环境中，可以捕获固件和硬件之间的互动。这项调研工作是产业界和学术界的一项重要合作，充分利用了近期与硬件有关的固件形式验证技术的进步，而且采用了间隔属性检查(IPC) 这种有界模型检验方式。

模型检验和 IPC
形式验证技术采用数学方法，以确保设计满足严格的功能准确性规范要求。它从设计模型、系统工作环境描述以及设计可能遇到的一系列属性入手。随后要验证这些属性能否适用于所有情况，是否会出现属性失效的情况。设计人员越来越多地结合采用形式验证和较传统的仿真验证技术，从而发挥二者的最佳优势。举例来说，等效性检验和断言源于形式验证技术，不过现已广泛融入仿真验证流程之中。

模型检验是一种先进的系统自动形式验证技术，这些系统可作为有限状态机，系统规范则被视为时序逻辑的一系列属性。每个属性指定一段时间内与系统状态集相关的有效（或无效）逻辑行为。举例来说，RESET 属性断言：当 RESET 信号处于活跃状态，不管系统在一段时间内转换为何种状态，都将返回 RESET 状态。这些属性能以熟悉的语言格式表达，如SystemVerilog 断言或 SVA（见侧栏：“间隔属性检查的工作原理”）。

一系列属性构成系统规范的抽象模型。模型检验软件负责处理每个属性，为全面验证属性，将涵盖设计所有可达的状态。如果属性失效，那么模型检测器会返回反例，说明属性未满足重设要求。

模型检验工作自动执行，相对迅速。与仿真验证技术不同的是，它能全面测试系统模型，从而常常能够发现隐蔽的问题。有时这些问题会出现在不起眼的角落里，有时那些为仿真测试台创建刺激测试模型和断言的验证工程师很容易忽视问题的起因。

现代系统有大量的状态变量，通常会出现所谓“状态空间爆炸”问题，可达的状态呈几何级数增长。由于状态空间非常复杂，很容易超出传统模型检测器的能力范围，从而限制这种技术的实用性，所以才需要使用间隔属性检查等更新的模型检验方法，也就是我们在这项工作中所使用的方法 [2]。

IPC 是一种专用的有界模型检测器。与其它有界模型检测器一样，IPC会将属性范围限制在有限的时钟周期数之内，从而控制整体复杂性，并采用布尔可满足性 (SAT) 解算器来执行实际的模型检验工作。IPC 和传统有界模型检测器的区别在于，它的时钟周期窗口能允许属性断言在任意时间点上启动。

IPC 还可提供一种解决状态空间爆炸问题的简单方法。IPC 方法通过设计抽象来指导用户创建代表验证的设计关键功能的概念状态机 (CSM)。CSM 可捕获给定设计中所有基本操作或事务处理。在抽象的最高层，CSM的每次状态转换都代表一个原子运动，被唯一的属性所覆盖。实际上，由于CSM 是设计提取后的抽象视图，因此在相应的 RTL 代码中，每个 CSM 事务处理都对应于多达数百个相关信号活动的时钟周期。适当的属性可捕获全部最相关的状态以及周期精度级的输入输出信号行为，支持提取的完整周期。每个属性指定多周期时间间隔中的预期行为，精确对应于 CSM 的一次转换或操作。因此该方法就叫做间隔属性检查，也被称作操作式间隔属性检查。

CSM 抽象有意不捕获底层 RTL设计的所有细节，而只是详细阐述对捕获完整系统行为至关重要的控制状态子集，以缩减状态空间和降低状态转换复杂性。这样，IPC 就不同于基于断言的标准验证（该验证需要设计人员向 RTL 代码添加局部信号级断言，并通过仿真或尽可能使用形式验证技术来进行检查）。很多情况下这种断言会检查设计人员在实施 RTL 代码相应部分时所推断的先决条件。这些局部断言与 IP 模块规范的关系可能不够清楚。此外，这种手动生成的断
言在整个代码库中不规则分布，难以分析其是否覆盖了整个设计功能。

下面，对所有可能的状态转换进行自动全面的探索，并对其相应的属性予以验证。任何属性失效会突出显示，并提供导致失效的反例细节。带有OneSpin 360 MV 形式验证工具的操作式 IPC 还能自动进行完整性验证分析。这也可以采用同样先进的用于验证 CSM 属性的属性检查技术（采用高效的布尔可满足性解算器）来完成。

完整性证明能够确保每个可能的输入序列都有唯一的操作属性链来确定设计行为。链的属性通过 CSM 中的抽象开始状态和结束状态链接在一起，而输入触发器则匹配考虑中的各个输入迹线。此外，分析过程中要检查每个属性是否分别指定了特定时间间隔内所有相关的输出信号，并确保各时间间隔彼此相连，不会存在输出行为描述上的任何漏洞。

这样，证明完整性时就能整体检查属性集。如果检查通过，就不会出现属性集无法确定设计行为的输入情况。因此，属性集也能涵盖完整的设计功能。

随着越来越多地要求对嵌入式固件及其与硬件互动进行验证，采用形式验证方法始终是一个挑战，也需要不断积极研究。分别对固件和硬件组件进行验证一直是标准做法，但这最终需要花费大量时间进行全系统集成。此前，验证工程师采用间隔属性检查，主要是用于硬件子系统的形式验证。不过近期调研发现，已找到将这种方法扩展应用于含有硬件和固件的更完整系统上的途径。这项工作的重点就是通过将 IPC 应用到赛灵思商用 IP 软核（即软错误缓解 (SEM) 内核）来评估描述固件、硬件及二者之间互动情况的统一形式验证环境( http://www.xilinx.com/cn/products/intellectual-property/SEM.htm )。该内核包括寄存器传输级 (RTL) 逻辑和一个PicoBlaze™ 微控制器。

SEM 内核
为更好地了解验证工作，我们先进一步了解一下这个 IP 软核。这个赛灵思 IP 软核不仅能检测、归类并纠正赛灵思 FPGA 配置存储器中的错误，而且还可为测试目的注入错误。

新型半导体产品容易受到高能级辐射的干扰。比方说，高能中子产生单粒子翻转 (SEU)，直接影响芯片，进而导致配置存储器单元状态的变化。为了缓解上述影响， 赛灵思FPGA 配置帧的存储器单元都采用单错误纠正/ 双错误检测硬件模块保护机制。对航空器仪表等特定应用而言，还应采取更为精密的纠错机制，以抵御极高能级辐射带来的影响。SEM 内核可通过赛灵思 FPGA 中的FRAME_ECC 端口来监控纠错码(ECC) 模块的状态，然后针对这些情况提供适当的解决方案。

SEM 内核采用赛灵思 PicoBlaze微控制器来监控配置存储器单元的状态，并根据需要采取纠错措施。设计人员可将 SEM 内核集成到设计中，并与设计中的其它电路系统组合在一起，实现更高级的防辐射保护机制，满足应用需求。如果检测到配置存储器错误，SEM 内核能直接纠正，或将错误情况通报给更高一级的系统设计。

正确操作 SEM 内核至关重要，因为其唯一目的就是确保用户 FPGA电路的准确性。赛灵思已对该内核进行了全面验证，不过应当指出的是，由于种种原因，该 IP 的验证确实非常艰难。

该内核与 UART、前面提到的FRAME_ECC、FPGA 的内部配置访问端口 (ICAP) 和定制错误注入接口等接口进行通信。虽然我们对这些接口了如指掌，但却很难以各种可能的输入组合加以操作， 让嵌入式PicoBlaze 微控制器唱重头戏。SEM内核功能的形式验证要求我们捕获如下三者之间的互动情况：用汇编代码编写的 PicoBlaze 固件、封装逻辑以及规范文档中所述系统资源的外部接口。

为完成上述任务，我们采用 IPC来验证 SEM 内核中与硬件相关的软件的准确性。

采用 IPC 对固件和硬件进行形式验证
在对总线协议的启动代码或驱动程序及其运行所在的硬件等低级固件进行形式验证时，设计团队往往面临着巨大挑战。近期，德国凯泽斯劳滕大学电子设计自动化集团的一个团队介绍了一种将 IPC 扩展应用于到软硬件协同验证的方法 [3]。其中要解决的难题就是如何处理包含成百上千代码行代码的状态空间爆炸问题。

该团队的主要观点是，利用间隔属性抽象为有限状态序列集，这些序列集用大量代码行表示，在此基础上进行操作式属性检查。这样，该技术可在单个概念状态机中将软硬件事件结合在一起。通用计算模型采用 IPC方法，首次支持软硬件交互表示和调试。当然，这种方法也存在局限性，也不适用于所有类型的软件。特别需要指出的是，大量使用递归的代码不在当前讨论范畴之中。

验证 SEM 内核时，我们采用固件控制流程图 (CFG) 来生成属性模板。基本模块之间的每个转换都被视为独立的属性，由 PicoBlaze 微控制器内置的寄存器或外部事件所触发。给定周期中描述抽象开始/ 结束状态的功能仅取决于 PicoBlaze 架构状态及任何外部刺激。

IPC 需要描述 SEM 内核在断言开始/ 结束时的状态，这时我们需要检查 PicoBlaze 固件和 FPGA 逻辑的RTL 代码。图 1 显示了固件和硬件状态的组合。需要注意的是，PicoBlaze微控制器在真正实现软件有限状态机，且其行为直接影响到封装硬件。如果可能，单独验证固件需要一个硬件总线功能模型 (BFM) 接口，实际上这会产生又一个行为测试平台。不过，IPC 的扩展使我们能在统一的验证环境中对包含硬件和固件的全系统的行为进行建模。我们本来能在指令集仿真器中运行固件并对其进行编译，但却无法在一个环境中全面捕获硬件和固件系统行为。而使用 IPC，我们则可以在统一的硬件/ 固件验证环境实现上述操作。

在构建属性时，我们可反复限制其复杂性，从而在 OneSpin 360 MV工具中我们就任何给定属性的复杂性及其评估时间进行折中，实现最佳平衡。在本例中，我们发现让属性的间隔在 100 个周期以下比较好，这样属性验证可在 30分钟内完成。

SEM 内核还涉及到更深层次的设计因素，也有助于降低属性复杂性。SEM 内核固件和 PicoBlaze 微架构的有关方面以及如何实施以简化属性创建等，都与此相关。

首先，我们可利用 SEM 内核嵌入式固件的某些特性：
 固件镜像可实现软件有限状态机，其某些特性有助于正式描述处理器状态。特别需要指出的是，固件不会动态分配存储器，也不会调用无限递归。这是一般低级嵌入式软件的典型情况。固件的这两大特性能大幅简化处理器状态及其存储器的建模。

 向验证工程师提供全局变量和局部变量的详尽内存映射。SEM 内核可提供封装 RTL 中用于触发固件状态转换的全部外部变量，以便配合供OneSpin 360 MV 工具，共同探索。

 最后，固件机代码存储在 SEM 内核的 ROM 中。由于 ROM 可提供可视化验证流程，因此无需全面验证 PicoBlaze 微控制器上可运行的任何程序，而只需验证 ROM 中实际存储的程序。换言之，经现场验证适用于所有固件的 PicoBlaze 微控制器，我们不必再次验证。我们可集中精力验证 PicoBlaze 微控制器与SEM 内核的固件以及 wrapper RTL 之间的互动情况。

其次，我们还可利用 PicoBlaze 微架构的特性来描述固件镜像的状态。PicoBlaze 微架构的一些特性能简化其在形式验证工具流程中的集成。

 指令的执行井然有序。由于 SEM内核中指令执行连续进行，因此我们能确切知道固件内某条指令相对于其它指令的启动时间。

 每条指令的解码或执行需要两个周期。由于 SEM 内核固件工作中时延是确定的，因此我们能创建出囊括多条指令的属性，而这些指令则能根据确定的总时延加以执行。

 PicoBlaze 微架构支持有限堆栈深度。堆栈内容是 SEM 内核状态的关键部分，但有限深度情况下，该状态不会超过设定的深度。由于属性验证的复杂性随状态数量的增加而增大，因此堆栈内部设定的深度可简化验证工作。

描述某个周期内处理器的状态时，架构状态数量的描述相对简单。这种可管理的状态描述可直接向 OneSpin360 MV 的属性生成工具提供信息。

有了这些简化因素，我们就要描述相关的状态转换了。我们可将作为各个设计状态的固件基本模块映射后直接描述。从定义上看，基本模块包括线性指令序列。每个条件跳转或条件函数调用都可决定一个基本模块或两个潜在后续模块的终点。指令的目标地址标志着新基本模块的起点。控制流程图包含基本模块及后续关系。图中每个边缘都对应于固件的条件分支，并标明分支条件。

如果用高级语言来实现固件，则编译器可自动生成 CFG。不过，借助（符号）指令集仿真器，我们同样也可从汇编代码中抽象 CFG。该技术还能支持仅提供汇编代码的传统平台的协同验证。

验证 SEM 内核时，我们采用固件CFG 来生成属性模板。基本模块间的每次转换都视为 PicoBlaze 内置寄存器或外部事件触发的独立属性。任何给定周期中描述抽象开始/ 结束状态的功能仅取决于 PicoBlaze 架构状态和所有外部刺激。

作为外部刺激到架构状态映射的一部分，实践证明我们必须指定每个条件跳转或函数调用的分支条件。我们关心的是设计的整体行为，因此我们要指定外部输入事件或封装电路重要的状态寄存器（而不是嵌入式处理器的局部状态寄存器）的条件。触发条件下评估的封装寄存器可成为抽象状态定义的一部分。

SEM 内核固件和 PicoBlaze 微控制器本身都能进行条件简化，因此我们能就处理器状态和外部刺激定义所有固件状态转换。这种状态涵盖固件和硬件， 可将设计的整体行为与OneSpin 360 MV 工具中的抽象概念有限状态机相关联。

属性的生成
我们发现，SEM 内核的固件和硬件均能用 1700 种属性描述，这些属性捕获了设计及其接口的端对端功能。我们用 OneSpin 360 MV 来检查属性，并探索整个属性集的完整性。属性能并行验证，服务器集群中属性验证最长大概需要 30 分钟才能完成。

乍然一看，总共 1700 个属性好像很多。不过，大多数属性（约 1500 个）的验证只涉及顺序 UART 的等待循环，顺序 UART 除转存控制器的状态信息外，主要用于调试目的。切记，每个属性都是一个以条件跳转结束的基本软件模块，因此每个 UART 等待循环都会在形式模型中创建唯一的属性。就设计的全面验证来说，我们发现等待循环期间无法预见的负面效果不会破坏抽象状态内容。

总之，生成的属性贯穿固件的整个控制流程，描述了相应固件基本模块执行过程中设计的输入/ 输出行为。就本案例研究而言，上述属性配合现有的验证测试平台，可让您对内核功能的准确性信心百倍。

生成的属性还反映出一个情况，即 SEM 内核错误注入测试特性可将错误注入到某个配置存储器位置，不过只有在不按 SEM 内核产品文档建议的方式操作错误注入端口时才会发生此类情况。虽然该问题在正常操作条件下不会发生， 但赛灵思还是更新了SEM 内核特性，从而彻底杜绝了这种可能性。

致力于打造高质量
在我们的调研中，我们演示了用于形式验证赛灵思 SEM 内核中高度集成的硬件和固件的 IPC 方法。在统一的验证环境中，用 1700 个并行验证的属性对 SEM 内核进行了全面验证。在验证过程中，采用了最新形式验证技术和工具。验证结果则能让您对 SEM 内核的功能准确性信心大增，同时突现了赛灵思继续致力于打造高质量 IP。