Axiomise通过形式验证公理化RISC-V处理器

尽管由于开源架构设计新的微处理器在经济上是可行的，但测试和验证仍然是主要障碍。

随着 RISC-V 等开源处理器架构的出现，芯片设计变得越来越大众化，越来越多的组织敢于涉足处理器设计，从嵌入式微控制器到高端台式机和服务器级 CPU，包括人工智能(AI) 和机器学习 (ML) 设计。

验证挑战

尽管由于开源架构设计新的微处理器在经济上是可行的，但开发周期的测试和验证部分仍然是主要障碍，一些人估计这些活动占芯片总成本的 70% 左右发展。此外，当发现芯片存在制造前未发现的功能缺陷（错误）时，这不考虑遗漏错误和重新设计的成本。人们必须只关注 Spectre 和 Meltdown 等安全漏洞的后果，这些漏洞几乎影响了地球上的所有处理器，无论供应商是谁，包括 Arm、英特尔和 AMD 等大牌。

那么，我们如何期望未来的芯片设计能够抵御这些使芯片容易受到黑客攻击的恶意漏洞？我们如何知道该芯片将继续按预期在航空航天和国防领域工作，并且不会由于测试和验证期间未发现的有意和无意的错误而出现异常？

答案在于查看形式验证，这是唯一可以提供错误不存在“证明”并提供设计和规范中错误的可证明证据的验证技术。

公理化 RISC-V 处理器的正确性

在Axiomise，我们使用行业标准、非专有 SystemVerilog 断言 (SVA) 开发了一个新的形式证明工具包，用于基于已发布的 RISC-V ISA 建立 ISA 合规性，我们已经使用了这个确定给定的处理器实现是否符合 ISA 语义。

 

Axiomise RISC-V 正式证明套件（来源：Axiomise.com）

 

 

我们的解决方案完全与形式工具供应商无关，不需要修改设计，并且只需要最终用户熟悉 Verilog/VHDL。此外，我们的方法可重复用于其他 RISC-V 处理器。我们的“公理化”方法是使用 SystemVerilog 断言的开放标准构建的，并通过我们的抽象和问题减少工具包增强了性能。我们在实践中部署了我们的方法，以确保我们可以确定处理器的所有功能/安全/安全/电源要求都转化为设计实现的可证明有效的公理（属性）。

方法论

检查的一般策略依赖于使用观察模型观察从发出点到完成点的所有指令的路径，其中非确定性允许其他指令交错穿插在特定指令的发出和完成之间被检查。这确保了我们可以捕获各种受控制和并发控制并可能导致错误结果发生的错误。

重要的是要强调，必须对每条具有不确定性的指令进行端到端检查，因为在实践中，由于测试的非常直接的性质，大多数错误都被遗漏了，这些测试专门探索了从问题到完成的定向路径，但不一定允许其他指令干扰。

对于大多数说明，我们通常会围绕观察因果关系编写一项检查。对 LOADS 和 STORES 的检查是使用内存的完整接口构建的，通过该接口我们检查 LOADS 和 STORES 的所有变体 - BYTE、WORD、HALF-WORD、对齐和未对齐。这使我们能够检查不同风格的 LOADS 和 STORES 之间所有可能的依赖关系，尤其是当一个序列具有指向同一地址的这些依赖关系时。

在某些情况下，在开发过程中，我们还发现了我们在测试开发阶段引入的错误。其中大部分是由于我们对 RISC-V ISA 的理解有误。值得庆幸的是，根据设计师的反馈，我们能够将其与 ISA 的要求保持一致。单击此处了解有关性能的更多详细信息、我们发现了哪些错误、我们能够获得多少证明、需要哪些运行时以及我们如何签署验证以完成。

总结

我们的目标是进行端到端的形式验证，但存在以下限制：

（a）我们的工作是在访问受限的设计师之外进行的，

（b）我们没有设计微架构的先验知识，

（ c) 我们没有描述接口和内部状态机的全面、详细的规范。

在许多方面，我们的工作代表了现代设计验证的现实，其中忙碌的设计师通常不会记录详细的微架构规范，初始验证通常由设计师自己使用模拟在本地进行，或者关于规范的知识是口口相传给独立验证设计的验证工程师。

据我们所知，这是第一个独立于特定形式验证工具供应商的形式验证解决方案，它使用所有工具都支持的 SVA 开放标准，并且需要最少的设置，保证大于 99% 的证明收敛.

您可以立即使用我们的证明工具包，并使用您选择的形式验证工具开始在您的 RISC-V 设计中查找错误并构建错误不存在的证明。

请单击此处了解我们的解决方案与其他解决方案有何不同以及我们在微处理器验证三个十年的历史。