Atomicity Violation Detection for Interrupt-Driven Aerospace Embedded Software
-
摘要:
嵌入式软件的可信性对航天任务的成败至关重要. 航天嵌入式软件广泛采用中断驱动的并发机制, 不确定的中断抢占可能导致并发缺陷, 引发严重的安全问题. 研究表明原子性违反是中断并发缺陷中最突出的一类缺陷模式. 目前面向中断驱动型嵌入式软件的原子性违反检测方法都无法同时实现高精度和高可扩展性, 且其对真实航天嵌入式软件的有效性尚未得到证实. 为了有效提升检测该类缺陷的精度与效率, 对82个航天嵌入式软件原子性违反进行实证研究, 获得该类缺陷在原子区范围、中断嵌套层数、访问交错模式、共享数据访问方式、访问粒度等5个方面的表现特征. 并在此基础上, 提出一个精确、高效的原子性违反静态检测方法intAtom-S. 首先, 基于一个由数值不变式参数化的细粒度内存访问模型, 引入基于规则的方法剔除标志变量访问, 并采用抽象解释进行精确的共享数据分析, 该分析能将共享数据访问粒度精确至数组元素, 并可识别共享的内存映射I/O地址. 然后, 使用轻量级数据流分析技术匹配符合缺陷访问交错模式的所有并发三次访问序, 作为潜在的原子性违反缺陷候选. 最后, 采用基于路径条件的约束求解对缺陷候选中的串行访问对和并发三次访问序进行路径可行性分析, 逐步消除误报, 得到最终的原子性违反结果. 在基准测试集和8个真实航天嵌入式软件上的实验表明, 与目前最先进的方法相比, intAtom-S误报率降低了72%, 检测效率提高了3倍. 此外, 该方法能够快速完成对真实航天嵌入式软件的分析, 平均误报率仅为8.9%, 并发现了23个已被开发人员确认的缺陷.
Abstract:The dependability of embedded software is vital to the success of the aerospace mission. Aerospace embedded software extensively uses interrupt-driven concurrency mechanisms. However, uncertain interleaving execution of interrupts may cause concurrency bugs, which could result in serious safety problems. Researches had showed that atomicity violation was the most prominent interrupt concurrency bug. Current atomicity violation detection methods for interrupt-driven embedded software cannot achieve both high precision and high scalability, and their effectiveness on real embedded software has not been evaluated. To significantly improve the ability of techniques in bug detection, we design an empirical study on 82 atomicity violations in aerospace embedded software and gain their manifestation characteristics of atomic region range, the number of interrupt nesting levels, shared data access interleaving pattern, access patterns and access granularities. On this basis, we present intAtom-S, a precise and efficient static detection technique for atomicity violations. Firstly, to realize accurate analysis of shared data, intAtom-S constructs a fine-grained memory model parameterized by numerical invariants, and introduces rule-based method to eliminate flag variable accesses. Moreover, it can handle array elements as well as shared I/O addresses. Then, a lightweight data flow analysis technique is used to find all access interleavings that match the patterns as potential bug candidates. Finally, intAtom-S adopts a consecutive access pair feasibility analysis and access interleaving feasibility analysis to prune the infeasible paths. intAtom-S gradually eliminates false positives, and obtains the final atomicity violations. Experiments on a benchmark and 8 real-world aerospace embedded software show that intAtom-S reduces the false positive rate by 72% and improves the detection speed by 3 times, compared with the state-of-the-art methods. Furthermore, it can finish analyzing the real-world aerospace embedded software very fast with an average false positive rate of 8.9%, while finding 23 bugs that had been confirmed by developers.
-
处理器开发阶段可以分为设计阶段和验证阶段. 当前，处理器的验证已经成为了处理器开发流程中的关键路径[1-4]. 面对不断增长的算力需求和不断多样化的应用类型，处理器的开发过程变得愈加复杂. 一方面，多样的应用需求和高算力需求驱动着处理器开发者们不断设计出更为复杂的处理器微结构以适应这一趋势，处理器状态空间不断膨胀. 另一方面，面对多样化的算力需求和摩尔定律接近终结的现状，发展领域专用架构（domain specific architecture，DSA）成为新的趋势，这要求处理器开发走向敏捷，快速迭代以适应DSA发展的需求. 面对这些趋势，高抽象层次的设计语言和面向对象的开发方法的应用对处理器的设计效率带来了巨大的提升. 然而，处理器的验证效率并未相应地提升. 面对不断膨胀的处理器状态空间和正在涌现的处理器敏捷开发需求，处理器验证正面临着前所未有的挑战. 验证已经成为了处理器开发中耗时最长的阶段，通常占据芯片开发周期的50%~70%[3]. 因此，提出全新的敏捷验证方法迫在眉睫.
以现代处理器当前的庞大规模而言，几乎不可能仅通过软件仿真的方式实现对处理器的充分验证. 从时间成本与经济成本的综合考虑的角度出发，FPGA原型验证，作为一种价格相对低廉、运行速度极快的验证方法，成为工业界的处理器开发流程中不可缺少的一环. 然而，FPGA的信号可见性差、可调试能力非常有限，因此很难对FPGA上检查到的处理器错误进行定位和解决. 基于断言的验证（assertion based verification，ABV）方法也是一种被广泛使用的方法[1,3]. 断言，尤其是基于时序逻辑的断言，能够高效地对处理器的局部功能行为进行检查，其贯穿于处理器设计的多个抽象层级，提升内部信号的可见性. 因此，断言可以很好地对FPGA原型验证的弱调试能力、弱信号可见性等不足进行针对性补充. 但是，在传统的FPGA原型验证当中，断言，尤其是支持时序逻辑的断言，是一种无法被FPGA的EDA工具综合的语法特性[5]，这一方面是由于EDA厂商长期只关注基础的调试工具，另一方面是由于基于时序逻辑的断言本身的复杂性（很多软件仿真器也未能完整实现对这些特性的支持）. 因此，断言方法被限制在部分软件仿真平台上，无法与FPGA原型验证相互配合使用.
为了解决以上问题，本文围绕着断言与FPGA原型验证，面向处理器的功能验证作出了3点贡献：
1）面向处理器功能验证需求，提出并实现了一种断言语言[6-7]SVA（SystemVerilog Assertion）的自动化编译方法，以及一套端到端的工具流和硬件平台，能将不可综合的断言转化为逻辑等效但可综合的RTL电路.
2）针对FPGA平台的断言提出了一种获取和利用断言结果的方法，从而对验证过程的进度进行指示，对设计运行状态进行检查.
3）通过FPGA加速的断言平台，取得了相对于软件仿真2万倍的验证加速能力，以及比传统硬件调试方法更小的资源占用和更全面的调试能力.
1. 传统处理器功能验证方法及其特点
处理器验证首要的任务是保证处理器的功能正确性，即功能验证. 功能验证一般通过输入一定的测试激励，动态地运行待测设计，从而检查处理器运行过程中是否存在错误，这与形式化验证方法有所不同. 处理器的功能验证基本上通过动态地与参考模型行为对比来实现：将待验证设计（design under verification，DUV）与验证人员预期的设计行为进行对比. 高效的功能验证涉及到2个方面：1）对于验证人员所预期的处理器行为进行建模的方式；2）处理器的验证平台. 以下从这2个方面对传统的处理器验证方法进行介绍.
1.1 处理器行为建模方法
对处理器行为进行建模的方式，决定了验证过程中使用的错误检查机制. 设计建模的层级、被建模状态与设计核心功能的关联程度，都影响着验证的有效性与高效性. 一般来说，建模的抽象层级越高，就越难定位到错误根因；被建模状态与核心功能关联越远，在调试过程中就越需要更多额外回溯.
处理器验证中使用的错误检查机制大致可以被归类为3类：基于I/O对比、基于全局指令集模型（instruction set simulator，ISS）对比以及基于局部模型对比.
基于I/O对比的方式通过观察DUV的输出结果是否与预期一致来对设计进行验证. 此种方式建模的抽象层级较高且与处理器的核心逻辑关联较弱，因此当出现错误时，往往需要大量回溯进行错误定位.
基于全局指令集模型对比的方式通过在处理器系统的某一个抽象层级，如指令集架构（instruction set architecture，ISA）层级、微架构（micro-architecture，μARCH）层级，建立ISS作为参考模型，并暴露待测设计的关键信号与之进行对比，从而对处理器进行验证. 全局模型对处理器的功能进行全面的建模，然而模型所在抽象层次之下的一些错误相对来说难以发现，如ISA级的ISS对比不会检查设计的分支预测实现，而进一步提升建模的精度会造成建模成本的上升和模型可迁移性的下降.
基于局部模型对比的方式通过对设计的一部分功能进行建模来检查设计功能行为. ABV就属于这一类型. ABV方法是指验证人员在待测设计中加入断言来描述处理器局部的组合与时序行为以验证设计正确性的方法. 在功能验证中，支持断言功能的平台会动态地对这些功能属性进行监测和检查，判断是否出现违例. 对电路行为进行描述的断言语言有很多，包括SVA[6-7]和属性规范语言（property specification language，PSL）等. 其中，SVA可以内嵌于SystemVerilog代码当中，而SystemVerilog语言[7]则是当前使用最为广泛的验证语言之一[3]. SVA相对于命题逻辑断言增加了对时序信息的描述，可以描述一组信号在一段时间内复杂的组合与时序行为. SVA中提供了多种描述时序逻辑（temporal logic）的操作符，包括采样函数$past和$rose，延迟操作符##等. 相对于命题逻辑断言，SVA表达能力更强、更贴近电路当中的硬件行为. SVA可以从2方面有效地增强验证过程当中的信号可见性：一方面是空间上可见性提升，即局部关键信号的暴露；另一方面是时间上可见性提升，即断言时序逻辑描述能让对电路行为的检查不局限于某个周期，而是对一段时间内的信号行为进行监测. 断言在实际中有着广泛的应用，在处理器设计中，断言可以应用于总线协议检查、仲裁机制合理性判断、状态机状态转移过程跟踪，也可以在大型设计中各个系统模块集成时对各类系统级接口行为进行检测[8-9].
1.2 处理器验证平台
主流的处理器验证平台可以分为3类：软件仿真器、硬件仿真处理器和FPGA.
软件仿真器包括各种开源或商业的仿真器，例如Modelsim，VCS，Verilator，Icarus Verilog等. 软件仿真方式拥有几乎全视的信号可见性，能够记录大量的运行时信息，方便对设计进行回溯. 同时，极高的信号可见性带来了多种高效的验证方法，可以动态地检查断言或在线与参考模型进行对比[2,4]. 软件仿真器最大的缺点是其极低的仿真速率. 软件仿真器周期精确的仿真方式使得软件仿真很难利用多处理器并行地对设计进行仿真，这也使得软件仿真往往受限于处理器的单核频率[10]. 在实际应用中，对于处理器规模的设计，仿真器的运行速率一般在kHz级别，因此，软件仿真的运行效率极低，现实中几乎难以仅依靠软件仿真对一个处理器进行充分地验证.
硬件仿真处理器是一种专门用于芯片验证的产品，例如Cadence的palladium、Synopsis的Zebu. 这类设备有着相对较好的可调试能力，速度介于FPGA与软件仿真器之间. 其最大缺点在于价格极其高昂，其成本每台达到几百万美元，对于个人和中小规模的开发团体来说，几乎没有使用的可能.
通过FPGA作为验证平台，构建与处理器功能一致的硬件原型系统，通过对该原型系统进行测试的方式被称为仿真或者原型验证[11]. FPGA平台有着3类平台中最高的运行效率，并且有着相对更低的价格. FPGA原型验证方式充分利用了FPGA高并行度的计算能力，相对于软件仿真器，可以对仿真速度起到质的提升. 由于FPGA仿真效率更高，可以使验证流程尽快收敛. 然而，传统的FPGA原型验证受限于自身弱调试能力，弱信号可见性的不足，往往被认为是一种高速运行以发现错误的工具而非定位错误的调试工具.
1.3 小 结
基于上述背景，断言与FPGA的结合对于基于断言的验证方法和FPGA验证平台都是很大的补充. 一方面，断言作为一种高效的验证手段，能够对DUV内部逻辑进行监测和检查，将设计内部的关键信号暴露出来，提升了验证过程中的信号可见性，对FPGA平台的验证方法有着很好的补充作用；另一方面，断言这种原本只能在软件仿真器上运行的机制，可以借助FPGA的高效运行速度更快更精准地定位错误，可以通过FPGA平台更快地完成验证. 正因如此，将FPGA与断言相结合成为了必然的方向.
2. 基于FPGA加速的验证方法
综合时间成本与经济成本2方面的因素，FPGA成为了充分验证处理器的较好选择. 本节主要针对基于FPGA的验证方法进行综述，重点围绕错误检查机制和可调试能力2个方面展开.
2.1 传统的FPGA原型验证方法
传统的FPGA原型验证方法使用FPGA厂商提供的EDA工具，将待测设计进行综合、布局布线、生成比特流等步骤映射到FPGA硬件电路上运行，并将运行结果和参考模型的结果进行比对，从而实现对待测设计的验证过程. 特别是对于处理器验证来说，基于FPGA的验证方法构建了一个系统级原型，可有效测试顶层软件和底层外设模型等软件仿真很难实际建模的场景，且运行速度远高于软件仿真，便于快速检测设计中是否存在错误.
然而，基于传统FPGA原型的验证方法在错误检查机制和可调试能力2方面都很有限，这主要受限于2个原因：传输带宽有限导致验证过程中只能对少量的信号进行监测；片上存储资源有限则限制了片上可容纳的运行时信息.
从错误检查机制来说，传统的FPGA原型验证方法往往只能使用简单的基于I/O的建模方式进行错误检查，通过FPGA的一些接口如串口的输出来检验设计的正确性. 从调试方法来说，FPGA开发者一般是通过扫描链和FPGA生产商提供的信号记录缓冲（trace buffer）机制[12]来进行片上调试. 例如Xilinx公司提供的ILA机制和Intel的SignalTap都属于信号记录缓冲方式. 这些方式通过消耗片上的额外存储资源来提供一个对内部信号观察的窗口. 但是由于错误出现的时刻以极其离散的方式分布在验证过程当中，有限的观察窗口内对有限信号的观察难以支持验证的错误检查与定位.
针对于FPGA的这一短板，一些工作针对于如何提升FPGA调试能力的问题展开了研究. 例如，文献[13]提出了将软件仿真中常用if-printf语句组合进行硬件化，从而方便地设置信号记录缓冲的内容与触发条件，但这些工作实际上并未提升FPGA的验证能力，仍然未突破FPGA原型在调试上的2方面不足.
2.2 敏捷FPGA原型验证方法
伯克利大学的DESSERT[14]工作对于FPGA的错误检查机制和可调试能力都进行了一定的扩展. DESSERT实现了简单的基于命题逻辑的断言和基于指令提交记录与软件仿真的对比，同时通过局部区域的输入输出记录实现了一定程度的错误重放.
多伦多大学的工作利用部分高端FPGA所支持的回读功能实现了一种软硬件协同的仿真框架StateMover[15]. StateMover是一种基于检查点的FPGA 调试框架，该框架利用对电路某一时刻的状态进行快照，从而允许用户在仿真器和FPGA之间转移状态，实现了FPGA原型与软件仿真器之间的无缝衔接切换. StateMover通过软件仿真器将FPGA上一瞬间的全局信号可见，拓展到检查点之后无限时间的全局信号可见. 然而StateMover要消耗秒级回读回写时间，相对于以大约100 MHz运行的FPGA原型系统来说，回读回写的开销显得过于高昂. 因此需要给出与出错现场接近的快照时间点，才能有效提升验证效率.
敏捷验证框架ENCORE[4]实现了一种软硬件协同仿真对比检查错误的机制. ENCORE在FPGA的行为上进行了扩展. ENCORE将FPGA上的处理器原型与通用处理器上的指令集模拟器进行对比，在线对比处理器ISA级的关键信号. ENCORE同时结合了前文提到的快照机制，以原型系统和仿真的不一致作为快照触发条件. 相对于StateMover，ENCORE将出错点作为设计快照点，很好地解决了何时快照的问题. 但是，ISA级的模型隐藏了底层的微架构细节，导致部分错误无法被即时捕捉，需要大量回溯. 而进一步提升模型的细节则会增大总线带宽的压力，降低软件端运行效率，导致整体系统效率进一步下降.
断言在FPGA原型系统中有2大优势：1）局部任意粒度的行为建模；2）片上在线自检查. 正如前文所述，DESSERT实现了基于命题逻辑的简单断言，但是此种断言的表达能力相对于SVA断言来说更弱. 此前也存在其他的一些基于SVA的硬件化断言方法[16-18]，但是这些工作往往只关注运算符的转换，而忽略了在实际设计中如何从设计中提取断言、如何将硬件断言与DUV进行连接，缺少对断言结果的访问方法和使用手段，需要一个全面完整的硬件化SVA的方法.
3. 硬件化断言平台的设计
断言是一种有效的辅助调试手段和错误检查机制，对于SVA的硬件化的困难来源于3个方面：1）SVA常内嵌于电路设计的代码之中，为了保证断言可以监测到正确的电路功能区域，需要分析断言与设计之间的连接关系，也需要考虑设计本身的嵌套关系. 2）SVA中包含大量的不可综合运算符，例如非交叠蕴含（non-overlapped implication）操作符、延迟操作符等，需要提供这些运算符的对应可综合实现，才能将整个断言表达式转化为硬件，嵌入实际的硬件之中. 3）此前的工作鲜少涉及到断言结果的使用，断言结果包括断言触发对验证进度的指示和断言失败对错误的电路或断言状态的暴露. 本文针对这一问题进行研究并提出一套结果收集方案.
硬件化断言平台的整体工作流程与结构关系如图1所示. 本节后续内容按照图1中划分的三大部分进行介绍，分别是：硬件化断言编译器、硬件化断言算子库、硬件化断言收集器.
![]()
图 1 硬件化断言自动化编译器工作流与平台结构Figure 1. Workflow and platform structure of the hardware assertion automatic complier3.1 硬件化断言编译器
硬件化断言编译器负责将设计中的断言进行提取、转换，同时保留必要的信息进行设计连接. 内嵌于设计代码之中的SystemVerilog断言与设计代码紧密关联，其中蕴涵了两大类的信息，即断言外部环境信息和断言内部结构信息. 外部环境信息指的是断言模块与待监测设计信号的连接关系，本质上是待监测设计信号与断言输入之间的映射关系. 内部结构信息则是断言的表达式结构，该结构描述了断言的各个子表达式之间的联系和数据流向. 硬件化断言编译器分2个步骤将这些信息进行提取和转化. 其具体结构如图2所示.
SystemVerilog是一种基于上下无关文法的硬件描述语言. 为了充分表达断言的外部环境信息与内部结构信息，本文选择在SystemVerilog的抽象语法树（abstract syntax tree, AST）上对断言代码进行提取和转化. 本文使用Slang[19]作为前端解析工具，对SystemVerilog代码进行词法分析和语法分析，从而获得其AST. 后续的分析都在设计代码对应的AST或AST子树上进行.
为了提取断言外部信息，同时也为了去除AST其余部分对分析过程的干扰，只保留断言本身的内部结构，本文设计了断言提取工具来完成这一步骤. 断言提取工具首先将用户指定的设计文件输入到Slang当中并进行解析，得到其对应的AST. 通过自上而下的方式遍历语法树，收集语法树上所有的断言子树. 值得注意的是，由于SystemVerilog存在层级嵌套关系，一个模块当中可能存在多个被实例化的子模块，一个含有断言的子模块也可能被多个模块所实例化. 此外，不同层级之间也可能存在重名等问题. 因此，为了维护断言与待监测信号之间的关系，需要对当前断言例化的作用域和断言进行记录，以便后续维护断言所需监测的信号层次化名称. 通过此种方式，维护断言所在的作用域内的名称，从而保证连接关系的正确性. 具体伪代码如算法1所示.
算法1. 基于AST解析的断言收集算法.
输入：RTL代码的AST根结点ASTnode与根路径$root；
输出：所有断言表达式的子树根结点与其所在路径构成的二元组的集合S.
① GatherAssertions(ASTnode, path)；
② S←{}；
③ if ASTnode is Module then
④ foreach subNode of ASTnode do
⑤ S←S∪GatherAssertions(subNode, path.join (subNode.instanceName))；
⑥ end for
⑦ else if ASTnode is Assertion then
⑧ S.insert(<ASTnode, path>)；
⑨ end if
⑩ return S.
算法1以AST根结点和SystemVerilog语言中定义的根路径为输入. 根路径代表了一个设计当中的顶层模块. 断言提取工具将AST上所有的断言子树进行提取构成一个断言集合，集合中的每一个元素称为一个断言实例，代表一个被设计代码例化的断言表达式. 每个表达式都排除了其与环境的关联，只包含表达式内部的结构. 以图3所示的SystemVeilog断言表达式为例. 对于这个表达式来说，断言形式会被表示为图3中的树形结构，即一个表达式子树.
对每个断言实例分别进行硬件化的任务由断言转化工具完成. 断言转化工具主要负责维护节点信息与连接关系. 由于各个节点之间存在较大的差异：节点本身的结构不同，节点本身代表的断言语义也不同，因此，每种类型的节点生成都有专门的处理方式. 按照处理方式的不同，断言节点大致可以被划分为2个大类，分别是代表表达式中间结果的非叶子节点InternalNode和代表待监测信号和常量的叶子节点LeafNode.
对于叶子节点，断言转换工具提取该节点对应的变量位宽，对于待监测信号则记录其信号名称. 常量在更高层节点的处理当中会进行简单的常量传播优化，将一些不必要的子表达式进行剪枝，降低硬件的开销.
非叶子节点的处理相对较为复杂. 在断言子树中，一个非叶子节点可能代表SystemVerilog中的多种运算符，包括4类：采样函数（sample function）、序列（sequence）、属性（property）相关的操作符，以及SystemVerilog中的基本运算符，如逻辑运算、移位运算、关系运算和四则运算. 从节点对应的运算符是否可被综合，可以将所有的非叶子节点归类为可综合节点和不可综合节点. 对于可综合节点，算法仅需要将对应的子树进行扁平化即可；而对于不可综合节点，则需要将对应的子树替换为一个等价的RTL模块.
算法2. 单个断言实例的硬件化算法.
输入：一个断言实例对应的表达式子树的根节点；
输出：实例化的断言与断言顶层信号.
① EvalAssertions(ExprNode)；
② if ExprNode is LeafNode then
③ NodeInfo← GenLeafNode(ExprNode)；
④ return NodeInfo；
⑤ else if ExprNode is InternalNode then
⑥ SubNodeInfoSet←{}；
⑦ foreach subNode of ExprNode do
⑧ subNodeInfo←EvalAssertion(subNode)；
⑨ subNodeInfoSet.insert(subNodeInfo)；
⑩ end foreach
⑪ NodeInfo ← GenInteralNode(ExprNode, subNodeInfoSet)；
⑫ return NodeInfo；
⑬ end if
以图4中的断言实例对应的语法树为例，对其中的$rose表达式的操作过程介绍如下：断言转化模块会自上而下递归访问整个表达式子树，自下而上地构建表达式，对于叶子结点a，这是一个待监测信号，转化工具会记录路径，为后面连接工作做准备，程序会返回a的信号名和位宽信息到RoseExpr节点的转化程序当中，该节点的转化程序会调用硬件库当中的$rose函数对应的RTL模块，并对该RTL模块进行实例化，指定其连线与参数，例化中间模块时需要利用子节点返回的信息隐式推断出当前模块的参数RoseExpr，例化完成后会以类似的形式将该模块的结果输出到上一层中代表交叠蕴含（overlapped implication）运算的Overlapped Implication进行处理，过程类似，不再赘述.
每一个断言实例都会被转化为一个逻辑等效的硬件模块，这样一个模块被称为一个硬件断言单元，包含着表达式需要监测信号的所有接口，记录当前断言状态的信号匹配（match）与失败（fail）以及必要的时钟与复位信号，match和fail展示了当前的断言状态，后续将会由断言数据收集平台进行记录供验证人员访问.
3.2 硬件化断言算子库
硬件化断言的核心步骤是对不可综合的运算符进行自动识别、替换，并将其转换成语义等价的可综合RTL实现. 这一系列的可综合实现被称为硬件断言算子. SystemVerilog断言中支持的序列操作符和属性操作符种类繁多，同时还包括供形式化验证工具使用的运算符. 因此，本文面向处理器的功能验证需求，针对4类的操作符，实现了其对应的操作符：
1）采样函数. 包括$rose，$past，$fell等；这些运算符主要用来对设计中的一些信号进行采样和行为检测. 其中$past是其中最为基础的采样函数，原则上其他的采样函数都可以由$past导出，采样函数提供了方便的接口去采样一个信号过去未来的值，对于处理器设计中的信号变化、状态转移，都可以通过采样函数进行描述.
2）序列操作符（sequence operator）. 包括and，or，intersect等，这些运算符主要对2个时序序列进行与或操作. 与简单的布尔变量的与或运算不同，2个序列的评估并非1个瞬时可以完成，往往需要多个周期、序列操作符.
3）延时与重复. 包括延时操作符##和重复操作符[*n]. 延时操作符在SVA标准中被称为序列连接（sequence concatenation）操作符，其后的操作数指定了前后2个序列的评估时序关系，## 1表示其后的序列在其前面的序列结束后1周期开始评估，##[1:2]则指明了多种可能的序列. 重复（repetition）操作符则表示一个序列会重复若干次. 延迟与重复在SVA标准中都属于序列操作符，但由于延迟与重复的操作在基于SVA的验证中使用太过广泛，因此，本文将其独立出来作为单独的一类. 延时与重复操作符以一种类似正则表达式的形式将若干信号的时序行为表示出来. 例如a ##1 b[*5]描述了信号a使能后，一周期后信号b会使能5个周期.
4）属性操作符. 包括非交叠蕴含|->和交叠蕴含|=>. 蕴含操作符描述了一种条件关系，即蕴含操作符的起因序列（antecedent sequence）匹配时，会对其结果序列（consequent sequence）进行判断，只有当起因序列匹配且结果序列不匹配时，蕴含才判定为假. 例如a |-> b这样一个断言，a是其中的起因序列，b是其中的结果序列，当信号a为真时，信号b也应当为真. 交叠蕴含与非交叠蕴含的区别在于前者的结果序列评估开始于起因序列评估结束后的一个周期，而后者的结果序列评估与起因序列评估的结束同时发生. 蕴含操作符同样在处理器设计的验证中应用非常广泛，因为验证者很多情况下会关注某一条件下的处理器行为，这类行为很容易通过蕴含操作符表示.
硬件算子繁多而复杂，但是不同的硬件算子满足着相同的基本设计规律. 以下主要讨论硬件断言算子的基本结构，以及断言输入输出的形成.
从实现的思路上来说，不同的硬件断言算子都可以被视为一个有限状态机. 每一个运算符会维护其运算状态，用于记录正在等待子节点所代表的断言算子结果或正节点中处于计算当中的待运算任务以及判断最终的计算结果. 不同的运算符状态机通过使能与反馈机制将各个运算符联合成一个有机整体共同实现完整的断言功能.
从输出结构来说，大多数硬件断言算子采用了 match，fail信号组作为输出，用以描述断言表达式的结果. 这一组输出被称为断言标准输出. 由于SVA断言是一种基于时序逻辑的断言描述方式，其描述的断言往往不能在当前周期就完成断言表达式结构的计算，甚至计算周期不是固定的，因此，断言表达式的结果并不是一个非对即错的二值逻辑，还存在处于计算当中的中间态. 因此，match信号标志着一个表达式或子表达式出现了匹配，即一次对断言的评估尝试结束并且与断言所描述的行为相符. 而fail信号则相反，若断言的一次评估尝试结束但被监测信号的行为与硬件预期不相符，则会出现fail. 一个完整的断言表达式同样采用标准输出，一个断言表达式的结果就是最顶层硬件化断言算子的输出.
断言的输入通过采样函数来完成. 采样函数是硬件算子库中一类特殊的操作符，负责对输入信号或输入信号组成的组合逻辑信号进行采样并进行一系列基本的运算. 例如，$rose，$past函数通过对输入信号进行采样，计算其当前值相对于前一周期是否发生上升或下降，从而生成相应的match和fail信号. 采样函数中还有另一类纯粹的采样函数，这类函数只负责对当前的信号值进行采样，而不进行额外的逻辑运算，如$past，$sample，其中$past函数会采样某个信号若干周期前的值，这一类采样函数则不采用标准输出，而是此前将某周期的信号值进行输出，并将其作为其他算子的输入进行下一步运算. 除了SVA中支持的标准采样运算符之外，本文还给出了一类自定义的特殊采样函数signal_check，主要用于将一个组合逻辑表达式转化为标准输出. 对于一个只包含组合逻辑表达式的断言，如@(posedge clk) a &b; signal_check能保证该断言与其他断言的结构同一性. 对于一个时序逻辑断言的组合逻辑部分，也需要通过signal_check将其进行转化，以使得该断言表达式的结果可以作为其他断言操作符的输入.
为进一步阐述断言算子的内部结构及外界互联关系，以“|->”运算符为例进行具体阐述. 从端口上看，该断言包含3个部分，分别是连接前因序列的标准输出、连接结果序列的标准输出和使能，以及该模块的标准输出. 当起因序列的评估结束后，对断言的评估转移至“|->”运算符，该运算符将会使能，若结果为match信号使能，则该运算符会使能后继运算符进行评估，在后继节点完成计算后，输出本节点的评估结果. 由于一个序列的评估可能耗费多个周期，而在后继序列进行评估的过程中，也可能存在前因序列因为一次不同的断言评估请求而产生新的评估操作，运算符内支持对于一定时间内已发出的对后继断言的评估操作进行记录，并内部维护这些评估操作的时序关系，以便正确地产生结果.
从方法学的角度，验证可分为基于动态方法的功能仿真验证和基于静态方法的形式化验证. 这2种方法都会使用断言的方式进行验证实现，但二者常使用的运算符不同. 本文是基于FPGA加速的仿真方法，因而针对开源项目中基于仿真的功能验证需求进行调研，归纳得到表1中的13种运算符. 对于不在表1中的断言操作符，本文工具尽管不能直接将其转化为对应的硬件电路，但仍支持对于该部分的断言符号识别，当识别到该类运算符时会对用户进行报告. 本文最终支持共计包括隐式调用的signal_check在内的14种操作符，可以覆盖处理器功能验证的基本需求.
表 1 已支持的硬件化断言算子Table 1. Supported Hardware Assertion Operators硬件算子类型 硬件算子名称 算子使用示例 采样函数 $rose
$fell
$stable
$past$rose(a)
$fell(a)
$stable(a)
$past(a)序列操作符 and
or
intersect
first_matcha and b
a or b
a intersect b
first_match(a)属性操作符 |=>
|->
if … elsea |=> b
a |-> b
if (a) b else c延迟与重复 ##
[*]a ## 1 b / a ##[1:2]b
a[*2]/a[*1:2]b3.3 硬件化断言方法
断言是一种重要的测试手段，而断言是否触发，则是一种重要的测试指标. 以往的工作往往忽略了断言触发结果的获取，未将其作为一个指导验证过程的指标.
如3.1节所述，每一个硬件断言单元会给出断言的触发与失败状态，断言的触发，即match信号使能，标志着当前的断言所描述的行为是设计中实际会出现的行为，断言的触发与否同样是一种测试充分性的指标，称为断言覆盖率. 本文扩展了基础的断言覆盖率，从断言覆盖与否转为断言覆盖的次数：通过将一个断言单元的match信号与一个计数器相连，通过计数器数值反映测试进展. 各个断言对应的计数器构成断言计数器组，而当断言失败，即fail信号使能，则表示断言所描述的行为与实际设计运行行为不符，需要检查设计或断言当中是否存在错误. 一个断言单元的fail信号连接到上位机的中断控制器上，以及时地向上位机反馈当前断言的运行状况. 所有的断言会被编号，而触发失败的断言会被记录在相应的寄存器当中供上位机的中断处理函数读取访问，如图5所示.
为了向上位机提供简单的访问界面，本文提供了一个根据地址索引访问断言数据的简单协议，在断言数据区域的地址空间范围内，上位机可通过地址索引对该模块进行访问. 断言数据平台的数据流结构如图6所示. 断言数据区域除了断言计数器组和断言失败记录，还有性能计数器用于生成断言触发的时间戳以及进行性能方面的比较. 具体的地址映射关系如表2所示.
表 2 断言数据地址分配Table 2. Address Mapping of Assertion Data地址 地址段功能 寄存器宽度 0x0000-0x0fff 触发计数器 16 0x1000 断言失败记录 32 0x1004 性能计数器低位 32 0x1006 性能计数器高位 32 本文设计基于软硬件协同仿真，将DUT映射到FPGA上，并通过FPGA与上位机的数据交互通路实现硬件仿真过程、测试覆盖程度、断言触发情况的监测. 由于对断言状态的访问数据量小，本文设计对于上位机的性能、架构、数据通路协议、带宽没有特定要求. 本文的具体实验环境将在第5.1节进行了详细介绍.
本文实现了一个基于AMD ZYNQ SoC（System on Chip）的具体用例，设计了一个端到端的硬件断言平台. 一个AMD ZYNQ片上系统由2部分组成，其中的处理系统（processing system, PS）充当上位机，与FPGA部分，即可编程逻辑（programmable logic, PL）通过AXI接口进行交互，用户可以通过相应的软件读取到硬件上的断言数据信息.
4. 基于断言的RISC-V处理器核功能验证
4.1 实例分析：开源RISC-V处理器核的功能验证
为了对提出的硬件化断言的有效性和高效性进行全面评估，本文选取了一款开源RISC-V处理器核：果壳处理器（Nutshell）[20]作为待验证设计和实验对象. Nutshell是一个基于RISC-V架构的64位处理器，使用Chisel[21]语言进行开发，支持RISC-V的I，M，A，C，Zicsr与Zifencei的指令扩展和M，S，U特权级. Nutshell支持分支预测、多级缓存，可以运行Linux/Debian系统.
4.2 针对特定微架构处理器的断言集合
本文设计的断言分为两大类：一类断言是基于RISC-V架构或者通用总线标准的断言，这类断言和待验证设计的微架构细节无关，也并非针对Nutshell设计，并且可以被快速迁移到其他采用相同指令集或总线协议的设备上. 另一类断言则聚焦于与处理器核微架构相关的行为，意在展示断言针对处理器微架构的验证能力.
断言覆盖的内容包括处理器的缓存、分支预测器、总线协议、特权寄存器行为等，具体如表3所示. 这些断言展示了针对标准断言的可扩展性，也展示了断言本身所具有的贯通各个抽象层级的验证能力.
表 3 断言类型与数量Table 3. Type and Amount of Assertions断言类型 断言子类型 数量 属性来源 AXI Assertion KEEP STABLE 29 Standard INVALID WHEN RESET 10 Standard TIME_OUT 1 Standard RESERVE SIGNAL 2 Standard CSR Assertion TRAP 5 Standard RET 6 Standard EXCEPTION PIRORITY 4 Standard BPU Assertion 4 Design Spec Cache Assertion 3 Design Spec Regfile 1 Standard 4.3 断言嵌入方法
为了解决Chisel转化后的Verilog文件可读性较差、难以进行验证的问题，本文采用了Chisel中的黑盒（blackbox）机制，通过黑盒可以在Chisel当中以模块的形式调用SystemVerilog设计的断言. 基于黑盒的方法可以在Chisel层面连接断言与设计，以保证断言能够正确地监视信号.
为了对比Nutshell在加入和去除断言后在硬件上的性能差异，以及基于硬件化断言的验证方法与Xilinx的ILA这样一种传统FPGA 调试方式的资源占用对比，本文采用了参数化的设计方法，通过调整传入到Chisel的编译器参数，设计可以在无断言模式、断言模式、ILA模式间直接进行切换. 其中ILA模式通过Chisel内置的BoringUtil和参数化端口将处理器内部的信号飞线至顶层模块，主要用于与传统的ILA模式进行对比.
5. 硬件化断言平台上的RISC-V处理器核功能验证
本节主要对于面向RISC-V处理器核Nutshell的硬件化断言平台进行评估. 本文通过硬件化断言平台的工具支持，将第4节中提到的断言集合进行硬件化，并与Nutshell设计相连，构建了完整的面向RISC-V处理器核的硬件化断言平台，并通过一系列的实验完成3个问题的回答：1）整个测试在何种平台上完成？ 2）将断言与RISC-V处理器核相连后，是否能够有效地对Nutshell进行验证； 3）硬件化断言平台在资源占用、运行效率方面表现如何?
5.1 实验平台
本文的软件测试运行在一台拥有11th Gen Intel Core i9-11700 CPU, 32 GB 3200MT/s的内存的机器上. 操作系统为Ubuntu 22.04，运行Modelsim 2020.4作为仿真后端.
本文的硬件部分将Nutshell部署在Fidus Sidewinder开发板上，其上的SoC芯片是AMD ZYNQ UltraScale+ XCZU19EG SoC，该芯片包括一块拥有114.3万逻辑单元的大容量FPGA（PL端）和4核ARM Cortex-A53处理器（PS端）.
5.2 软件平台上的RISC-V处理器核功能验证
为了对比硬件化断言在验证效率上的提升，本文以软件仿真器为基线进行评估. 首先在软件平台上运行Nutshell，并提供一致的断言集合.
为了能够运行SystemVerilog断言，本文选取了Modelsim作为软件测试平台. 相对于不支持断言或只支持简单断言的开源仿真器Verilator和Icarus Verilog，Modelsim支持更为完整的断言功能，因此本文选取Modelsim作为仿真器比较的基线. 由于Modelsim在运行时本身不会记录实际的仿真时间，本文额外使用VPI机制记录仿真开始和结束的时间戳，以精准地测量仿真的时间.
另外，为了能够在一定程度上确认断言是否能找到处理器内核中的错误，本文在Nutshell的代码中植入了若干人为设计漏洞，如针对于寄存器堆和分支预测器的逻辑错误等. 这些人为植入的漏洞可以通过参数化选项在编译时选择开启或关闭. 实验中；为了对RISC-V处理器核进行功能验证，本文选取了一系列常用的通用基准测试（Benchmark）程序作为处理器的工作负载，包括Coremark[22]，Dhrystone[23]，Microbench[24]，其中，Microbench包括10个子测试程序，如qsort，bf，lzip，md5等. 本文实验选取了每个基准测试的前1 000 000条指令执行.
从实验结果来看，在功能方面，人为插入的断言均能被硬件化断言检测到；而在性能方面，在软件Modelsim当中以不同的基准测试作为测试负载，Nutshell的仿真时间平均为456.16 s. 实验过程中记录了仿真过程中的周期数，通过将周期数与总共花费的时间做比值，可以得到软件仿真的仿真频率，Nutshell的仿真频率为4~7 kHz左右. 具体的结果如表4所示.
表 4 软件仿真Nutshell运行各基准测试结果Table 4. Testing Results of Each Benchmark Run by Software Simulation Nutshell基准测试 运行时间/s 周期数 仿真频率/kHz coremark 371.42 1858853 5.005 dhrystone 437.63 2143378 4.898 microbench-qsort 463.21 2369069 5.114 microbench-queen 360.46 1821639 5.054 microbench-bf 448.01 1967435 4.392 microbench-fib 390.40 2639506 6.761 microbench-sieve 485.60 3174664 6.538 microbench-15pz 457.99 2585612 5.646 microbench-dinic 539.19 3412524 6.329 microbench-lzip 510.03 3796330 7.443 microbench-ssort 495.73 3109954 6.273 microbench-md5 514.30 4066747 7.907 实际上，1 000 000条指令相较于动态指令数的规模而言只占很小的一部分. 以coremark为例，完整运行coremark程序需要总共运行353 976 300条指令，是目前运行的测试集指令数的354倍. 以现有的仿真频率运行，大约需要一天半的时间. microbench的md5测试程序的指令数高达6 576 597 538条，在现有仿真频率下需要39天才能完整运行完. 另外，在运行仿真的过程中，Modelsim的波形输出被全部关闭，如果发生错误，Modelsim没有任何对错误的回溯能力. 如果打开波形输出的开关，仿真器的性能还会进一步降低.
5.3 硬件化断言平台上的RISC-V内核的功能验证
为了验证硬件化断言平台的验证效率，本文将5.2节中软件运行的断言集合进行硬件化，与Nutshell一起部署在FPGA平台上，部署结果如图7 所示. 硬件FPGA将Nutshell默认配置在100 MHz的情况下进行，对其运行时间进行了测试，运行时间通过记录的运行周期数除以时钟频率得到.
本文对比了硬件化断言平台相对于软件仿真运行相同基准测试的时间，通过计算相同的指令数量下，硬件与软件的运行时间占比来计算加速比，具体结果如图8所示. 不同的基准测试的加速比不同，其范围是13 424~22 589，几何平均数为17 858. 即，软件需要运行几天甚至几周的基准测试程序，硬件只需要跑几分钟就可以得到结果. 如果为软件仿真器提供基本的调试能力，如波形导出，其速度还将进一步下降，这一加速比还将继续提升.
![]()
图 8 FPGA仿真相对于软件仿真加速比Figure 8. Acceleration ratio of FPGA simulation compared with software simulation传统的验证调试主要采用ILA等基于信号记录缓冲的方法，为了与传统的ILA的方式进行对比，比较硬件化断言的额外资源占用，本文同时测试了基于ILA的调试方式的面积资源占用.
在工程实践当中，常常会面临通过ILA设计内部行为逻辑检查的需求，因而本文设置了实验对断言方式的资源占用进行有效说明：通过ILA方式与断言对相同功能进行检查. 为此，本文通过Vivado工具链将所有原本被断言监视的信号与ILA相连. ILA通过接出的信号进行离线检查，而断言进行在线检查. 本文配置了不同的ILA深度，包括1024和65536这2种配置，具体的资源占用如表5所示. 为了对比，表5中同时列举了Nutshell部署在FPGA上本身所消耗的资源数量作为一个基准参考.
表 5 硬件断言与ILA的资源占用量和资源占用比Table 5. Resource Usage and Resource Usage Ratio of Hardware Assertions and ILA资源类型 硬件断言 ILA（配置1） ILA(配置2) 果壳处理器 LUTs 1223 (0.23%) 2266 (0.43%) 3749 (0.72%) 41537 (7.95%) Registers 933 (0.09%) 3833 (0.37%) 4243 (0.41%) 53273 (5.1%) BRAMs 0 (0%) 8 (0.81%) 512 (52.03%) 56 (5.69%) DSPs 0 (0%) 0 (0%) 0 (0%) 16 (0.81%) 注：括号内部的资源占用比表示该类型资源用量与FPGA片上资源总量的比值. 可以看到，硬件断言相对传统的ILA方式，占用的资源更小. 其中，硬件化的断言几乎不耗费BRAM资源，这是由于硬件化断言并不需要保存过去运行状态的全部过程，只需要捕捉关键信号和关键逻辑的出错现场即可. 反观ILA，它需要通过信号记录缓冲机制保存运行时信息，即使这些信息对于调试并无帮助，甚至会成为系统的资源瓶颈. 比如，深度为65 536的ILA仅能监测6万个周期的设计状态，使用的BRAM资源却超过了片上该资源总量的一半，这一数量甚至远远超过Nutshell本身所使用的BRAM资源数量.
传统的基于ILA调试方法中，设计者往往会在可能出错的点位附近设置ILA的记录触发器，然后观察可能出错点位前后的信号状态以确定错误. 然而，真正导致设计错误的只有很短时间内的异常行为，因此，ILA的记录中含有大量冗余信息. 与之对比，断言可以更精准地定位错误的位置，并且内嵌了对于设计行为的描述，所以断言不需要额外的记录，因此硬件断言相对于传统的ILA方式消耗的资源用量更小.
相对于传统的FPGA原型验证方式，ILA和断言由于在设计上插入了新的硬件单元，对于FPGA编译过程中的综合与布局布线等步骤会产生一定的影响，进而影响系统时序的收敛. 但如果新加入的硬件单元不在系统的关键路径上，则对时序的影响较小. 为验证此问题，本文利用Vivado工具对实现后的设计时序进行分析，对处理器所在时钟域下的时序裕量进行测量，并计算其理论最大频率fmax. 实验结果表明，ILA的fmax值为169.43 MHz而断言的fmax值是172.08 MHz，因此可以认为二者对于时序的影响差异较小. 此外通过检查时序报告发现，整个设计的关键路径并不在处理器或者断言实现，而在待测处理器之外用于模拟外界环境的外设，因此ILA和断言对于完整工程的时序都无明显影响.
6. 其他硬件化断言工作
在本文之前，国际上也有一些学者对断言的硬件化做了研究，然而，这些工作既没有开放其源代码也没有开放其设计的硬件化断言工具，无法定量地进行横向对比. 因此，本节根据这些工作的描述，主要讨论本文与此前工作在设计思路、技术选型上的不同.
Pellauer等人[16]提出了一种将SVA转换成Bluespec SystemVerilog的方法，支持了较为完整的SystemVerilog断言运算符，然而，该工作对于常用的采样函数如$rose，$past等没有支持. 从实现上来说，该工作以一个Sequence/Property表达式为建立状态机的基本单元，对于SVA中的多种可能的执行路径采用对Property状态机复制的方式来实现.
Das等人[17]的工作支持的运算符相对更少. 实现上来说，该工作以延迟/重复/基本布尔逻辑为基础模块，在此基础上构建出复杂的断言实现. 对于每个Sequence操作符，只提供一个match信号用于标注断言匹配，对于断言失败的情况，则是通过对Sequence表达式进行逻辑取反等价变换，对变换后的表达式生成一个额外的断言硬件模块进行检测. 对于推测路径，Das等人也采用了复制所有执行路径的状态机的方法.
Kastelan等人[18]的工作在支持运算符上同样比较少. 实现上来看，他们的工作同样需要额外的逻辑用于计算断言失败的情况. 另外，对于推测路径的处理没有太多涉及.
本文工作面向功能验证的需求，实现了足够多的断言运算符. 从实现上说，本文工作以运算符作为基本单元，每个基本单元存储了必要的信息来维护正在进行中的断言计算以解决推测执行问题. 文献[16-18]的工作除了断言本身实现与本文工作不同外，这些工作都仅仅聚焦在断言单元的实例化. 对于断言提取、连接、数据收集都没有关注，不能形成真正完整的断言工具链.
7. 结 论
本文聚焦于处理器验证中的实际问题，针对果壳处理器（Nutshell）这一个具体的处理器实例，根据待验证处理器的具体功能设计了一组断言进行验证.
断言是一种贯穿设计各层级的非全局建模方法. 相对于传统的ILA等方式，硬件化断言提升了FPGA原型验证中的信号可见性，大大提升了验证的有效性与高效性，能够帮助开发者在验证过程中更好地发现错误、定位错误. 通过断言的方式，本文针对一个RISC-V内核的ISA级和μARCH级的行为进行了验证，确认断言方法能够有效发现和定位处理器当中的错误.
面向处理器功能验证的需求，本文提供了一个SystemVerilog断言子集的硬件化方法，将原有的软件断言以更高效的形式运行在硬件上. 同时提供了硬件断言的断言触发情况收集平台，让硬件验证人员可以有效地对测试进度与设计异常进行监测.
通过对于硬件化断言平台的实验可以看到，本文相对于软件断言有着高达2万倍的加速比，极大提升了验证效率. 断言提供了细粒度的可见性和自检查能力，很好缓解了FPGA本身信号可见性不足的问题. 相对于ILA等传统FPGA调试方式，本文提出的方法也有更高的调试效率.
当然，目前的硬件断言平台与特定RISC-V内核的验证需求息息相关，如果未来要向更为实际的应用场景中迁移，还需要进一步地丰富硬件化断言的转化工具链. 另外，在功能性验证方面，单纯依靠断言很难做到全面，仍然依赖于基于模型检查的方法进行补充.
作者贡献声明：张子卿完成了设计的实现和论文的撰写；石侃对论文的实现与撰写进行了指导；徐烁翔协助完成实验平台的搭建和部分实验数据的测量；王梁辉协助完成了硬件断言算子库的设计；包云岗提出指导意见.徐烁翔和王梁辉在中国科学院计算技术研究所实习期间完成本文相关工作.
-
表 1 原子性违反的访问交错模式
Table 1 Access Interleaving Pattern of Atomicity Violation
序号 模式 描述 1 {ep:R(x)er:W(x)ec:R(x)} 2个连续的读访问被中断的写访问打断. 2个对同一内存的连续读访问预期读到相同的值, 而交错的写访问打破了该预期. 2 {ep:R(x)er:W(x)ec:W(x)} 连接在读访问之后的本地写访问被中断的写访问打断. 写操作依赖于本地读操作读到的值（例如, 本地写访问依赖于本地读访问相关的分支条件）, 而交错的写访问修改了该值. 3 {ep:W(x)er:R(x)ec:W(x)} 2个连续的写访问被中断的读访问打断. 本应不对外可见的中间结果被交错的读访问获取并使用. 4 {ep:W(x)er:W(x)ec:R(x)} 连接在写访问之后的本地读访问被中断的写访问打断. 读访问预期读到本地的赋值, 而交错的写访问修改了该值. 
下载: 导出CSV
表 2 共享数据访问方式与访问粒度
Table 2 Access Modes and Access Granularities on Shared Data
访问方式 整体 元素 成员 位 合计 全局变量名 44 9(4*) 7 12 72(4*) 指针 6(2*) 0 0 1 7(2*) MMIO 1 1(1*) 0 1 3(1*) 合计 51(2*) 10(5*) 7 14 82(7*) 注：(*)表示共享数据访问的偏移量不是常量, 例如BRCST_buf[i].
下载: 导出CSV
表 3 不同数据类型表现形式
Table 3 Representation of Different Data Types
数据类型 数据名称 Base Offset Size Mode ConstAccess 标量类型 func_run func_run {0} 1 read true 聚合类型 upload_data[i] upload_data {0,4} 4 write false MMIO *((unsigned int*) addr) ADDR_ZERO {0xff00} 4 read true
下载: 导出CSV
表 4 被分析的真实航天软件项目
Table 4 Analyzed Real-world Aerospace Software Projects
序号 项目 描述 代码行数 1 module1 某电源供应器控制软件 2275 2 module2 某推进控制软件 970 3 module3 某热控软件 1701 4 module4 某遥测和指挥软件 2380 5 module5 某姿态控制软件 5099 6 module6 某电源控制软件 3767 7 module7 某CPU软件 1544 8 module8 某推进线路盒软件 4015
下载: 导出CSV
表 5 基准测试集检测结果
Table 5 Results of Benchmark
序号 代码
行数中断
个数共享数
据个数原子性违
反个数Rchecker intAtom-S #WN #TP #FP 时间/s #WN #TP #FP 时间/s 1 65 2 3 1 2 1 1 0.3 2 1 1 0.203 2 46 2 2 1 2 1 1 0.47 2 1 1 0.093 3 74 2 4 1 2 1 1 0.51 1 1 0 0.484 4 69 2 9 1 3 1 2 0.31 1 1 0 0.375 5 47 1 2 1 3 1 2 5.2 1 1 0 0.125 6 54 1 3 1 2 1 1 0.31 1 1 0 0.266 7 51 1 2 1 11 1 10 0.37 1 1 0 0.328 8 53 1 2 1 2 1 1 0.32 2 1 1 0.375 9 48 1 3 3 2 2 0 0.34 3 3 0 0.156 10 54 1 2 1 1 1 0 0.32 2 1 1 0.125 11 44 1 4 1 1 1 0 0.28 1 1 0 0.078 12 35 1 2 1 1 1 0 0.31 1 1 0 0.031 13 67 3 4 1 2 1 1 0.45 2 1 1 0.203 14 60 3 4 1 2 1 1 0.36 2 1 1 0.156 15 41 1 2 1 1 1 0 0.31 1 1 0 0.094 16 34 1 1 3 3 3 0 0.36 3 3 0 0.063 17 42 1 2 5 5 5 0 1.81 5 5 0 0.109 18 65 2 2 3 3 3 0 0.36 3 3 0 0.109 19 66 1 8 1 2 1 1 0.37 1 1 0 0.531 20 55 2 3 1 3 1 2 0.32 1 1 0 0.172 21 81 1 6 3 3 3 0 0.35 3 3 0 0.578 22 67 1 4 4 6 4 2 0.34 4 4 0 0.219 23 40 1 1 2 2 2 0 0.3 2 2 0 0.063 24 65 1 3 1 1 1 0 0.141 25 39 1 2 1 1 1 0 0.31 1 1 0 0.078 26 44 2 1 2 1 1 0 0.29 2 2 0 0.062 27 49 3 1 5 2 2 0 0.32 5 5 0 0.078 28 54 3 2 1 1 1 0 0.41 1 1 0 0.109 29 95 1 3 1 1 1 0 1.4 1 1 0 0.359 30 57 3 2 1 2 1 1 0.35 1 1 0 0.109 31 92 1 7 3 3 3 0 0.31 3 3 0 0.21 合计 1753 48 96 54 75 48 27 17.76 60 54 6 6.082 准确率 88.9% 100% 误报率 36% 10% 平均时间/s 0.592 0.196 注：#WN表示报告的缺陷数量；#TP表示正报数；#FP表示误报数.
下载: 导出CSV
表 6 真实中断驱动型航天嵌入式软件检测结果
Table 6 Detection Results of Real-World Interrupt-Driven Aerospace Embedded Software
项目 代码
行数中断
个数共享数据分析 模式匹配 路径裁剪第1阶段 路径裁剪第2阶段 #FP 总时间/s 时间
占比/%数据
个数时间
占比/%违反
个数时间
占比/%违反
个数减少
比例/%时间
占比/%违反
个数减少
比例/%module1 2275 3 8.7 72 23.5 289 22.3 123 57.4 45.4 10 96.5 1 114.7 module2 970 3 1.8 52 4.9 376 1.9 194 48.4 91.4 6 98.4 1 136.7 module3 1710 2 21.3 81 37.7 201 27.7 125 37.8 13.3 6 97.0 0 30.0 module4 2380 2 33.5 222 56.4 334 4.9 179 41.5 5.2 2 99.4 0 185.7 module5 5099 5 5.9 16 87.8 15 12.5 6 60.0 0.2 2 86.7 0 58.9 module6 3767 2 32.9 94 36.6 183 21.7 101 44.8 8.7 8 95.6 2 169.9 module7 1544 2 23.0 26 54.4 88 12.7 62 29.5 9.9 1 98.4 0 28.1 module8 4015 2 5.5 83 36.1 418 7.9 311 25.6 50.5 10 97.6 0 304.7 总计 1904 1101 42.2 45 97.6 4 平均值 15.9 37.8 11.1 35.2 注：#FP表示误报数.
下载: 导出CSV
表 7 intAtom-S与intAtom有效性及效率对比
Table 7 Comparison of Effectiveness and Efficiency Between intAtom-S and intAtom
项目 intAtom intAtom-S 时间/s #FP 时间/s 额外开销 #FP module1 104.7 2 114.7 9.6% 1 module2 134.3 1 136.7 1.8% 1 module3 23.6 3 30.0 27.1% 0 module4 123.5 1 185.7 50.4% 0 module5 55.4 0 58.9 6.3% 0 module6 113.9 3 169.9 49.2% 2 module7 21.6 0 28.1 30.0% 0 module8 287.9 1 304.7 5.8% 0 合计 11 4 注：#FP表示误报数.
下载: 导出CSV
表 8 共享数据分析结果
Table 8 Results of Shared Data Analysis
项目 static-TSA intAtom-S 共享数据个数 #FP 共享数据个数 #FP module1 43 0 72 0 module2 54 2 52 0 module3 117 36 81 0 module4 232 10 222 0 module5 16 0 16 0 module6 118 24 94 0 module7 26 0 26 0 module8 202 119 83 0 合计 808 191 646 0 注：#FP表示误报数.
下载: 导出CSV
表 9 Naive+RPPS和 intAtom-S 与Naive的时间开销对比
Table 9 Time Cost of Naive+RPPS and intAtom-S Compared with That of Naive
项目 Naive Naive+RPPS intAtom-S 时间/s 时间/s 效率比 时间/s 效率比 module1 193.8 54.3 3.6× 52.1 3.7× module2 331.1 232.0 1.4× 125.0 2.6× module3 10.9 5.6 1.9× 4.0 2.7× module4 81.9 68.4 1.2× 9.6 8.5× module5 0.3 0.1 3.0× 0.1 3.0× module6 56.6 16.3 3.5× 14.8 3.8× module7 9.0 3.9 2.3× 2.8 3.2× module8 397.6 220.9 1.8× 153.8 2.6× 合计 1081.2 601.5 1.8× 362.2 3.0× 注：以Naive为基线，Naive+RPPS或intAtom-S的效率比表示Naive的时间分别和它们的时间的比值.
下载: 导出CSV
-
[1] Sung C, Kusano M, Wang C. Modular verification of interrupt-driven software[C]//Proc of the 32nd IEEE/ACM Int Conf on Automated Software Engineering (ASE). Piscataway, NJ: IEEE, 2017: 206−216
[2] Regehr J. Random testing of interrupt-driven software[C] //Proc of the 5th ACM Int Conf on Embedded Software. New York: ACM , 2005: 290−298.
[3] 中国空间技术研究院软件产品保证中心. 中国空间技术研究院软件质量问题分析报告[R]. 2015 China Academy of Space Technology Software Product Assurance Center. Analysis Report on Software Quality Problems of China Academy of Space Technology[R]. 2015(in Chinese)
[4] 陈睿, 杨孟飞, 郭向英. 基于变量访问序模式的中断数据竞争检测方法[J]. 软件学报, 2016, 27(3): 547−561 Chen Rui, Yang Mengfei, Guo Xiangying. Interrupt data race detection based on shared variable access order pattern[J]. Journal of Software, 2016, 27(3): 547−561 (in Chinese)
[5] Flanagan C, Freund S N, Yi J. Velodrome: A sound and complete dynamic atomicity checker for multithreaded programs[C] //Proc of the ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2008: 293–303
[6] Park S, Harrold M J, Vuduc R. Griffin: Grouping suspicious memory-access patterns to improve understanding of concurrency bugs[C]//Proc of the Int Symp on Software Testing and Analysis. New York: ACM, 2013: 134–144
[7] Park S, Vuduc R, Harrold M J. unicorn: A unified approach for localizing non-deadlock concurrency bugs[C] //Proc of the Software Testing, Verification and Reliability. Hoboken: Wiley, 2015: 167–190
[8] Razavi N, Farzan A, McIlraith S A. Generating effective tests for concurrent programs via AI automated planning techniques[J]. International Journal on Software Tools for Technology Transfer, 2014, 16(1): 49−65
[9] Sorrentino F, Farzan A, Madhusudan P. PENELOPE: Weaving threads to expose atomicity violations[C] //Proc of the 18th ACM SIGSOFT Int Symp on Foundations of Software Engineering. New York: ACM, 2010: 37–46
[10] Wang Chao, Limaye R, Ganai M, et al. Trace-based symbolic analysis for atomicity violations[C] //Proc of the Int Conf on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2010: 328–342
[11] Park S. Fault comprehension for concurrent programs[C] //Proc of the 35th Int Conf on Software Engineering (ICSE). Piscataway, NJ: IEEE, 2013: 1444–1446
[12] Park S, Vuduc R W, Harrold M J. Falcon: Fault localization in concurrent programs[C] //Proc of the 32nd ACM/IEEE Int Conf on Software Engineering. Piscataway, NJ: IEEE, 2010: 245–254
[13] Sadowski C, Freund S N, Flanagan C. SingleTrack: A dynamic determinism checker for multithreaded programs[C] //Proc of the European Symp on Programming. Berlin: Springer. 2009: 394–409
[14] Wang Liqiang, Stoller S D. Accurate and efficient runtime detection of atomicity errors in concurrent programs[C] //Proc of the 11th ACM SIGPLAN Symp on Principles and Practice of Parallel Programming. New York: ACM, 2006: 137–146
[15] Feng Haining, Yin Liangze, Lin Wenfeng, et al. Rchecker: A cbmc-based data race detector for interrupt-driven programs[C] //Proc of the IEEE 20th Int Conf on Software Quality, Reliability and Security Companion (QRS-C). Piscataway, NJ: IEEE, 2020: 465–471
[16] Racebench website. 2019.https://github.com/chenruibuaa/racebench.
[17] Li Chao, Chen Rui, Wang Boxiang, et al. Precise and efficient atomicity violation detection for interrupt-driven programs via staged path pruning[C] //Proc of the 31st ACM SIGSOFT Int Symp on Software Testing and Analysis, New York: ACM, 2022: 506–518.
[18] Wang Boxiang, Chen Rui, Li Chao, et al. SpecChecker-ISA: A data sharing analyzer for interrupt-driven embedded software[C] //Proc of the 31st ACM SIGSOFT Int Symp on Software Testing and Analysis. New York: ACM, 2022: 801−804
[19] Wang Yu, Wang Linzhang, Yu Tingting, et al. Automatic detection and validation of race conditions in interrupt-driven embedded software[C] //Proc of the 26th ACM SIGSOFT Int Symp on Software Testing and Analysis. New York: ACM, 2017: 113–124
[20] Lu Shan, Tucek J, Qin Feng, et al. AVIO: Detecting atomicity violations via access interleaving invariants[C] //Proc of the Int Conf on Architectural Support for Programming Languages & Operating Systems. New York: ACM, 2006: 37–48
[21] Codish M, Mulkers A, Bruynooghe M, et al. Improving abstract interpretations by combining domains[J]. ACM Transactions on Programming Languages and Systems, 1995, 17(1): 28−44
[22] Vaziri M, Tip F, Dolby J. Associating synchronization constraints with data in an object-oriented language[J]. ACM Sigplan Notices, 2006, 41(1): 334−345
[23] DG website. 2021.https://github.com/mchalupa/dg
[24] Shi Qingkai, Xiao Xiao, Wu Rongxin, et al. Pinpoint: Fast and precise sparse value flow analysis for million lines of code[C] //Proc of the 39th ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2018: 693–706
[25] Snelting G, Robschink T, Krinke J. Efficient path conditions in dependence graphs for software safety analysis[C] //Proc of the ACM Transactions on Software Engineering and Methodology (TOSEM). New York: ACM, 2006: 410–457
[26] Huang J. Scalable thread sharing analysis[C] //Proc of the 38th Int Conf on Software Engineering. Piscataway, NJ: IEEE, 2016: 1097–1108
[27] Lu Shan, Park S, Zhou Yuanyuan. Finding atomicity-violation bugs through unserializable interleaving testing[C] //Proc of the IEEE Transactions on Software Engineering. Piscataway, NJ: IEEE, 2011: 844–860
[28] Lucia B, Devietti J, Strauss K, et al. Atom-aid: Detecting and surviving atomicity violations[C] //Proc of the 2008 Int Symp on Computer Architecture. Piscataway, NJ: IEEE, 2008: 277–288
[29] Chew L, Lie D. Kivati: Fast detection and prevention of atomicity violations[C] //Proc of the 5th European Conf on Computer Systems. New York: ACM, 2010: 307–320
[30] Chopra N, Pai R, D’Souza D. Data races and static analysis for interrupt-driven kernels[C] //Proc of the European Symp on Programming. New York: Springer, 2019: 697–723
[31] Yu Tingting, Srisa-an W, Rothermel G. 2012. SimTester: A controllable and observable testing framework for embedded systems[C] //Proc of the 8th ACM SIGPLAN/SIGOPS Conf on Virtual Execution Environments. New York: ACM, 2012: 51–62
[32] Wu Xueguang, Wen Yanjun, Chen Liqian, et al. Data race detection for interrupt-driven programs via bounded model checking[C] //Proc of the IEEE Seventh Int Conf on Software Security and Reliability Companion. Piscataway, NJ: IEEE, 2013: 204–210
[33] Wu Xueguang, Chen Liqian, Miné A, et al. Static analysis of run-time errors in interrupt-driven programs via sequentialization[J]. ACM Transactions on Embedded Computing Systems, 2016, 15（4）: 1−26
-
期刊类型引用(1)
1. 程知，何立新，胡春玲，张新，张琛. 基于SystemC的计算机组成与结构课程总线仿真方法. 电脑知识与技术. 2025(03): 131-133+138 . 
百度学术
其他类型引用(0)
计量
- 文章访问数: 262
- HTML全文浏览量: 40
- PDF下载量: 91
- 被引次数: 1
