Chisel高层电路设计的转换和验证方法

1. 成果简介

Chisel作为开源的硬件构建语言，在目前流行的RISC-V处理器设计和敏捷硬件开发中发挥重要作用。Chisel将硬件构造原语添加到Scala编程语言中，为硬件电路设计用户提供了现代编程语言的能力，可以编写复杂的、参数化的电路生成器，生成可综合的Verilog/System Verilog代码。用户可以创建可重用的组件和库以适应不同的具体应用场景，提高设计中的抽象级别，同时保留细粒度控制。

目前对Chisel电路设计的验证针对Chisel生成的具体电路进行。执行Chisel代码生成较高级的HiFIRRTL代码；展开、化简、整理得到结构和语法简单的LoFIRRTL；对LoFIRRTL或进一步转换得到的Verilog/System Verilog、BTOR2等格式进行仿真或形式化验证。

这些验证方法并不能完全说明Chisel高层电路设计本身的正确性。在生成电路的过程中，Chisel设计中的参数会被实例化，参数的控制信息丢失；Chisel高层次设计中的代码结构会被破坏。由此生成的最终编码，仅能表示特定参数下的一种电路设计，不能表现Chisel高层次设计中的语义和结构信息；基于该编码进行的验证工作，仅能说明Chisel设计在特定参数下正确性，不能说明Chisel高层电路设计整体的正确性；对于不同参数下的电路，需要枚举参数分别进行验证。

针对以上问题，课题组提出了一种Chisel高层电路设计的转换和验证方法。通过对Chisel高层电路设计代码本身的分析、排序和处理，转换生成一种Scala模拟代码，保留了Chisel设计的参数化信息及大部分的结构信息；通过语句重排序的机制，解决了Chisel硬件设计语义与顺序执行软件语义不一致的问题；提供了与Chisel中硬件设计原语对应的Scala模拟库；通过Scala上的形式化证明工具Stainless对电路功能进行了形式化验证；提出了针对上述Scala模拟程序的性质编写方法和证明策略。

通过该方法，可以对Chisel硬件设计进行带参数的高层形式化验证，验证Chisel设计的电路在不同参数下均保持功能正确性；还可以解决Chisel生成电路的规模随参数增大带来的验证问题。

2. 技术先进性

该工具先进性主要体现在以下方面：

（1）通过软件验证的方法和工具对Chisel硬件设计进行高层验证。

（2）转换后的Scala模拟代码表达Chisel电路设计的高层语义，可以对包含生成电路在内的完整Chisel功能进行验证。

（3）保留Chisel设计参数信息，在形式化验证中可以带参数进行验证，证明Chisel电路设计在不同参数下的正确性，避免待验证电路规模随参数膨胀。

（4）保留Chisel设计结构信息，保留设计者原始的功能模块和段落划分，体现用户设计意图，便于利用软件验证和分析方法。

3. 技术成熟度

该方法已经形成相应工具，已在硬件电路验证合作项目中应用，可推广使用。

4. 可应用领域

电子设计自动化，硬件电路设计与验证

5. 联系人

刘易铖，liuyc@ios.ac.cn，15890069966