中文 英语

RISC-V对正确的验证变得更少的危险

检测具有正式验证的高批量芯片中的开源核心中的关键错误。

人气

RISC-V继续通过电子设计行业进行头条新闻。您可能已经看到了最近的消息,即OpenHW集团正在提供他们的第一个RISC-V核心,CV32E40P。如果您上个月的RISC-V Summit参加,则您可以通过Rick O'Connor,OpenHW集团总裁Rick O'Connor参加“核心V:工业级开源RISC-V核心。在本次会议中,Rick讨论了组织如何与Onespin和其他几个验证合作伙伴一起开发核心V-Verif硅验证的工业级功能验证平台。该平台用于执行Core-V CV32E40P的完整验证,当前用于验证CV32A6和CV64A6核心。

CV32E40P核心将用于高批量,商业芯片项目,具有严格的完整性标准。OpenHW集团认识到单独使用模拟将使核心容易受到未检测到的关键错误,不完整的覆盖范围和/或未受伤的隐藏指令 - 并且完全认识到这些验证缺点中的任何一个都可能导致功能错误,安全问题和安全漏洞。为了解决这个问题,Core-V-Verif平台超越了模拟,以包括Onespin的独特形式验证技术,这已经证明了实现CV32E40P核心的快速,成功和无霸递送的速度至关重要。

Rick O'Connor了解正式在实现完整验证的影响:“Onespin的独特技术是对OpenHW验证任务组的理想贡献,帮助识别单独模拟的错误。ONESPIN解决方案允许任务组实现所需的覆盖范围,以便在速度和质量方面达到职能RTL冻结签署目标。“高度赞扬 - 谢谢,瑞克! - 但是Onespin究竟与OpenHW组有多工作以验证他们的Core-V核心吗?合作从头开始,在整个验证过程中继续进行。

ONESPIN首先与OpenHW验证任务组密切合作,以制定正式的验证计划。ONESPIN然后增强了基于SystemVeriLog / UVM的Core-V验证测试台仿真工作。断言证明核心实现/ rtl模型符合ISA;这些断言是自动生成的或手动编写的,以涵盖计划的所有项目。审查代码覆盖,突变覆盖范围和断言覆盖度量指标,增加了计划所有项目的信心。一旦进行了测试台,运行时在几天内完成,并且在几分钟内完成调试。ONESPIN检测到许多关键错误:八个与常规和例外指令相关,其他与特权规范相关。ONESPIN的敏捷方法允许调整正式验证计划,以满足OpenHW验证任务组的验证优先级,以最大限度地提高冻结结果。最终结果在很短的时间内令人遗憾和完整验证。

硅实验室在验证工作中有一个前排座位,因为他们有助于领导OpenHW验证任务组。史蒂夫里士满,硅实验室的验证经理和任务组的共同主席,规定:“CV32E40P核心是第一个用于高卷芯片的开源核心,该芯片验证了高级的最先进的过程诚信,商业SoC。ONESPIN是一个关键的贡献者。ONESPIN RISC-V Integrity正式验证解决方案在异常逻辑和管道中系统地检测到的角色案例错误。这些问题只能在指令序列,内存档位和控制和状态寄存器编程中的罕见条件下触发。受限随机仿真测试,以查找这些问题需要大量的开发和模拟时间。“

Arjan Bink,Silicon Labs和OpenHW Cores任务组主席的主要建筑师,继续说:“问题根本原因的精确点令人印象深刻,并且在调试中具有大量的时间。该解决方案还在检测真正的RTL错误时显示出几乎零噪声,而不是其他方法,这些方法通常会导致验证环境中的问题。“

查看标题为“深入潜入Core-V CVE4的正式验证”的OpenHW电视集团拥有我们自己的Sven Beyer Risc-V产品经理,了解有关缺乏贡献效力的更多信息。

任何人都考虑使用RISC-V作为下一个设计的一部分,了解开源架构提供的定制和灵活性。但是,处理器验证是一种新要求,即采用者必须承担。值得注意的是,任何用户优化或自定义指令的添加需要完全重新验证,以防止先前提到的恶意插入可能导致的相同潜在问题。复杂的微架构,用于实现电源,性能和面积目标,结合大量的指令组合,缓存,中断,例外和无数自定义扩展,所有这些都需要完全验证。进一步复杂化验证是需要确保核心对指令集架构(ISA)的正确是正确的,以及RTL与ISA匹配。

OpenHW CV32E40P核心完全验证并准备使用,但仍然存在一些验证挑战,设计人员在整合核心时需要克服:特别是在核心定制的情况下。此核心和其他RISC-V核心如此,应在集成或定制后重新验证,以确保任何更改都不会引入新的错误或产生不需要的行为 - 而正式的验证是消除风险的方式,并详尽证明所有内容就像应该一样。

要了解有关如何对您的risc-v设计的完整性,请下载我们的白皮书,“确保RISC-V核心和SOC的完整性,”https://www.onespin.com/resources/white-斑点



1评论

Kirk Weedman. 说:

我也一直在开发几个RISC-V CPU。一个是基于新的动态指令调度Algorthim I创建的,另一个是基于开源5级流水线RV32i的out ..我的开放源的目标是使其高度参数化,以便可以创建大量不同版本,并作为车辆到正式验证测试设置以测试此基于RISC-V基于的CPU。这很苦难。目前在RV32imCzicsr上使用许多基于扩展的衍生品和可以更改的各种参数。RISC-V的真正问题是验证。具体而言,正式验证。那里有很多RISC-V CPU,符合一些“金色模型”,但我不确定它有多金色,因为真的没有正式规格。然而。SAIL, from what I’ve seen, doesn’t cover much, especially when it comes to CSRs, etc.. I joined the Formal group to keep tabs and see if can help, but in the mean time I’ve been developing a System Verilog model that I use to verify my test CPU and it’s derivatives. Currently all of my 700+ property assertions for RV32imc are proven in about 15 min. Of course this means nothing if my model doesn’t match the Formal spec – whenever that becomes a reality. CSR’s have some gotchas and I wonder how many RISC-V’s out there will really match a Formal spec. I currently use commercial formal verification tools. Most of my property assertions are generated using SV macros.

发表评论


(注意:此名称将被公开显示)