检测大容量的关键错误在一个开源核心芯片与正式的验证。
RISC-V电子设计行业继续占据头条新闻。你可能已经看到了最近的新闻,OpenHW集团是交付第一RISC-V核心,CV32E40P。如果你参加了上个月的RISC-V峰会,或许你参加“CORE-V:工业品位开源RISC-V核心”里克·奥康纳OpenHW集团的总裁。在这个会话中,里克。讨论了如何组织与OneSpin和其他几个验证合作伙伴开发CORE-V-VERIF silicon-proven,工业级功能验证平台。这个平台是用于执行的完整验证CORE-V CV32E40P和目前被用来验证CV32A6 CV64A6内核。
CV32E40P核心将用于大容量、商业芯片项目,严格诚信标准。OpenHW集团认识到,仅使用仿真核心将容易发现关键错误,不完整的覆盖,和/或忽视隐藏指令和他们充分认识到这些功能错误,验证缺陷可能导致安全问题,安全漏洞。为了补救,CORE-V-VERIF平台超越模拟包括OneSpin独特的形式验证技术,实现快速,它已证明是至关重要的成功,没有错误CV32E40P核心的交付。
里克·奥康纳理解的影响正式对实现完整的验证:“OneSpin独特的技术是一种理想的贡献OpenHW验证任务组帮助识别错误,模拟就会错过了。OneSpin解决方案允许任务组实现必要的覆盖率达到功能性RTL冻结的结果目标的速度和质量。“高praise-thanks,瑞克!但OneSpin究竟是如何运转与OpenHW组验证CORE-V核心?协作发生从地上起来,继续在整个验证过程。
OneSpin第一OpenHW验证任务组密切合作,开发一个正式的验证计划。基于OneSpin然后增强SystemVerilog / UVM CORE-V验证试验台模拟工作。断言用来证明核心实现/ RTL模型符合ISA;这些断言是自动生成或手工编写覆盖所有项目的计划。代码覆盖率、突变的报道和综述了断言覆盖率增加信心,所有项目的计划已经解决。一旦试验台实现,运行时在几天内完成和调试是在短短几分钟内完成。OneSpin发现许多关键错误:八正常和异常相关特权指令和其他相关规范。OneSpin敏捷方法允许调整的形式验证进度满足OpenHW验证任务组的验证重点最大化代码冻结的结果。最终的结果是全面和完整的验证在很短的时间内。
硅实验室有一个前排座位在验证期间的努力,因为他们帮助领导OpenHW验证任务组。验证经理史蒂夫·里士满硅实验室和工作组的联合主席,说:“CV32E40P核心是第一个开源核心与最先进的大容量芯片验证流程所需的高度集成,商业出类拔萃。OneSpin是一个关键因素。的OneSpin RISC-V完整形式验证解决方案系统检测到个别案例异常逻辑错误和管道。这些问题只会触发指令序列在罕见的情况下,内存摊位和控制和状态寄存器编程。Constrained-random模拟测试来找到这些问题需要大投资开发和仿真时间。”
阿扬架子,硅实验室的首席架构师和主席OpenHW核心任务组,接着说:“确定问题的根源是令人印象深刻的,大量节省调试。解决方案还显示几乎为零的噪音检测真正的RTL的bug,而不是其他方法问题的报道往往会导致在验证环境修复。”
查看OpenHW电视播出的名为“深入探究的形式验证CORE-V CVE4”我们的斯文拜尔、RISC-V产品经理,了解更多关于如何OneSpin导致验证工作。
任何人考虑使用RISC-V作为他们的下一个设计的一部分理解开源架构提供的定制和灵活性。然而,处理器验证一个新的需求,用户将不得不承担。重要的是要注意,任何用户优化或添加自定义指令需要一个完整的重新核定,以防止同样的潜在问题,前面提到的恶意插入可能导致。实现权力的复杂的微体系结构、性能和区域目标,结合大量教学组合,缓存,中断,例外,和无数的自定义扩展,都需要被完全证实。更为复杂的验证需要确保核心是正确的指令集架构(ISA),以及RTL匹配ISA。
的OpenHW CV32E40P核心完全验证并准备使用,但是仍有一些设计师验证挑战需要克服当集成的核心:尤其是在这种情况下,核心是定制的。这样一个核心,和其他RISC-V核心喜欢它,应该re-verified集成或定制后,确保任何变化没有引入新的错误或产生不必要的动物的形式验证的方法消除风险和详尽的证明一切都是应该的。
了解更多关于OneSpin如何保证RISC-V设计的完整性,下载白皮书,“保证RISC-V核的完整性和sochttps://www.onespin.com/resources/white-papers。
|
|
|
|
|
|
|
|
|
我也一直在开发几个RISC-V cpu。的订单是基于一个新的动态指令调度algorthim我创建,另一个是一个开源5阶段管线式RV32i基础。开源的我的目标是使其高度参数化,这样可以创建许多不同的版本和作为一个正式的验证测试车辆设置测试这个和其他RISC-V基于CPU的。这是很烦人的。目前致力于RV32imcZicsr许多衍生品基础上扩展和各种参数,可以改变。RISC-V的真正问题是验证。具体来说,正式的验证。有很多RISC-V cpu遇到一些“黄金模式”,但我不确定它有多金,其实没有一个正式的规格。帆,从我所看到的,没有涵盖太多,特别是在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.