© 2026 Journal of Northwestern Polytechnical University. All rights reserved.

RISC-V指令集架构于2010年由加州大学伯克利分校提出并于2016年正式开源以来，以开放性、模块化和易扩展的特性迅速获得全球范围内的广泛关注[1]。据2024年统计数据显示，阿里达摩院RISC-V架构的玄铁处理器出货量已超过40亿颗，预计到2030年基于RISC-V架构的芯片出货量将达到170亿颗，届时将占据全球市场近四分之一的份额。这一开放架构的快速发展为芯片设计带来了前所未有的创新机遇，打破了长期由Intel、AMD和ARM主导的商业处理器架构专利壁垒。

然而，RISC-V架构的广泛应用也伴随着严峻的安全性挑战。现代高性能处理器为了追求更高的计算效率，普遍采用了推测执行、乱序执行、分支预测等复杂的微架构优化技术。这些技术显著提升处理器性能，同时也引入了新的安全风险点。2018年，谷歌安全团队Project Zero公布的幽灵(Spectre)和熔断(Meltdown)2组漏洞[2–3]震惊了整个计算机安全领域，揭示了现代处理器微架构设计中的根本性安全缺陷。幽灵攻击利用处理器的分支预测机制，通过误导推测执行路径访问敏感数据，并利用缓存等微架构侧信道泄露机密信息。

幽灵漏洞的影响范围极其广泛，几乎涵盖了所有采用推测执行技术的现代处理器。更为严重的是，自初始变种公布以来，研究人员不断发现新的攻击变种，如NetSpectre、SgxPectre、RETBLEED等[4–6], 这些变种不仅在攻击技术上更加精细化，还扩展了攻击的适用场景和威胁范围。例如，NetSpectre通过网络数据包实现远程攻击，突破了传统本地攻击的限制；而针对Intel SGX的SgxPectre攻击则表明，即使是硬件级的可信执行环境也无法完全防御此类攻击。

针对幽灵等瞬态执行攻击，业界和学术界提出了多种防御方案，主要包括限制推测执行机制、对机密数据访问限制、防止机密数据流入隐蔽通道、防止从隐蔽通道提取信息以及防止毒化分支预测器等方向[7]。然而，这些防御措施往往存在显著的滞后性，只能在漏洞被发现并公开后才能实施修复，无法弥补已经造成的安全损失。更为关键的是，新型攻击变种经常能够绕过现有的缓解措施，如推测干扰攻击能够绕过InvisiSpec等不可见性防御策略。

在这种背景下，从处理器设计阶段就开始进行安全性验证显得尤为重要。传统的处理器安全验证方法主要包括仿真验证和形式化验证两大类。仿真验证方法通过构建仿真环境和测试向量检测潜在的安全漏洞，但其验证效果高度依赖于测试用例的质量和覆盖范围，难以保证验证的完备性，尤其是在处理复杂微架构行为时容易遗漏边界情况[8]。形式化验证方法虽然能够提供数学上的严格保证，但在处理大规模硬件设计时面临状态空间爆炸等挑战，且现有方法主要针对指令集架构语义层面，缺乏对具体硬件实现细节的考虑[9–10]。

信息流分析技术作为一种新兴的安全验证方法，通过追踪数据在系统中的流动路径并附加安全标签，能够在更高维度评估系统中敏感数据的安全性。门级信息流跟踪(GLIFT)技术将信息流分析应用于硬件设计领域，为每个逻辑门的输入输出信号分配安全标签并建立标签传播规则，能够精确捕获硬件设计中的信息流动特性[11–12]。相比传统验证方法，信息流分析技术具有以下显著优势：能够检测隐式信息流，包括通过控制流和时序变化传递的信息；可以在设计阶段进行早期验证，避免后期修复的高昂成本；提供了统一的理论框架，能够涵盖多种类型的安全威胁。

尽管信息流分析技术在硬件安全验证中展现出巨大潜力，但将其应用于幽灵漏洞检测仍面临诸多挑战。首先，幽灵漏洞涉及多个微架构组件的复杂交互，包括分支预测器、缓存系统、加载存储单元等，需要建立准确的信息流模型来刻画这些组件间的信息传播关系[13]。其次，幽灵攻击的核心在于推测执行路径中的瞬态行为[14]，这些行为在正常功能验证中往往被忽略，需要专门的安全属性来描述和检测。最后，不同的幽灵攻击变种虽然利用了不同的微架构组件，但其攻击机理有共性特征，需要提取通用的安全属性以提高验证方法的适用性。

基于上述分析，本文提出了一种基于信息流分析的RISC-V处理器幽灵漏洞检测方法。该方法的核心创新在于：构建了完整的门级信息流建模框架，能够精确刻画RISC-V处理器微架构中的信息流动特性；通过深入分析幽灵漏洞的攻击机理，提取了3条通用的安全属性，涵盖了推测执行过程中的关键安全风险；结合形式化验证技术，实现了对RISC-V处理器设计的自动化安全验证；基于验证反例构建了相应的攻击方法，验证了检测结果的准确性。

1 幽灵漏洞共性特征分析

1.1 幽灵攻击变种分析

2018年Spectre v1变种公布以来，各类变种不断涌现，如表 1所示。

回顾现有攻击方法可以发现，大多数幽灵类攻击依赖分支预测技术实现数据窃取，其变种的差异主要体现在针对不同分支预测部件的利用方式上。因此，本文对幽灵攻击的变种进行归纳和总结，提炼其共性特征，为安全属性提取提供依据。幽灵攻击(Spectre)的基础是现代处理器中的分支预测机制，这是为提升性能而设计的重要优化技术。然而，分支预测器在推测执行过程中缺乏严格的安全约束，尤其在权限检查和数据访问控制方面。攻击者利用这一特性，通过操控分支预测器使其在推测路径上执行违反程序逻辑的指令，从而间接访问敏感数据。

1.2 攻击流程共性分析

通过对上述变种的深入研究，可以进一步将幽灵攻击完整流程抽象为图 1所示的6个关键阶段。

图1 幽灵攻击流程示意图

1) 准备阶段: 攻击者对目标系统进行分析，识别潜在的漏洞点和相关推测执行机制，将微架构和侧信道状态初始化，为后续的机密信息访问和泄露做准备。

2) 触发指令: 攻击者通过构造特定的输入或指令序列，诱导分支预测部件或预测机制进入错误执行路径，使目标处理器进入瞬态执行窗口。这一阶段是整个攻击的关键触发点。

3) 瞬态指令访问机密数据: 在预测执行路径中，处理器短暂执行攻击者精心构造的指令序列。这些指令虽然在正常执行流程中不会生效，但在瞬态执行中却可以绕过权限或安全检查，访问到原本受保护的机密数据。

4) 传输机密数据: 攻击者通过侧信道将访问到的机密数据传递至其可观测的系统状态。例如，通过缓存命中和未命中行为的时间差来编码数据内容，这是幽灵漏洞进行信息传递的关键机制。

5) 处理器状态回滚: 由于错误的预测执行路径最终会被丢弃，处理器会恢复到其正常状态。然而，虽然架构状态被修复，微架构状态通常不受影响，因此机密数据的泄露已经通过侧信道完成。

6) 获取机密数据: 攻击者分析收集的侧信道信息，重构出机密数据，完成整个攻击过程。

1.3 核心攻击特征提取

1.3.1 推测性访存绕过权限检查

幽灵漏洞的第一个关键特征是推测执行过程中的未授权内存访问。现代处理器的分支预测机制为了提升性能，在推测执行阶段往往缺乏严格的安全约束，特别是在权限检查和数据访问控制方面。图 2展示了攻击者利用这一特性，通过操控分支预测器使其在推测路径上执行违反程序逻辑的指令, 从而间接访问敏感数据。

图2 攻击阶段示意简图

以典型的Spectre-v1攻击为例，攻击者通过多次训练分支预测器，使其错误预测特定路径并触发未经权限检查的访存操作。在推测执行窗口内，边界检查被绕过，允许访问数组边界之外的敏感数据。这种绕过机制是所有幽灵变种的共同基础。

1.3.2 微架构状态传播机密信息

幽灵攻击的第二个核心特征是通过微架构状态变化传播敏感信息。如图 3所示，在推测路径中，虽然指令不会直接影响程序的存储或寄存器状态，但其访问和操作行为会改变缓存、分支预测器、页表缓冲区(TLB)等微架构资源的状态。

图3 推测执行期间敏感信息传播示意图

这种传播机制的共性在于：推测路径上的指令虽然在正常逻辑上被忽略，却对微架构资源产生了隐式影响，为信息泄露提供了基础。例如，在大多数变种中，攻击者通过推测性访存指令，将敏感数据加载到缓存中，从而改变缓存的命中状态。这种行为在幽灵攻击的各类变种中表现得尤为一致。

1.3.3 侧信道泄露机密信息

幽灵攻击的最终目标是将敏感数据泄露给攻击者。不同变种虽然在泄露手段上有所不同，但基本都依赖于侧信道对微架构资源状态的观测。最为常见的方式是利用高速缓存的访问时间差异。推测路径上的访存操作改变了缓存的命中情况，从而影响后续访问同一数据的时间延迟，攻击者可以通过测量这一时间特性推断出敏感数据的内容。

如图 4所示，典型的Flush+Reload攻击流程包括：首先通过Flush指令清空缓存中的目标数据，接着等待受害者程序运行，然后通过Reload操作访问目标地址并测量访问时间，如果访问时间较短，则说明数据已被受害者加载到缓存中, 如果访问时间较长，则说明缓存未命中。通过这种时间差异，攻击者能够推断受害者是否访问了目标数据。

图4 刷新+重载缓存攻击示意图

除了缓存侧信道，还有一些变种通过观察TLB的状态变化、执行路径的时间差异或端口争用方式来泄露信息。无论采用何种侧信道，攻击者的基本思路都是利用微架构资源的状态变化传递信息。

RISC-V处理器虽然在指令集设计上相对简洁，但为了实现高性能，同样采用了分支预测、推测执行等优化机制，因此面临与传统处理器相似的幽灵攻击风险。特别是在高性能RISC-V处理器如SonicBOOM和Xuantie-910中，复杂的微架构设计进一步增加了攻击面。

通过对幽灵攻击机制的逐步分析，其核心特征可以归纳为上述3个主要方面。这种分阶段的特征表明，幽灵漏洞在不同变种中的核心逻辑是一致的，为提取通用安全属性提供了有力依据。

这种基于共性特征的分析方法不仅有助于理解现有幽灵攻击变种的本质，也为识别潜在的未知变种提供了理论指导。随着RISC-V生态的不断发展，预计会出现更多针对该架构的攻击变种，而本文提出的特征分析框架将为应对这些新兴威胁提供重要支撑。

2 基于信息流分析的幽灵漏洞验证

2.1 安全验证框架架构

针对幽灵漏洞检测中传统方法的局限性，本文提出了一种基于信息流分析的RISC-V处理器安全验证框架，并在此基础上定义了专门针对幽灵漏洞的安全属性验证方法。该方法通过构建门级信息流模型，结合形式化验证技术，能够系统性地检测处理器设计中的幽灵漏洞风险。

如图 5所示，安全验证框架包含3个核心组件：门级信息流模型生成、安全属性生成和形式化验证。

图5 处理器设计安全验证框架整体架构图

该框架的工作流程为：首先，将处理器的RTL设计通过逻辑综合工具转换为门级网表；然后，基于预定义的信息流模型库，将门级网表映射为门级信息流模型；根据幽灵漏洞的特征生成相应的安全属性断言；最后，利用形式化验证工具对信息流模型和安全属性进行验证，检测潜在的安全违例。

2.2 门级信息流模型构建

2.2.1 信息流建模理论基础

信息流模型是一种数学化、系统化的框架，旨在抽象描述系统中信息在不同组件间的传递规律与路径。在硬件安全领域，信息的流动与系统的安全性密切相关，任何不符合安全属性的信息流动均可能导致严重的安全隐患。

如图 6所示，门级信息流建模的核心思想是为硬件设计中的每个二进制位分配安全标签，用于表示信息的安全属性及其流动情况。通过跟踪输入标签的传播，观测其他信号的标签变化，若输出标签因输入标签变化，则判定两者间存在信息流动关系。

图6 信息流跟踪技术基本原理

2.2.2 模型构建流程

门级信息流模型的构建流程分为3个步骤。

1) RTL到门级综合: 使用Yosys等开源逻辑综合工具，将处理器模块的RTL描述转换为标准逻辑门组成的门级网表。

2) 信息流模型映射: 基于预构建的信息流模型库，为门级网表中的每个逻辑单元实例化相应的信息流模型。这个过程是自动化的，通过模式匹配将标准逻辑门映射到对应的信息流传播规则。

3) 标签传播网络生成: 根据门级网表中逻辑单元之间的连接关系，结合信息流模型库中定义的标签传播规则，递归构建完整的信息流路径，生成包含原始逻辑和标签传播逻辑的信息流模型。

2.3 幽灵漏洞安全属性定义

基于第1节对幽灵漏洞共性特征的分析，本文提出3条通用安全属性。

属性1  推测性访存指令权限检查保护

该属性确保推测执行过程中的访存指令必须通过严格的权限验证，防止未经授权的敏感信息访问。

该属性的核心逻辑是当推测性执行被激活时，所有访存操作必须设置为机密级别，仅在权限检查通过的情况下才被允许执行，否则默认设置为不可信状态。

属性2  微架构状态传播控制

该属性限制推测路径指令对微架构状态的修改，防止机密信息通过缓存、TLB等微架构资源泄露。

该属性约束只有在分支预测正确时才允许对缓存进行写操作，在推测执行期间缓存访问都被标记为不可信，从而防止推测路径对微架构状态的非法修改。

属性3  微架构状态恢复一致性

该属性确保推测执行结束后微架构状态能够正确恢复，防止推测路径的残留信息被利用。

该属性要求在推测执行激活时，缓存和TLB等微架构状态的变化都是临时性的，在推测执行结束后必须完全恢复到执行前的状态。

2.4 安全属性实例化

在通用安全属性的基础上，将相关属性转化为适用于特定模块的具体属性定义，是安全验证的重要环节。安全属性的实例化不仅需要严格遵循漏洞的逻辑特性，还需要结合目标模块的设计实现，将抽象的安全性约束具体化为模块内部的信号关系和时序逻辑。这一过程的核心在于从通用安全属性中提取关键验证要素，映射到信息流模型中特定信号，并结合模块的行为特点，给出形式化的属性定义。

以安全属性1为例，其通用描述为：推测性访存指令应受到严格的权限检查，不得在未经验证的情况下访问敏感数据。为了将这一属性应用于LSU模块，需要首先定位LSU设计中与权限检查相关的核心信号。结合LSU的功能，进行权限检查，比如：权限异常信号用于标识加载指令是否发生权限异常，异常汇总信号标识当前访存操作中是否存在任何异常。这些信号明确了权限检查的逻辑基础。与此同时，下一阶段访存请求信号则表示当前访存请求是否有效并传递至后续模块。通过将这些信号相互关联，可以建立安全属性1的具体形式化定义，如断言逻辑表达式(_mem_xcpt_valids_T_6|-> dmem_req_0_valid == 0)，可以验证异常信号_mem_xcpt_valids_T_6是否严格约束了访存请求dmem_req_0_valid的有效性，验证推测性访存指令在异常发生时是否会继续生成有效请求信号。

通过上述实例化过程可以看出，从通用安全属性到模块化属性的转化，既需要针对模块功能和信号特点进行信号定位，也需要结合漏洞特性构建符合实际的约束条件。这种从抽象到具体的过渡，为形式化验证提供了精确的理论依据。

2.5 安全属性形式化验证方法

如图 7所示，针对幽灵漏洞的复杂特性，本文提出了系统化的验证方法。

图7 安全属性验证方法

根据幽灵漏洞的3条通用安全属性定义，需要在处理器微架构中定位相关的验证模块：属性1对应加载存储单元(LSU)，负责访存指令的权限检查; 属性2和3对应数据缓存单元(Dcache)，负责微架构状态的管理和恢复。

以属性1为例，需要定位LSU设计中与权限检查相关的核心信号；识别异常信号和访存请求信号之间的逻辑关系；构建形式化断言，验证异常信号是否严格约束访存请求的有效性。

图 8展示了验证框架采用Questa Formal进行形式化验证的具体流程。

图8 处理器设计安全验证框架流程示意图

1) 验证环境构建: 将门级信息流模型和安全属性断言加载到验证工具中。

2) 状态空间探索: 通过穷尽性搜索验证所有可能的执行路径。

3) 反例分析: 当检测到违例时，生成具体的反例信息以供分析。

除了针对幽灵漏洞的专门验证外，该框架还支持时间侧信道的检测。时间侧信道利用操作时间与机密数据之间的关联，通过分析执行时间变化推断敏感信息。

3 实验验证与分析

3.1 实验环境与配置

本文选择了2种具有代表性的RISC-V处理器进行实验验证：学术界广泛使用的SonicBOOM处理器和商用领域的Xuantie-910处理器。实验使用开源工具Yosys Open Synthesis Suite对处理器模块的RTL代码进行逻辑综合，生成门级网表后通过离散映射得到信息流模型。验证工具采用Questa Formal，该工具支持SystemVerilog Assertions语言，能够高效处理复杂的形式化验证任务。

3.2 SonicBOOM处理器验证结果

SonicBOOM是加州大学伯克利分校开发的开源超标量乱序处理器，采用Chisel硬件描述语言实现，具有复杂的微架构设计和多种性能优化机制。

针对推测性访存指令权限检查属性(属性1)，选择SonicBOOM的加载存储单元(LSU)进行验证。通过逻辑综合生成LSU模块的门级网表，并构建相应的门级信息流模型。在构建信息流模型的过程中，为了便于捕获推测路径上的信号流动和潜在的安全风险，对每一个信号都引入了对应的标签信号和标签传播逻辑。例如，在LSU单元的门级信息流模型的标记中，对输入信号分别新增了对应的标签信号。这些标签信号用于标识信号流动过程中是否携带潜在的敏感信息。此外，本文还定义了这些标签信号与原始信号之间的标签传播逻辑，通过逻辑规则确保标签信号能够准确反映原始信号在推测路径中的传播行为。

在完成针对LSU单元的信息流模型构建后，将关键信号实例化为标签信号，并依据标签传播逻辑提取出属性1的具体安全属性断言。通过对异常信号和访存请求信号的标签化处理，明确了推测性访存指令在发生异常时是否受权限检查约束的验证逻辑。属性1的实际断言如代码1所示，用于验证异常信号的标签是否正确影响后续请求信号的标签。

代码1  幽灵安全属性1

1  formal netlist constraint _mem_xcpt_valids_T_6_t 1

2  formal netlist constraint _mem_xcpt_valids_T_6 1

3  formal netlist constraint io_core_exe_0_req_bits_uop_ctrl_is_load 1

4  formal netlist constraint io_core_exe_0_req_bits_uop_br_mask 8′b11111111;

5  …//约束其他输入信号的安全标签值均为0

6    property A1;

7      @(posedge clock) disable iff(reset)

8      (_mem_xcpt_valids_T_6 |-> (dmem_req_0_valid_t == 1));

9     endproperty

10    assert property(A1);

从形式化验证结果可以直接看出，安全属性1在验证过程中被违反，表明在SonicBOOM处理器的LSU单元中，推测性访存指令在异常发生时并未受到权限检查的严格约束。具体而言，异常信号的标签未能有效约束访存请求信号的传播路径，导致推测路径中的访存请求绕过了预期的权限检查逻辑。这种验证反例明确指出了处理器在推测执行阶段的权限管理机制存在缺陷，为推测性访存指令未经验证访问敏感信息提供了可能性。图 9展示了属性违反的形式化验证结果，后续结果图片类似，由于篇幅原因不再展示。

图9 SonicBOOM属性1 Questa形式化验证结果

针对微架构状态传播控制属性(属性2)和微架构状态恢复一致性属性(属性3)，对SonicBOOM的数据缓存(Dcache)模块进行验证。

结果显示这2个安全属性都被违反，说明推测性访存指令会影响缓存微架构状态，且在推测执行结束后微架构状态无法正确恢复。

3.3 Xuantie-910处理器验证结果

Xuantie-910是阿里巴巴平头哥半导体推出的商用高性能RISC-V处理器，代表了当前RISC-V商用处理器的先进水平。

对Xuantie-910的LSU模块进行属性1验证，结果同样显示存在违例，表明推测性访存指令的权限检查机制存在安全风险。对Dcache模块进行属性2和属性3的验证，验证结果均显示安全属性被违反，证明该商用处理器同样存在幽灵漏洞风险。

验证结果表明，2种处理器3条安全属性上都存在违例情况，证明了当前RISC-V处理器设计中普遍存在幽灵漏洞风险，同时也验证了所提安全属性的通用性和有效性。

3.4 攻击方法验证

3.4.1 时间侧信道攻击验证

对于SonicBOOM处理器，验证了基于端口争用的时间侧信道攻击。实验中，通过在推测执行前插入4条DIV指令，在推测执行路径中插入4条ADD指令，制造了ALU和DIV单元之间的资源争用，结果如图 10所示。

图10 端口争用与非争用状态执行时间示意图

通过测量程序执行时间，实验定义了端口争用阈值为146个周期。当执行时间超出阈值时，表示发生了端口争用。实验结果显示，争用状态与非争用状态的时间分布具有明确的分离特性，进一步验证了基于端口争用的时间侧信道攻击的有效性。

对于Xuantie-910处理器，采用基于缓存的Flush+Reload模型对时间侧信道攻击进行了验证。实验测量了缓存读取时间与内存访问时间的差异，结果如图 11所示。实验表明，缓存命中读取周期显著低于内存命中的读取时间。选定缓存命中阈值为50个周期，该值为缓存命中与内存命中周期之间选定的一个随机值，此时从实验结果中可以看出，当Reload阶段的访问时间小于阈值时，数据一定来自缓存，否则来自内存。实验结果验证了该方法的有效性，时间测量结果显示出显著的分离特性。通过合理选择阈值，进一步提高了攻击的精度与效率，为后续的优化设计提供了指导。

图11 缓存读取与内存读取时间差示意图

3.4.2 幽灵攻击方法验证

基于验证反例构建了8种幽灵攻击变种，包括基于PHT、BTB、RSB、SSB的攻击方法。以Spectre-SSB为例，SonicBOOM和Xuantie-910上攻击仿真结果如图 12~13所示。

图12 SonicBOOM上Spectre-SSB仿真结果

图13 Xuantie-910上Spectre-SSB仿真结果

其中左侧红框内为目标机密信息，右侧红框内为通过攻击恢复的机密信息，实验结果表明，攻击方法能够准确还原敏感数据。

3.4.3 性能评估

在软件仿真完成之后，本文进一步测量了不同攻击方法的机密信息窃取速率，主要由恢复一个字节机密数据所需时钟周期数和每秒能够泄露的字节数(频率为100 MHz)2个指标来衡量，各个攻击方法在相应架构上的仿真结果和泄露速率如表 2所示。

表 2显示在2种架构下，Spectre-PHT和Spec-tre-BTB这类依赖误训练的攻击恢复机密信息耗时较长。以BTB为例，端口争用攻击无需重复，但每字节攻击需误训练分支预测器64×256=16 384次，因此攻击时间显著高于其他方法。而在不同时间侧信道方式中，基于Cache的攻击需遍历256个可能值，耗时较长；相较之下，SonicBOOM中基于端口争用的攻击耗时更短。分析表明，攻击效率与架构设计及触发机制复杂性密切相关。基于缓存的攻击较端口争用耗时更长，而无需误训练的攻击方式因触发机制更高效，整体效率更高。

4 结论

本文提出了一种基于信息流分析的RISC-V处理器幽灵漏洞检测方法。通过深入分析幽灵漏洞的攻击机理，提取出推测性访存绕过权限检查、微架构状态传播机密信息和侧信道泄露机密信息的3个共性特征，进而定义了3条通用的安全属性，涵盖了推测执行过程中的关键安全风险点。该方法将信息流分析技术与形式化验证相结合，构建了系统化的处理器安全验证框架，能够精确捕获硬件设计中的信息流动特性。

选择SonicBOOM和Xuantie-910处理器作为实验验证对象。验证结果表明，2种处理器都存在幽灵漏洞风险，3条安全属性都出现了违例情况，证明了所提方法的有效性和通用性。基于验证反例，本文进一步构建了2种时间侧信道攻击和8个幽灵攻击变种，仿真实验成功验证了机密信息的泄露，证实了检测结果的准确性。

References

All Tables

All Figures

	图1 幽灵攻击流程示意图
In the text

	图2 攻击阶段示意简图
In the text

	图3 推测执行期间敏感信息传播示意图
In the text

	图4 刷新+重载缓存攻击示意图
In the text

	图5 处理器设计安全验证框架整体架构图
In the text

	图6 信息流跟踪技术基本原理
In the text

	图7 安全属性验证方法
In the text

	图8 处理器设计安全验证框架流程示意图
In the text

	图9 SonicBOOM属性1 Questa形式化验证结果
In the text

	图10 端口争用与非争用状态执行时间示意图
In the text

	图11 缓存读取与内存读取时间差示意图
In the text

	图12 SonicBOOM上Spectre-SSB仿真结果
In the text

	图13 Xuantie-910上Spectre-SSB仿真结果
In the text