RISC-V处理器指令集体系结构（ISA）是当今电子领域中讨论最多的主题之一。许多会议论文和技术文章都讨论了RISC-V，并且还有更多计划。尽管RISC-V仍处于处理器体系结构发展的早期，但它可能是知识产权（IP）和半导体行业的革命性变化。RISC-V基金会将其定义为 “一种自由开放的ISA，通过开放标准的协作实现了处理器创新的新时代。” 因此，它直接挑战了成熟的处理器系列。任何人都可以开发RISC-V处理器内核或将它们集成到芯片上系统（SoC）设计中。基金会支持、标准化以及发展RISC-V ISA，而无需获得许可或评估任何特许权使用费。
RISC-V最初是由加利福尼亚大学伯克利分校的EECS部门开发的。ISA的设计具有大量可配置性，并具有可选扩展，例如IEEE 754-2008浮点支持和自定义指令。它不是针对特定技术或微体系结构样式而设计的，因此允许进行多种实现。事实上，现在开放源代码站点上可以使用多个处理器内核，甚至整个片上系统（SoC）项目。这种开放性和广泛的吸引力使对RISC-V内核进行全面验证至关重要。在传统处理器家族中，很多年以来都只有一两个供应商提供内核和芯片。供应商应该验证他们的产品，SoC设计人员通常会感到他们必须重新验证其许可的内核，这是不寻常的。
相比之下，已经有多家公司提供RISC-V内核，并且这一数字在未来几年中将大大增加。没有一个中央团队来设计和验证这些核心。为了使RISC-V生态系统蓬勃发展，核心供应商需要一种独立的验证解决方案，以确保他们的设计相互兼容并符合ISA规范。经过多年的广泛验证和芯片实施，彻底的验证对于与已建立的处理器系列成功竞争至关重要。同样，SoC开发人员必须确保他们许可的内核经过充分验证并且符合ISA。虽然RISC-V基金会提供了一些合规性支持，但这只是部分解决方案。
确保RISC-V实现的完备性远远超出了验证功能正确性的范围。内核供应商和集成商都面临安全、安保和信任的挑战。他们正将许多RISC-V的内核设计为具有严格功能安全性要求的产品。设计必须包括安全逻辑以处理现场的随机错误，包括阿尔法粒子切换存储位。诸如用于汽车电子设备的ISO 26262之类的标准要求验证安全逻辑并计算故障概率。核心集成商将坚持其供应商必须满足这些标准的严格要求，这也有助于认证其SoCs和最终产品的安全性。
另外，许多RISC-V内核将用于必须免受攻击的应用程序中。必须分析内核和SoC设计的安全漏洞，这些漏洞可能被想要控制系统的人利用。入侵自动驾驶汽车，核电厂和军事/航空安全漏洞的后果可能很严重。不法分子或设计链中的工具可以通过将硬件木马或其他恶意逻辑插入内核（或SoC）来辅助进行攻击。完备性确保过程必须包括对任何此类信任破坏的检测。
从所有这些挑战中得出一个不可避免的结论：必须对RISC-V内核进行广泛的验证，而形式技术起着关键作用。形式工具可以保证核心设计能够准确地实现ISA，不会丢失任何必要的功能，同时不会插入任何违反ISA的故意或意外行为。这包括筛选设计中的安全漏洞和检测硬件木马。只有形式工具可以验证其设计可以完成应做的事情，而且还可以验证它没有完成应做的事情。形式应用程序（apps）还可以分析功能安全性的核心设计，并计算安全标准所需的故障和失败指标。许多这类应用程序还在全芯片级别运行，以确保集成RISC-V内核的SoCs完备性。
对于RISC-V生态系统的发展，最好是可以通过第三方工具和IP进行合规性和完备性验证。这使多个核心供应商可以使用同一解决方案进行验证，并将其确立为事实上的行业标准。许可开源内核的SoC供应商可以使用相同的工具和IP来筛选潜在的内核，并仔细检查合规性以及对安全、安保和信任要求的遵守情况。考虑到这些目标，OneSpin最近推出了RISC-V完备性验证解决方案。
该解决方案在一组SystemVerilog断言（SVA）中将RISC-V ISA形式化。这些断言定义每条指令的结果，并涵盖任何RISC-V实作中从指令解码到完成的执行过程。这种方法为针对ISA规范的所有指令的实现提供了100％的形式验证，并保证内核完全合规。用户提供有关实施的信息，例如流水线级数，以将SVA映射到设计。该解决方案还可以检测ISA规范之外的任何其他功能，从而正式验证对内核不包含任何硬件木马或其他意外功能的信任。
RISC-V完备性验证解决方案将作为一系列应用程序交付，以尽可能简化使用过程。它具有足够的灵活性来验证RISC-V允许的用户添加的自定义扩展，同时确保不损害合规性。它已被用于验证开源RISC-V内核和SoC实现，发现有趣的设计错误和意外的功能。过去的几个月中，在一系列会议上已经介绍了这项工作的结果。这些结果为RISC-V社区提供了价值，同时对解决方案进行了验证，以确保处理器和SoC设计的完备性。
长按识别二维码关注北京开源芯片源码创新中心
联系我们：comms@baec.org.cn
