系统与设计
的意见

正式的验证RISC-V内核

RISC-V产品扩大,这是至关重要的,以确保他们符合ISA规范。

受欢迎程度

RISC-V是热的和站在什么可能是一个重大转变的开始。即使是一个粗略的即将召开的会议计划和最近的技术文章让清晰。虽然它仍然是在处理器体系结构的发展早期,当然可能RISC-V将IP和半导体行业的游戏规则的改变者。是“一个自由和开放的ISA启用一个新时代的处理器通过开放标准协作创新,“直接挑战了几个出色的处理器家族。这个定义来自RISC-V基金会认为支持与进化后的RISC-V EECS原始发展部门加州大学伯克利分校。

RISC-V指令集架构(ISA)设计与大量的可配置性的可选的扩展,如754 - 2008年IEEE浮点支持。它不是对特定技术架构或微体系结构风格,从而使各种各样的实现目前开源内核。任何人都可以设计一个核心或使用一分之一SoC (SoC)项目。正是这种开放和巨大的吸引力使彻底验证RISC-V核心必不可少的。与传统的处理器家族,只有一个或两个供应商已经提供核心芯片很多年了。供应商预计来验证他们的产品,是不同寻常的SoC设计人员认为他们必须re-verify核心许可证。

相比之下,已经有多个政党提供RISC-V核心和这个数字将在接下来的几年中显著增长。没有一个核心团队设计和验证这些核心。RISC-V生态系统的蓬勃发展,核心供应商需要一个独立的验证解决方案,以确保他们的设计兼容,符合ISA规范。彻底的验证是至关重要的成功对建立竞争处理器有多年的广泛的家庭硅验证和实现。同样,SoC开发人员必须确保他们许可的核心是充分验证和ISA-compliant。

超越功能正确性、核心供应商和用户面临的安全挑战,安全,和信任。许多RISC-V核心将被设计到产品有严格的功能安全要求。设计必须包括安全逻辑处理随机误差,如α粒子。标准ISO 26262等汽车电子需要验证的安全逻辑与计算失败的可能性。

此外,许多RISC-V核心将用于应用程序必须从对手的攻击是安全的。核心(SoC)的设计必须为安全漏洞进行分析,可以利用人希望控制系统。后果等应用自主车辆,核电站和军事/航空确实可能是可怕的。对手的攻击可能是由于硬件木马或其他恶意逻辑插入到核心由流氓个人或工具(SoC)的设计链。验证过程必须包括检测任何此类违反信任。

所有这些挑战导致一个不可避免的结论:RISC-V核心必须正式验证。正式工具可以保证核心设计实现了ISA,缺少所需的功能而不插入任何故意或意外的行为违反了ISA。这包括检查安全漏洞的设计和检测任何硬件木马。只有正式的工具不仅可以证明,设计做它应该做什么,而且它做的是什么应该做的。正式的应用程序(应用程序)也可以分析功能安全的核心设计和计算错误和失败指标所要求的安全标准。

发展的RISC-V生态系统,最好是如果可以由第三方工具和形式验证IP。这使得多个核心供应商验证相同的解决方案,建立它作为一个事实上的标准。SoC提供商许可开源内核可以使用相同的工具和IP筛选潜在核和仔细检查合规以及坚持安全、安全、信任的要求。记住这些目标,OneSpin最近推出了我们RISC-V完整性验证的解决方案。

我们的解决方案正式RISC-V ISA在一组SystemVerilog断言(上海广电)。这些断言定义的结果为每个指令,执行指令解码完成。有限数量的断言可以覆盖任何RISC-V实现任意长指令序列。这种方法使100%的正式实施证据说明对ISA规范和保证核心是完全兼容的。它还检测到任何额外的功能超出了ISA规范,正式验证信任的核心不包含硬件木马或其他意想不到的功能。交付的解决方案被看作一系列应用程序利用尽可能按钮。它有足够的灵活性来验证用户添加自定义扩展同时确保合规不妥协。

我们已经使用现有RISC-V实现这个解决方案来验证和发现一些有趣的设计缺陷。我们将论文几家即将来临的事件,包括政府微电路应用和关键技术会议(GOMACTech)和在台湾RISC-V车间将分享报告,论文,结果当我们可以。与此同时,联系我们如果您正在开发或考虑许可RISC-V核心。我们期待着帮助创造一个丰富的生态系统。



留下一个回复


(注意:这个名字会显示公开)

Baidu