0
  • 聊天消息
  • 系统消息
  • 评论与回复
登录后你可以
  • 下载海量资料
  • 学习在线课程
  • 观看技术视频
  • 写文章/发帖/加入社区
会员中心
创作中心

完善资料让更多小伙伴认识你,还能领取20积分哦,立即完善>

3天内不再提示

基于形式的高效 RISC-V 处理器验证方法

jf_pJlTbmA9 来源:jf_pJlTbmA9 作者:jf_pJlTbmA9 2023-07-10 09:42 次阅读

RISC-V的开放性允许定制和扩展基于 RISC-V 内核的架构和微架构,以满足特定需求。这种对设计自由的渴望也正在将验证部分的职责转移到不断壮大的开发人员社群。然而,随着越来越多的企业和开发人员转型RISC-V,大家才发现处理器验证绝非易事。新标准由于其新颖和灵活性而带来的新功能会在无意中产生规范和设计漏洞,因此处理器验证是处理器开发过程中一项非常重要的环节。

在复杂性一般的RISC-V 处理器内核的开发过程中,会发现数百甚至数千个漏洞。当引入更多高级特性的时候,也会引入复杂程度各不相同的新漏洞。而某些类型的漏洞过于复杂,导致在仿真环节都无法找到它们。因此必须通过添加形式验证来赋能 RTL 验证方法。从极端漏洞到隐匿式漏洞,形式验证能够让您在合理的处理时间内详尽地探索所有状态。

在本文中,我们将介绍一个基于形式验证的、易于调动的 RISC-V 处理器验证程序。与 RISC-V ISA 黄金模型和 RISC-V 合规性自动生成的检查一起,展示了如何有效地定位那些无法进行仿真的漏洞。通过为每条指令提供一组专用的断言模板来实现高度自动化,不再需要手动设计,从而提高了形式验证团队的工作效率。

1、基于先进内核的处理器开发

嵌入式系统的应用越来越广泛,同时对处理器的性能、功耗和面积(PPA)要求越来越高,因此我们将这样的产业和技术背景下用实际案例来分析处理器的验证。Codasip L31 是一款用于微控制器应用的 32 位中端嵌入式 RISC-V 处理器内核。作为一款多功能、低功耗、通用型的 CPU,它实现了性能和功耗的理想平衡。从物联网设备到工业和汽车控制,或作为大型系统中的深度嵌入式内核,L31可在一个非常小巧紧凑的硅片面积中实现本地处理能力。L31是通过 Codasip Studio 使用 CodAL 语言设计而成,该内核完全可定制,包括经典的扩展和特性,以及实现这些扩展和特性所需的高效和彻底的验证。

1685495502743186.png

图1 Codasip L31处理器内核架构图解(来源:Codasip)

表 1 Codasip L31内核展示了RISC-V处理器的优异特性

特性 描述
指令集架构 (ISA) RV32 I/M/C/F/B
流水线 3级顺序流水线
分支预测器 可选,优化过的单线程性能
并行乘法器 并行实现,单周期乘法
序列除法器 顺序执行
内存保护 ●具有 2/4/8/16 个区域的可选MPU
●具有 2/4/8/16 个区域的物理内存属性
机器和用户权限模式
耦合存储器 (TCM) ●指令和数据TCM
●可定制大小高达2MB
AHB-Lite TCM 辅助端口
接口 用于获取和数据的 32 位 AHB-Lite 接口(带缓存的 AXI-Lite)
浮点单元 (FPU) 可选,单精度
调试 ●标准 RISC-V 调试
●2/4 JTAG
●2-8 个断点和观察点
●系统总线接入
中断 ●中断控制器
●标准 RISC-V CLINT 执行
●多达 128 个中断
●WFI(等待中断)
●NMI(不可屏蔽中断)

2 创建最优的RISC-V处理器验证方法

处理器验证需要制定合适的策略、勤勉的工作流程和完整性,而方兴未艾的、更加灵活的RISC-V处理器开发则需要针对自己处理器功能设置做详尽的验证规划;也需要参考一些内核供应商的内外部因素,比如该供应商自己的开发工具体现和外部开发工具伙伴,以及同系、同款或者同厂内核的出货量等。

验证处理器意味着需要考虑诸多不确定性。最终产品将运行什么软件?用例是什么?可能发生哪些异步事件?这些未知数意味着较大的验证范围。然而,覆盖整个处理器状态空间是无法实现的,这也不是Codasip这样的领先内核供应商的目标。

在确保处理器品质的同时,充分利用时间和资源才是处理器验证的正解。明智的处理器验证意味着在产品开发过程中尽早并高效地发现相关漏洞。在顶层方面,Codasip提供了多种创新的验证路径,其验证方法基于以下内容:

验证是在处理器开发期间与设计团队合作完成的。

验证是所有行业标准技术的组合。使用多种技术可以让您最大限度地发挥每一种技术的潜力,并有效地覆盖尽可能多的极端情况。

验证需持续进行。有效的办法是运用随着处理器复杂程度而不断发展的技术组合。

在验证L31内核时,我们的想法是让仿真和形式验证相辅相成。

2.1仿真的优势和目的

仿真实际上不可或缺,它允许我们在两个级别上进行验证设计:

顶层仿真(Top-level),主要是为了确保设计在最常见的情况下符合其规范(CPU 的 ISA)。

块级仿真(Block-level),以确保微架构按照预期设计。然而,很难将这些检查与顶层架构规范联系起来,因为这通常依赖于定向随机测试生成,因此能够应付棘手和不寻常的情况。

顶层仿真通常不像块级仿真那样特意强调设计。因此,它可以实现针对 ISA 的设计的整体验证。

2.2形式验证的优势和目的

形式验证使用数学技术对以断言形式编写的问题提供有关设计的明确答案。

形式验证工具对断言和设计的组合进行详尽的分析。不需要指定任何刺激,除了指定一些非正常情况以避免假漏洞。该验证工具可以提供详尽的“已证实”答案或“失败”答案,同时生成显示刺激的波形,证明断言是错误的。在大型和复杂的设计中,工具有时只能提供有限的证明,这意味着从重置到特定数量的周期都不存在漏洞场景。同时也存在不同的技术方法来增加该周期循环次数,或获得“已证明”或“失败”的答案。

形式验证用于以下情况:

为完整的验证一个模块,潜在地消除了任何仿真的需要。由于形式验证的计算复杂性,形式化验收(sign-off)仅限于小模块。

除了仿真之外,还要验证一个模块,即使是个大模块,因为形式验证能够在极端情况下找到漏洞,而随机仿真只能“靠运气”找到,而且概率非常低。

处理一些仿真不充分的验证任务,例如时钟门控、X态传播(X-propagation)、数据增量处理(CDC)、等价性检查等。

帮助调查缺少调试信息的已知漏洞,并确定潜在的设计修复。

对漏洞进行分类和识别,以便通过形式验证来学习和改进测试平台/仿真。

为了潜在地帮助仿真,填充覆盖范围中的漏洞。

3解决方案:一种基于形式验证的高效的 RISC-V 处理器验证方法

为了获得一种高效的RISC-V处理器验证方法,我们决定以采用西门子EDA 处理器验证APP来高效验证Codasip L31 RISC-V 内核为例,来进行详尽的说明。该工具的目标是确保 RTL 级别的处理器设计正确且详尽地实现指令集架构 (ISA)规范,而本文希望介绍的是一种端到端的解决方案

1.该工具从一个顶层并有效的“黄金模型”中生成以下:

Verilog 语言中,ISA 的单周期执行模型。

一组断言,用于检查待测试模块 (DUT)和模型 (M)在架构级别的功能是否相同。

注意:这并没有进行任何正式等价性检查。

2.当在 DUT 中获取新指令 (I)时,会捕获架构状态 (DUT-init)。

3.该指令在流水线中运行。

4.捕获另一个架构状态(DUT-final)。

5.M 被输入 DUT-init 和 I,并计算出一个新的 M-final 状态。

6.断言检查 M-final 和 DUT-final 中的资源是否具有相同的值。

1685495496934257.png

图 2 3 级 L31 内核的端到端验证流程(当验证指令 I 既没有停止也没有清除缓存数据时)

这种端到端的验证方法可以在比整个CPU 更小、更简单的模块(例如数据缓存)上合理实现。可以在缓存上写入端到端断言,以验证写入特定地址的数据是否从同一地址正确读取。这使用了众所周知的形式验证技术,例如记分牌算法

然而,对于 CPU来说,手动编写这样的断言是不可行的。它需要指定每条指令的语义,并与所有执行模式交叉。这通常根本不可能实现。 CPU 的形式验证被分成更小的部分,但是仍然无法验证所有部分是否正确执行了 ISA。

使用建议的方法意味着能够立即验证完整的 L31 内核,而无需编写任何复杂的断言。如上所述,黄金模型和检查断言是自动生成的。

这种方法同时具有高度可配置性和自动化性,特别是对于 RISC-V CPU,例如 L31:

用户可以指定设计执行的顶层 RISC-V 参数和扩展。

该工具能够自动从设计中提取数据,例如将架构寄存器与实际每秒浮点运算次数相关联。

该工具允许添加自定义,例如用来验证的新指令(具有为用户“扩展”黄金模型的能力)。

最后,黄金模型不是由Codasip开发的(除了一些自定义部分),这一事实提供了额外的保证,这从验证独立性的角度来看很重要。

声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉
  • 处理器
    +关注

    关注

    68

    文章

    19275

    浏览量

    229756
  • RISC-V
    +关注

    关注

    45

    文章

    2275

    浏览量

    46143
  • codasip
    +关注

    关注

    0

    文章

    37

    浏览量

    6233
收藏 人收藏

    评论

    相关推荐

    验证RISC-V处理器的安全性

    。 本文讨论了与硬件安全验证相关的一些挑战,并介绍了一种基于形式方法来解决。实现流行的RISC-V指令集架构(ISA)的设计示例展示了这种方法
    的头像 发表于 03-16 10:47 9669次阅读
    <b class='flag-5'>验证</b><b class='flag-5'>RISC-V</b><b class='flag-5'>处理器</b>的安全性

    学习RISC-V入门 基于RISC-V架构的开源处理器及SoC研究

    RISC-V架构的开源处理器与SoC。1 RISC-V简介1.1 RISC-V的基本设计RISC-V是一个典型三操作数、加载-存储
    发表于 07-27 18:09

    RISC-V是什么?如何去设计RISC-V处理器

    RISC-V是什么?有哪些特点?如何去设计RISC-V处理器
    发表于 06-18 09:24

    RISC-V开源处理器核介绍

    本期文章目录一个小型RISC-V开源处理器核介绍!#SOC#FPGA#RISC-V点击阅读数字积木从零开始写RISC-V处理器(超详细)#
    发表于 07-23 09:42

    香山处理器 RISC-V的典范

    https://github.com/JiaoXianjun/XiangShan谈到RISC-V,应该都会想到香山处理器。其经历了几代的演进,性能越来越高。采用Chisel Rocketchip框架,能够方便的定制属于你的RISC-V
    发表于 04-14 15:51

    读《玄铁RISC-V处理器入门与实战》

    是由美国伯克利大学的 Krest 教授及其研究团队提出的,当时提出的初衷是为了计算机/电子类方向的学生做课程实践服务的。由于这是伯克利大学研究并流片的第五代RISC架构处理器,因此就命名为RISC-V
    发表于 09-28 11:58

    RISC-V是通用RISC处理器还是可定制的处理器?

    随着这些年的发展,RISC-V的受重视程度与与日俱增。这主要因为它是免费的、灵活的,并且速度很快。这使RISC-V成为许多开发人员的安全便捷选择。但是您会认为RISC-V是通用RISC
    的头像 发表于 11-17 16:11 3525次阅读

    定制RISC-V处理器简化设计验证

      Imperas 产品组合以及来自快速发展的 RISC-V 生态系统的其他工具,为您今天开始自己的开放式处理器设计提供了足够的资源。
    的头像 发表于 06-01 10:00 1598次阅读
    定制<b class='flag-5'>RISC-V</b><b class='flag-5'>处理器</b>简化设计<b class='flag-5'>验证</b>

    关于RISC-V 处理器验证的问题

    处理器验证是一个全新的领域。我们知道 Arm 和 Intel 对处理器质量的期望设置了很高的标准。在 RISC-V 中,我们必须尝试并遵循这一点。
    发表于 03-22 15:19 574次阅读

    如何利用形式化验证提高RISC-V处理器质量?

    RISC-V是一个模块化的指令集架构,可以为其开发一个架构测试套件。它被用于基于仿真的验证,以验证一个处理器的实现。
    发表于 04-17 14:54 582次阅读

    基于形式验证高效RISC-V处理器验证方法

    转型RISC-V,大家才发现处理器验证绝非易事。新标准由于其新颖和灵活性而带来的新功能会在无意中产生规范和设计漏洞,因此处理器验证
    的头像 发表于 06-01 09:07 622次阅读
    基于<b class='flag-5'>形式</b><b class='flag-5'>验证</b>的<b class='flag-5'>高效</b><b class='flag-5'>RISC-V</b><b class='flag-5'>处理器</b><b class='flag-5'>验证</b><b class='flag-5'>方法</b>

    基于形式验证高效RISC-V处理器验证方法

    随着RISC-V处理器的快速发展,如何保证其正确性成为了一个重要的问题。传统的测试方法只能覆盖一部分错误情况,而且无法完全保证处理器的正确性。因此,基于
    的头像 发表于 06-02 10:35 1394次阅读

    利用先进形式验证工具来高效完成RISC-V处理器验证

    在本文中,我们将以西门子EDA处理器验证应用程序为例,结合Codasip L31这款广受欢迎的RISC-V处理器IP提供的特性,来介绍一种利用先进的EDA工具,在实际设计工作中对
    的头像 发表于 07-10 10:28 552次阅读
    利用先进<b class='flag-5'>形式</b><b class='flag-5'>验证</b>工具来<b class='flag-5'>高效</b>完成<b class='flag-5'>RISC-V</b><b class='flag-5'>处理器</b><b class='flag-5'>验证</b>

    思尔芯原型验证助力香山RISC-V处理器迭代加速

    2023年10月19日,思尔芯(S2C)宣布北京开源芯片研究院(简称“开芯院”)在其历代“香山”RISC-V处理器开发中采用了思尔芯的芯神瞳VU19P原型验证系统,不仅加速了产品迭代,还助力多家企业
    的头像 发表于 10-25 08:24 551次阅读
    思尔芯原型<b class='flag-5'>验证</b>助力香山<b class='flag-5'>RISC-V</b><b class='flag-5'>处理器</b>迭代加速

    使用 RISC-V 进行高效数据处理方法

    使用RISC-V进行高效数据处理方法涉及多个方面,包括处理器内核与DSA(领域特定加速)之间
    的头像 发表于 12-11 17:52 352次阅读