你确定你RISC-V RTL不包含任何惊喜?

给定的相对新颖性和复杂性RISC-V RTL设计,不管你是买一个商业核心或下载一个流行的开源提供支持,有意外惊喜的小但非零风险逃离未被发现到你的最终产品。为了到低概率,考虑:

• 的存在weird-yet-entirely-possible个别案例
• 虫子“内部”自定义指令,你或你的供应商为您的应用程序创建
• 虫子“边缘”的自定义指令——例如,指令执行正确,但它在某种程度上使机器损坏的状态
• 相关:无证和/或不指定新特性,无意中打开洞的设计
• 恶意木马逻辑偷偷地插入通过供应链的攻击

常见的缓解方法

当然,第一道防线是专家检查传入的或开发RTL代码。显然,这应该做;但它应该同样明显,这种技术——正如他们所说在数学世界“是必要但不充分”(即使你帕特森教授自己回顾你的代码)。

下一道防线是应用基于仿真的方法:指令集仿真(ISS),自动比较你的DUT成熟黄金模型,constrained-random UVM testbenches为DUT RTL模拟,甚至管道刺激到DUT的借助硬件模拟现实世界。再一次,这些方法都是有价值的,应该做的;但他们都遭受相同的缺陷:它们本质上是不完整的,因为他们依赖于刺激的一代。例如,在极端但可能供应链攻击的情况下,特洛伊逻辑开发人员故意创建了一个触发信号和数据序列可能会逃避检测,即使是最有创意的白帽黑客。当然,功能缺陷有他们自己的方式使用天然的熵保持隐藏。

底线是,唯一的方法是完全确保你RISC-V RTL是完全免费的,没有任何自然或恶意的惊喜是应用详尽,正式的方法来验证设计。

说起来容易做起来难,对吗?

“是”和“不是”:14年前,这种分析是唯一可行的博士生研究人员利用自己的手工制作的项目。但自2008年以来,工具和技术的产品化,那些熟悉的基础形式验证和IEEE标准的写作系统Verilog断言(上海广电)可以在这里快速应用和成功。

formal-based过程三个阶段

推荐formal-based流展开如下:

1. 创建一个“模型”的正式testbench DUT规范
2. 定义输入约束和检查对DUT运行
3. 执行分析

第一步,创建一个“模型”的正式testbench DUT规范

这种方法的基础是编写一组属性,代表每条指令的行为在你RISC-V设计。给定的任务是捕获效应IP的输出和内部架构状态指示(RISC-V世界,这是程序计数器(PC)和注册文件(RF))对于任何给定的任意长度的输入序列。这是使用专用扩展IEEE上海广电运营上海广电。简而言之,这是一个库,附带formal-based处理器验证的工具;从验证工程师的角度来看,它看起来像一个直观的子集,熟悉上海广电代码。图1显示了通用的结构:

财产instruction_A;/ /概念状态t # # 0 ready_to_issue()和/ /触发t # # 0操作码= = instr_A_opc意味着/ /概念状态t # # 0 ready_to_issue()和/ /内存接口输出/ /读取下一个指令t # # 0 imem_access (instr_A_opc)和数据加载/存储/ / t # # 1 dmem_access (instr_A_opc)和t / /建筑寄存器# # 1 RF_update (instr_A_opc)和t # # 1 PC_update endproperty (instr_A_opc)

图1:操作上海广电代码捕获的规范结构处理器指令。[1]

指的是图1中,左边的含义(代码的一部分以上关键字意味着)确定当机器准备发出新的指令,指令发布。断言捕捉建筑的状态和当前值,右边的含义(部分代码下面关键字意味着),证明了他们的下一个值。

此外,处理器的输出被证明是正确的——在这种情况下,以确保指令访问预期的数据和指令的内存位置。断言也证明这台机器已经可以发出新的指令在下一个周期。这是至关重要的解耦验证的一个指令序列的指令的一部分。例如,指令可以正确执行,但离开机器的状态。这个错误的状态可能导致下一个指令B产生不正确的结果并不是自己的过错。因此,股东价值分析与操作方法,断言验证指令B能通过,而断言验证指令会失败(读写内存操作可能会持续几个周期)。

底线:函数操作上海广电的代表建筑州代码必须映射到实现信号和必须反映出微体系结构的处理器。射频的状态,例如,可能取决于转发路径的激活。[1]

【注:如果你熟悉模拟或正式的功能覆盖,这个概念完整性不依赖于结构覆盖率指标,或功能覆盖率模型的创建和收集度量标准。(并获得剩下的步骤和结果)的前面,这里分析的输出都是关于获得所有属性的完整证明。充分证明也含蓄地表明,没有其他功能——不明或意外(规范或编码错误),或恶意插入——这不是被这组属性。挖出,这种方法是实现100%的“测试计划覆盖”详尽的正式验证了分析结果,没有什么比一个“完整的”数学证明!)

步骤2 -定义输入约束和检查对DUT运行

补充规范属性对于每个指令,下一个步骤是定义输入约束和任何额外的输出检查。操作采用上海广电,现在,用户指定一个“完整性计划”来定义两个合法的输入和非法信号的DUT应该忽略。/图2所示的例子中,有三个部分:确定假设,确定需求和属性图。

完整性处理器;determination_assumptions: / /输入决定(imem_data_i);确定(dmem_valid_i);如果(dmem_valid_i)决定(dmem_data_i) endif;determination_requirements: / /输出(imem_read_o)决定的,如果(imem_read_o)决定(imem_addr_o) endif;确定(dmem_enable_o);如果(dmem_enable_o) (dmem_rd_wr_o)决定,决定(dmem_addr_o) endif;/ /建筑州决定(PC);确定(RF);property_graph: all_instructions: = instruction_not_a、instruction_add_a instruction_sub_a, […]all_instructions - > all_instructions; end completeness;

图2:一个完整的例子计划确定条件假设和要求。

阐述:

• “determination_assumptions”只是一个花哨的名字输入值的约束
• “determination_requirements”是一个信号,必须验证的定义(包括处理器的输出信号和建筑状态)
• “property_graph”部分只是一个绑定的文件在步骤1中创建的所有属性

说过我们在这一点上:在步骤1中创建一个有效cycle-accurate DUT的模型必须被证明适用于所有时间和所有输入;在步骤2中你设置约束和任何特殊行为来寻找。把这些加起来,实际上你的正式testbench准备好运行!

步骤3——执行分析

正式的所有工具的目的是详尽的证明,所有的属性都是适用于所有时间和所有输入。RISC-V处理器的验证,该工具可以证明任何任意长度的输入序列可以匹配一个独特的序列指定操作的股东价值分析,预测输出的值和架构。

这是究竟发生了什么。如果有任何不同的行为规范和DUT之间发现,正式的工具提供了一个“反例”波形显示的一系列输入信号和数据,可以创建一个违反规范。正如上面提到的,可以找到此类故障的内部指令的RTL逻辑或t恤的“切换逻辑”下一个/法律分支指令。

无论哪种方式,当这些问题是固定的和工具证明了所有属性,结果是真正的——即“完成”。在数学上,你可以确信没有RTL编码错误的形式分析确实证明了没有任何错误!

结果

首先,如上所述,多年来许多处理器开发人员都受益于这个流[2],[3],[4]。

将这种方法与RISC-V测试,我的同事做了一个案例研究使用流行的火箭开源核心芯片。具体来说,RV64IMAFDC sv39 vm配置检查。这是一个64位的处理器内核39-bit虚拟内存系统[5]和扩展,如压缩和原子指令[6]。这个开源,RISC-V ISA实现使用一个五级,个别问题,按次序的管道与无序的完成为潜伏期长指示,如部门或缓存错过。还支持核心分支预测和运行时修改对剧中“登记,允许它关掉某些指令集扩展。

虽然这快照的火箭芯片被广泛验证,多次贴出,四个未知,个别案例,发现可疑行为,据报道,火箭RTL核心开发人员。这些问题([7],[8],[9],[10])被发现仅仅通过完整的系统化应用本文介绍的形式验证的方法。

阐述具体[10]——的发现非标准指令停止在RTL(操作码0 x30500073):显然火箭芯片团队落后他们的文档(他们固定这个几乎立即申请的GitHub拉请求)。更重要的一点是,这表明整个指令实现所需要的逻辑——几十行代码和许多合成的盖茨,和路由逻辑,可以通过目视检查逃避检测,RTL模拟、门级仿真、后端实现整个过程,和硬件原型在实验室!

但是这个流的性能呢?

首先,让我们解决的更大意义”的性能。“由于火箭芯片设计的新颖性质,对于这个案例研究花了大约20 engineering-weeks为我们的正式验证从业者开发整个testbench和约束。然而,这个流更多的结构化的应用之前,商业IP通常采取了这一次的一小部分。自然,整个启动过程会更快更稳定和成熟规范,记录和可读的DUT RTL代码,和你有多少访问问答的设计工程师。

一旦环境设置,时钟运行时都是2小时,即。,很多不到你可以合理地预期constrained-random RTL模拟甚至借助硬件验证。另外,回想一下,这个分析的结果是有效的对所有输入和所有的时间——总之,详尽的[11]。

总结

完整,formal-based处理器验证方法本文使用一个扩展IEEE股东价值分析,上海广电业务,正式确认RISC-V ISA是免费的差距和矛盾。与testbenches constrained-random模拟、模拟或物理原型,属性和约束的完整详尽的检测到许多类型的RTL错误,以及非法或不指定代码和恶意木马。

引用

1 - 2019 GOMACTech发布会上,阿尔伯克基纳米,2019:3月28日完成正式验证RISC-V处理器ip Trojan-Free信任ICs,大卫•Landoll出版社。

2 - 2007年DVCon:完整的正式验证TriCore2和其他处理器,英飞凌Gmbh是一家。

3 - 51^圣设计自动化会议(DAC):正式验证应用于瑞萨单片机设计平台使用OneSpin工具

4 - DVCon欧洲2019:完整的家庭形式验证汽车dsp、博世公司。

5 - RISC-V指令集手册,第二卷:特权架构、文档版本1.10。

6 -https://github.com/freechipsproject/rocket-chip(2018年12月20日通过)

7 - DIV指令结果没有写寄存器文件
https://github.com/freechipsproject/rocket-chip/issues/1752

8 -日航和JALR指令存储不同的PC
https://github.com/freechipsproject/rocket-chip/issues/1757

9 -非法操作码重播,导致意想不到的副作用
https://github.com/freechipsproject/rocket-chip/issues/1861

10 -非标准指令停止在RTL(操作码0 x30500073)发现,https://github.com/freechipsproject/rocket-chip/issues/1868

11 -验证视野的博客,你怎么能说形式验证是详尽的?第三,乔Hupcey
https://blogs.sw.siemens.com/verificationhorizons/2021/09/16/how-can-you-say-that-formal-verification-is-exhaustive/