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

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 语言设计而成,该内核完全可定制,包括经典的扩展和特性,以及实现这些扩展和特性所需的高效和彻底的验证。

图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可定制大小高达2MBAHB-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 中的资源是否具有相同的值。

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

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

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

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

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

  • 用户可以指定设计执行的顶层 RISC-V 参数和扩展。
  • 该工具能够自动从设计中提取数据,例如将架构寄存器与实际每秒浮点运算次数相关联。
  • 该工具允许添加自定义,例如用来验证的新指令(具有为用户“扩展”黄金模型的能力)。

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

本文摘录于《基于形式的高效 RISC-V 处理器验证方法 – 形式化验证》白皮书,出版人为总部位于欧洲的全球领先RISC-V供应商和处理器解决方案领导者,该公司的处理器IP目前已部署在数十亿颗芯片中。Codasip通过开放的RISC-V ISA、Codasip Studio处理器设计自动化工具与高品质的处理器IP相结合,为客户提供定制计算。这种创新方法能够轻松实现定制和差异化设计,从而开发出高性能的、改变游戏规则的产品,实现真正意义上的转型。如希望得到该白皮书的完整版本,可浏览Codasip中文网站或者关注该公司微信公众号。

该技术白皮书英文版下载链接:https://codasip.com/papers/a-formal-based-approach-for-efficient-riscv-processor-verification

责编:Amy.wu
阅读全文,请先
您可能感兴趣
早在十多年前,电动汽车就已经引入400V电池系统,现在我们看到行业正在向800V系统迁移,主要是为了支持直流快速充电。随着电压的提高和从400V系统中学到的经验教训,设计人员现在正专注于增强高压保护电路的性能并提高可靠性。他们正在重新评估使用熔丝、接触器或继电器的现有解决方案,以寻找响应速度更快、稳健性更强且可靠性更高的解决方案,如热熔丝和电子熔丝(即E-Fuse)。
对于工程师来说,当不同的工程有不同的电池充电需求时,设计使用可充电电池并为消费者提供出色充电体验的应用可能具有挑战性。如果对每个应用使用专用的电池充电器,会增加设计时间,因为您必须重新设计、调试和重新鉴定每个新电路。
自ChatGPT带火AI以来,AI芯片得到了空前的发展,十月底高通发布了基于Arm架构的带有AI算力的骁龙X Elite芯片。刚刚,Arm宣布将在2024年推出Cortex-M52芯片,为低功耗物联网设备带来AI加速功能。
因应人工智能(AI)等应用对于更高效能计算的需求,以及小芯片(chiplet)异质整合架构的挑战,英特尔(Intel)打造可用于下一代先进封装的玻璃(Glass Core)衬底...
由于电子器件的频率和性能不断提高,要求与之匹配的二极管必须具备恢复时间短,反向恢复电流小和软恢复等特点。而快恢复二极管(FRD)因具备上述特点而被广泛应用。本文简要介绍快恢复二极管的反向恢复过程,及基于TCAD软件工具采取一系列方法优化恢复二极管的反向恢复,使其能够实现快速而软的恢复。
音频产品具有独特性质,这意味着将给工程师带来特殊的测试挑战。那么,如何通过评估使音频产品能够输出“最佳”声音?本文详论了主客观评估之间的巨大差异,给出了音频测试的层次结构、客观测试性能指标、以及客观评估测试技巧。并强调,音频产品开发无论是哪个阶段,都必须为测试留出超出常规想象的时间预算。
根据TrendForce集邦咨询最新OLED技术及市场发展分析报告统计,在近期发表的摺叠新机中,UTG的市场渗透率已逾九成,随着摺叠手机规模持续成长,预估2023年UTG产值将达3.6亿美元;2024年可望挑战6亿美元。
随着终端及IC客户库存陆续消化至较为健康的水位,及下半年iPhone、Android阵营推出新机等有利因素,带动第三季智能手机、笔电相关零部件急单涌现,但高通胀风险仍在,短期市况依旧不明朗,故此波备货仅以急单方式进行。此外,台积电(TSMC)、三星(Samsung)3nm高价制程贡献营收亦对产值带来正面效益,带动2023年第三季前十大晶圆代工业者产值为282.9亿美元,环比增长7.9%。
治精微推出具过压保护OVP、低功耗、高精度运放ZJA3018
无线技术每天都在拯救生命,有些非常方式是人们意想不到的。在美国加利福尼亚州Scotts Valley,一名路过的慢跑者发现一处住宅冒出火焰后,按响了门铃,试图通知屋主。屋主不在家中,但无线门铃连接到了智能家居中枢,提醒屋主慢跑者试图联系。屋主立即向他提供了安全密码,让他跑进房子,从火场中救出了宠物。
点击左上角“锂电联盟会长”,即可关注!锂离子电池是一种二次电池(充电电池),它主要依靠Li+ 在两个电极之间往返嵌入和脱嵌来工作。随着能源汽车等下游产业不断发展,锂离子电池的生产规模正在不断扩大。本文
来看看,你需不需要这门接收机设计课程吧(已更新八次)。如有需要,现在仍然可以报名。(1)前几天,号友发来她的听课笔记,我真的是泪流满面。感觉,自己这么长时间的备课,总算没白费。说实话,我备课的时候,真
注:各大公司财政年度的起始时间不同于自然年,因此会出现财政季度、年度等与自然年不一致的情况。软件微软(Microsoft)公布截至2023年9月30日的2024财年第一财季业绩。第一财季营收为565.
有奖问卷调查:各位工程师朋友,作为全球知名的授权半导体和电子元器件代理商,贸泽电子 Mouser多年来一直倾心为中国工程师服务,助力本土创新! 时至年终,为了更好的服务工程师朋友,我们特别推出“贸泽电
广告分割线12月11日,据台媒报道,群创(3481.TW)竹南T1厂员工向媒体爆料,群创竹南T1厂将裁员50%!据报道,群创竹南厂工程师预计将减少一半,在线作业员也预计砍一半。群创今天表示,已于第一时
点击左上角“锂电联盟会长”,即可关注!文 章 信 息干法改性工艺新认识,助力锂离子电池高镍正极材料实现高结构稳定和热稳定性能第一作者:吴锋通讯作者:苏岳锋*,陈来*通讯单位:北京理工大学,北京理工大学
01 项目简介该项目是使用ESP32模块复刻的Nokia1110,可运行NES游戏模拟器和LVGL,主要功能包括彩屏显示,ADC按键,Type-C充电,USB转串口,DAC音乐播放,SD卡读写,WS2
曹原 发自 副驾寺智能车参考 | 公众号 AI4Auto全球第一的 Tier 1,官宣裁员了。博世刚刚证实,准备裁员1500人,以适应汽车行业不断变化的技术和需求。博世发言人表示:我们面临了比年初预期
点击左上方蓝色“一口Linux”,选择“设为星标”第一时间看干货文章 ☞【干货】嵌入式驱动工程师学习路线☞【干货】一个可以写到简历的基于Linux物联网综合项目☞【干货】Linux嵌入式知识点-思维导
 /记得星标我/比大部分人早一步看见未来乡村振兴,产业兴旺是重点。今年是加快建设农业强国的起步之年,在陕西,陕西移动依托自身信息技术优势,在电子商务、养殖业、农业等方面注智赋能,推动特色产业稳步发展,