中文 英语
德赢vwin
的意见

RISC-V通过正确的验证来降低风险

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

人气

RISC-V继续成为电子设计行业的头条新闻。你可能已经看到了最近的新闻,openw集团正在交付他们的第一个RISC-V核心,CV32E40P。如果你参加了上个月的RISC-V峰会,也许你参加了“CORE-V:工业级开源RISC-V核心”,作者是openw集团总裁Rick O 'Connor。在本次会议中,Rick讨论了该组织如何与OneSpin和其他几个验证合作伙伴合作开发CORE-V-VERIF硅验证、工业级功能验证平台。该平台用于执行CORE-V CV32E40P的完整验证,目前正在用于验证CV32A6和CV64A6内核。

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

Rick O 'Connor理解了形式化对实现完整验证的影响:“OneSpin的独特技术对openw验证任务组做出了理想的贡献,它帮助确定了仅通过仿真就可能遗漏的bug。OneSpin解决方案使任务小组能够在速度和质量方面达到RTL冻结目标。”高praise-thanks,瑞克!但是OneSpin到底是如何与openw集团合作来验证他们的core - v核心的呢?合作从头开始,并在整个核查过程中继续进行。

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

Silicon Labs在验证工作中拥有前排座位,因为他们帮助领导了openw验证任务组。Silicon Labs的验证经理和任务小组的联合主席Steve Richmond说:“CV32E40P内核是第一个高容量芯片的开源内核,它采用了高完整性商用soc所需要的最先进的工艺进行验证。oneespin是一个关键的贡献者。OneSpin RISC-V完整性形式化验证解决方案系统地检测了异常逻辑和管道中的极端情况bug。这些问题只会在指令序列、内存停滞以及控制和状态寄存器编程的罕见情况下触发。为了找到这些问题,需要在开发和模拟时间上投入大量资金。”

Arjan Bink是Silicon Labs的首席架构师,也是openw核心任务小组的主席,他继续说道:“准确定位问题的根本原因令人印象深刻,并且节省了大量的调试时间。在检测真正的RTL bug时,该解决方案也显示出几乎零噪音,而其他方法通常报告的问题会导致在验证环境中进行修复。”

查看标题为“深入潜入Core-V CVE4的正式验证”的OpenHW电视集团介绍我们自己的Sven Beyer, RISC-V产品经理,了解更多关于OneSpin如何有助于验证工作。

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

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

要了解更多关于OneSpin如何确保你的RISC-V设计的完整性,下载我们的白皮书,“确保RISC-V核心和soc的完整性,”在https://www.onespin.com/resources/white-斑点



1评论

柯克• 说:

我也一直在开发两个RISC-V cpu。一个是基于我创建的一个新的动态指令调度算法的乱序算法,另一个是基于开源的5阶段流水线RV32i的算法。我对开源的目标是使它高度参数化,以便可以创建许多不同的版本,并作为正式验证测试设置的载体,以测试这个和其他基于RISC-V的CPU。这真是一件苦差事。目前工作的rv32imcicsr与许多衍生的基础上扩展和各种参数,可以改变。RISC-V的真正问题是验证。具体来说,正式的验证。现在有很多RISC-V cpu满足了一些“黄金模型”,但我不确定它有多黄金,因为还没有一个正式的规范。据我所知,SAIL并没有涵盖太多内容,尤其是涉及到csr等。我加入了正式组,以保持标签,看看是否可以帮助,但在此期间,我一直在开发一个系统Verilog模型,我用它来验证我的测试CPU和它的衍生物。 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.

留下一个回复


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