RISC-V处理器Chisel设计指令集一致性形式验证方法

1. 成果简介

RISC-V是一个新兴的开源精简指令集架构，由加州大学伯克利分校在2010年首次发布。RISC-V通过对现有指令集架构的学习，吸收了现有各体系结构的优点，去除了对历史遗留问题的顾及和旧有技术的依赖。RISC-V作为精简指令集，包含较少种类的指令，同时采用模块化设计，保留大量的自定义编码空间，允许用户根据需求进行精简或扩展。

Chisel同样由伯克利提出，是一种嵌入到Scala中的新型硬件构建语言，为用户提供了现代编程语言的能力，可以编写复杂的、参数化的电路生成器，生成可综合的Verilog代码。Chisel在目前流行的敏捷硬件开发中发挥重要作用，已经广泛用于RISC-V处理器的RTL设计。

处理器设计的基本功能要求是符合对应指令集规范。对于使用Chisel语言设计的RISC-V处理器通常通过测试方法进行验证。其问题在于不能对处理器设计进行完备的验证，即通过测试不能完全保证设计的正确性。对Chisel生成的Verilog进行测试或形式验证的方法，延长了工具链，需要再根据生成的Verilog代码与不同的工具对接，实现较为困难。

针对以上问题，课题组提出了一种针对RISC-V处理器Chisel设计基础和特权指令集的一致性形式验证方法。通过一个模块化、与原文对应、可参数化配置的参考模型描述RISC-V指令集规范的行为，减轻了验证人员对形式化验证知识的需求，无需人工编写待验证的性质；通过一系列同步接口和辅助工具，简化了待验证处理器设计和参考模型之间的连接，并可以方便地设置验证范围。对于特权指令和异常处理，设计了相应全局处理函数；通过组合电路逻辑代替状态机实现了虚拟内存机制，并设计了相应访存接口。最终使用形式化方法中的模型检测技术，对指定的验证范围，如果存在设计问题则一定能发现；全部验证的连接与配置工作在Chisel代码中完成，当发现错误时，可以返回对应波形反例。

截至目前，基于该方法实现的工具已经支持RISC-V32/64位I、M、C、Zifencei、Zicsr、Zb系列扩展指令，支持M、S、U特权级，并已在果壳、香山、Boom等顺序、乱序的开源Chisel处理器设计上到验证。

2. 技术先进性

该技术先进性主要体现在以下方面：

（1）通过一个模块化、与原文对应、可参数化配置的参考模型描述RISC-V指令集规范的行为，减轻了验证人员的知识需求，无需人工编写待验证的性质。

（2）通过一系列同步接口和辅助工具，简化了待验证处理器设计和参考模型之间的连接和使用。

3. 技术成熟度

该技术已形成产品，可应用推广可应用领域。

4. 可应用领域

该技术可应用于电子设计自动化，硬件电路设计与验证，处理器设计。

5. 联系人

申世东，shensd@ios.ac.cn，19929931316