(资料图)

作者：Laurent Arditi, Paul Sargent, Thomas Aird
职务：Codasip高级验证/形式验证工程师

RISC-V的开放性允许定制和扩展基于 RISC-V 内核的架构和微架构，以满足特定需求。这种对设计自由的渴望也正在将验证部分的职责转移到不断壮大的开发人员社群。然而，随着越来越多的企业和开发人员转型RISC-V，大家才发现处理器验证绝非易事。新标准由于其新颖和灵活性而带来的新功能会在无意中产生规范和设计漏洞，因此处理器验证是处理器开发过程中一项非常重要的环节。

在复杂性一般的RISC-V 处理器内核的开发过程中，会发现数百甚至数千个漏洞。当引入更多高级特性的时候，也会引入复杂程度各不相同的新漏洞。而某些类型的漏洞过于复杂，导致在仿真环节都无法找到它们。因此必须通过添加形式验证来赋能 RTL 验证方法。从极端漏洞到隐匿式漏洞，形式验证能够让您在合理的处理时间内详尽地探索所有状态。

在本文中，我们将介绍一个基于形式验证的、易于调动的 RISC-V 处理器验证程序。与 RISC-V ISA 黄金模型和 RISC-V 合规性自动生成的检查一起，展示了如何有效地定位那些无法进行仿真的漏洞。通过为每条指令提供一组专用的断言模板来实现高度自动化，不再需要手动设计，从而提高了形式验证团队的工作效率。

1、基于先进内核的处理器开发

嵌入式系统的应用越来越广泛，同时对处理器的性能、功耗和面积（PPA）要求越来越高，因此我们将这样的产业和技术背景下用实际案例来分析处理器的验证。Codasip L31 是一款用于微控制器应用的 32 位中端嵌入式 RISC-V 处理器内核。作为一款多功能、低功耗、通用型的 CPU，它实现了性能和功耗的理想平衡。从物联网设备到工业和汽车控制，或作为大型系统中的深度嵌入式内核，L31可在一个非常小巧紧凑的硅片面积中实现本地处理能力。L31是通过 Codasip Studio 使用 CodAL 语言设计而成，该内核完全可定制，包括经典的扩展和特性，以及实现这些扩展和特性所需的高效和彻底的验证。

image001.png

表 1 Codasip L31内核展示了RISC-V处理器的优异特性