Chisel断言语言的类SVA扩展及形式化验证方法

1. 成果简介

Chisel 由加州伯克利的Bachrach等人于2012年提出，是一种基于Scala的硬件构建语言，具有参数化、模块化、复用性高的特点，已经被广泛使用于RISC-V处理器和片上系统（System On Chip）设计中。由于Chisel仍在活跃发展中，对于Chisel设计的形式化验证尚不充分。

基于上述背景，我们对Chisel的断言语言提出了一套类SVA的扩展，并提出了针对该断言语言的形式化验证框架，既支持Chisel设计的安全性质（Safety property）验证，又支持了活性性质（Liveness property）验证。

我们将SVA支持的部分序列算子和性质算子引入Chisel断言语言中，并利用Chisel和FIRRTL提供的Annotation和Target机制实现对断言的编译，在后端对编译后的断言进行语法上的简单处理，并调用外部工具Spot生成相应的Büchi自动机，进而将设计是否满足断言转化成判断设计对应的迁移系统与断言对应的Büchi自动机乘积是否为空。我们将乘积自动机略作调整并通过L2S算法将乘积自动机是否为空这一活性性质编码成安全性质（btor2格式），以适配目前的硬件模型检测工具。调用硬件模型检测工具（如BtorMC，rIC3)对生成的btor2文件进行模型检测，即实现了在设计中对断言所描述性质的形式化验证。

2. 技术先进性

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

（1）对Chisel断言语言的类SVA扩展：将SVA的部分序列算子和性质算子引入到Chisel断言语言中，以提高Chisel断言语言的表达能力。

（2）对Chisel设计的直接形式化验证：利用Annotation-Target机制保证断言中的信号与设计中的信号匹配；调用Spot来完成断言描述的时序逻辑公式到自动机的转化。

3. 技术成熟度

该技术处于小试阶段（实验室验证）。

4. 可应用领域

该软件应用于Java程序单元测试。

5. 联系人

于世禛，yusz@ios.ac.cn，13121802177