1. 引言
顺应我国经济社会的发展要求，对公共电力基础设施适应高新技术产业提出了“智能化”的更高要求 [1]。“智能电网”将电力资源高效率地输送、调配，保证供电质量和稳定 [2] [3]。智能化设施将海量的传感器设备和通信节点布设到电力系统中，形成电力物联网系统 [4] [5]，其运算能力的主要承载者来自于大规模部署的嵌入式控制器 [6]。因此，智能化广泛在电力物联网的实现需要大量经过功能验证的微控制器，尤其是在涉及到电力等关键基础设施的情况下，需要严格地保证软硬件的功能正确性 [7] [8]。
RISC-V是一种新兴的开源指令集，具有简洁、紧凑、模块化、易于实现的特点，是近几年国内外处理器研发创业公司的首选 [6] [9]。对处理器进行功能验证不同于其它ASIC的验证 [10]，在于任何处理器的实现需要符合它依赖的指令集规则。在目前，很多实现将能够运行定点/浮点性能测试程序，或Linux操作系统作为其功能正确性的标志，但这类方法往往不能穷尽所有的测试用例，而高级语言的编译器也可能隐藏硬件中的一些设计错误。对处理器或其它复杂硬件最可靠的功能验证方式是形式化验证，通过数学证明检查硬件实现与一套预设规则集是否等价。形式化验证能够系统地、完备地发现设计中的错误，或证明设计中没有错误 [11]。
在后续的章节，首先对适用于RISC-V控制器设计的形式化验证流程进行概述，然后分析了RISCV-Formal，一个用于发现设计错误的开源工具链，最后将该工具链应用于一个具体的RISC-V嵌入式处理器实现。
2. 形式化验证流程
处理器形式化功能验证流程要解决的两个问题是：已知一个处理器电路的设计和其寄存器合法的初始状态，1) 处理器是否会运行到某些不可接受的状态，称为安全属性(Safety Property)；2) 一些可接受的的状态是否可以运行到，称为活跃属性(Liveness Property) [12]。证明形式分为有界检查和无界检查，有界检查仅考虑从初始状态开始经过预设的时钟数后是否存在属性违例；无界检查则推测经过任意时钟数后是否会存在属性违例，通常通过k步数学归纳法验证 [11] [13]。
如图1所示，RISC-V形式化验证分为三个主要步骤：1) 产生/获取对指令集的形式化规约；2) 在硬件设计过程的关键点中插入断言；3) 对HDL代码进行属性证明 [14] [15]。
2.1. 形式化规约
在一开始，处理器指令集架构是以自然语言发布的规范文档，它规定了一个处理器要实现或兼容此指令集的设计需要能够处理哪些指令，指令的格式，以及运行指令产生的后果。指令集架构规范是与具体的机器无关的 [1]。
Figure 1. RISC-V formal verification workflow
图1. RISC-V形式化验证流程
自然语言描述的规范可能带有各种歧义或疏漏。为了避免阅读时产生歧义，进一步便于作为自动化证明系统的输入，程序语言规约用规范的方式定义和描述。程序化的规约也和机器实现无关 [10]。
2.2. 插入断言
现代处理器通过硬件描述语言(HDL)设计。HDL的硬件描述通过综合器输出为逻辑门构成的网表格式，或直接在仿真器上运行。
设计错误本质上就是对规约的违反，因此要在仿真时发现这些违例，可通过在代码中加入断言的方式表征处于安全状态时处理器状态所必须具备的特性。
YOSYS综合器支持四种断言，如下表1所示：
Table 1. Four categories of assertions
表1. 四种断言类型
在编写代码时，断言结构一般被内嵌于一个独立的always-case结构中，用于捕获电路部分信号之间的关系。assume断言和assert断言用来组成安全特性规则，出现assert语句内的表达式为假时，判断安全特性违例；cover断言用来构造活跃特性规则，如果cover语句内的表达式能够在有效的步数内取得一次真，则说明所监视的状态可达，因此cover语句只能在有界模型中测试。
2.3. 形式化证明
当前广泛用于硬件验证的软件是基于可满足性模块理论(Satisfiability Modulo Theories, SMT)的固定规模布尔变量证明器，典型的有Z3、Yices 2、CVC4、boolector等 [10] [16]。SMT证明器的输入是一组变量声明和一组断言，然后通过无量词的皮尔斯伯格自动机算法决策这组断言是否能够被满足 [17]。表2是一个SMT-LIB 2格式的输入实例，它描述了RISC-V指令集中的add指令所必须满足的特性。
Table 2. SMT input example—instruction add
表2. SMT输入实例——add指令
在表2中，断言(assert(not(= (select(regf, rd)), sum)))宣布从regf的索引rd处读取的值一定等于sum，在此将其取否，通过(chech-sat)命令求解是否存在使整个表达式为真的赋值；当证明器找到一个解时返回sat，无解时返回unsat。由于希望断言恒成立，则等价于其否断言无解。证明处理器实现的指令行为符合规约是否符合规约则转换为该指令对应断言的否是否无解，这是进行符合性验证的一般思路 [11] [13]。
3. 形式化验证工具链
虽然在上述的三个步骤中，可选取的开源或闭源工具有很多，但是RISCV-Formal是一整套依托于开源工具的验证框架。RISCV-Formal的主体部分是HDL综合器YOSYS的前端工具SymbiYosys，这一工具可将YOSYS的综合输出网表转交给后端的SMT证明引擎。SymbiYosys支持多种SMT证明器，包括有界模型和无界模型的工作模式。在有界模式下，SymbiYosys每个周期把电路状态的快照翻译成命题逻辑，由证明器解析；在无界模式下，它仍然先进行一次完整的k步有界检查，如果正确，它再尝试进行k步归纳，证明第k + 1步的状态一定正确。
在YOSY断言分类下，assume、assert、cover、restrict断言和SMT输入格式有一一对应的关系。
1) assume和restrict断言对于证明器是同一种，它们都被转换成(declare-)赋值，这些确定的变量作为已知的皮尔斯伯格自动机输入序列，可以减少证明的时间；
2) cover断言被原样地转化成SMT断言，当证明器找到一个解时，说明断言描述的状态是可达的；
3) assert断言被转换成取否的SMT断言，如果证明器发现了一个解，则说明发现了一个不符合性问题，这个解的变量赋值情况被解析成波形文件报告给用户，告知这一非法状态是如何到达的。
RISCV-Formal能够验证两种形式化符合性问题，它通过以时钟周期为单位调用证明器求解状态来解决这两种问题，它们调用证明器的时机和求解的问题如下：
对单条指令行为进行的端到端有界模型检查。在每个用户使能的指令测试中，处理器首先无约束地运行预设的时钟周期，在最后一个周期时，证明从提交单元交付的每个指令字的交付前/交付后状态符合规约。
对多条指令序列的行为进行一致性有界模型检查。在该模式下，检测器先在复位状态下运行N个周期，再在置位状态下运行M个周期；在M个周期内，检测器任意选择一个周期锁存当前状态，然后在最后一个周期比对前后的状态。这一机制可以发现：PC一致性问题，即第k条指令注册的PC是否与第k + 1条指令读取的PC相同；寄存器一致性问题，即对同一寄存器的写入和读取的结果是否匹配；活跃性问题，即某条指令提交后，有后续的指令继续执行；因果关系，即对前一指令存在依赖关系的指令是否提前提交。
通过这些测试用例的实现将可以保证符合最基本的RISCV-32I规范。除去正确地实现合法指令及流水线外，该控制器必须能够发现未定义的非法指令，这意味着指令译码逻辑必须是完备的(在译码合法指令时总返回真，译码非法指令时总返回假)。截至到本文撰写时，RISCV-Formal尚未支持64I和32E两种变体，考虑到微控制器基本是32位的，选择32E的实现需要临时补全32个寄存器的寄存器文件。
4. 应用实例
在图2的智能电力巡检系统中，提出了一种在丘陵、山地地形，气候恶劣，经常有大风暴雨的环境下，对电力传输杆塔进行远程智能监控的解决方案。在这一方案在被控地区的传输塔体上安装多种传感器(倾角传感器、位置传感器、结构应力传感器等)，这些不同制式的数据在地面通信节点汇总，进行转换处理后中继到卫星或附近的基站。通信节点需要用到一款微控制器作为融合传感器到卫星链路/基站的协议转换节点 [1]。我们希望通过一个自主研发的RISC-V核心代替基于ARM Cortex-M的核心。
PICORV32是一款小面积、低功耗，具有相当可配置性的RISC-V 32位实现。通过控制描述文件的宏定义，它可以配置为支持压缩、乘法扩展，并可以选择32E或32I中的一种基础整数值指令集。它还带有一个可选的中断控制器，以及AXI-Lite或Wishbone内存总线。
RISCV-Formal为PICORV32准备了76个单指令测试用例，覆盖了全部整数指令，部分常用的控制与状态寄存器指令和它们的汇编别名。其它测试包括：单字只读内存模拟，用于检查内存系统到检查器的路径上是否存在问题，指令内存和数据内存均可以被测试；等价性测试，形式化地证明电路在移除RISCV-Formal逻辑前后功能等价；完备性测试保证非法指令不被提交。
为了测试RISCV-Formal的工作流程，在PICORV32的源文件中注入了一个常见的bug。因为RISC-V的最小指令长度为16位，因此所有指令的地址应当至少是16的整数倍；在规约中，跳转并链接寄存器指令JALR会把一个符号扩展的立即数和一个链接寄存器相加，将结果的最低位直接清零后，作为新的取指地址写入PC。有些实现忘记把最低位清零，或只是把写入PC的副本最低位清零。表3中进行的替换复现了这一bug。
在替换后，对JALR指令的测试用例发现了这一错误，并生成了一个违例的反例，用户可以通过波形查看软件分析反例的波形(如图3)。因为这一bug，RISCV-Formal检查器取回的下一条PC值与预期的不符，报告错误的指令的细节在最后一个周期从rvfi_*端口中读取，例如编码和操作数可以分别从rvfi_insn和rvfi_rs*_rdata输出信号中获取，这可以为除错工作指明方向，提高排查效率。
Figure 3. JALR counterexample waveform
图3. JALR反例波形图
5. 结论
在实际的测试中，RISCV-Formal确实发现了一些被高层次软件屏蔽的处理器实现错误。
当然，这套工具仍然存在一些实用性的问题。例如目前，它没有实现从程序规约文件推导断言测试用例的能力；这意味着从指令集规范到sby测试用例是由开发者编写的，这在很大程度上削弱了程序规约的使用价值；此外，RISC-V规范的草案版本除整数指令集外正处于快速迭代中，一些模块的定义或设计逻辑发生了根本的变化(例如此前所有强制要求的计数寄存器被移除出基础指令集，而转为统一的控制与状态寄存器指令)，那么下一版本的定案规约将同目前的版本有很大差异，如何充分利用社区的劳动成果，把机器无关的程序规约转化成具体的、机器相关的HDL断言是一件很有价值的工作。
推广RISCV-Formal及类似形式化验证框架的意义在于，让形式化方法在小规模电路设计(不仅限于微控制器)团队中普及起来，让硬件验证成为一门严谨的数学，有助于提高数字产品设计研发的质量，提高IC设计行业的整体水平 [8] [18]。
最后，硬件的形式化验证可以从根源上排除功能设计上的错误，不仅限于处理器的设计，还适用于其它种类数字电路，乃至软件系统的设计 [9] [18]。目前，国内应用形式化验证的正式系统实现尚较为缺乏，这使得开源硬件运动缺少与涉及国计民生的关键应用结合的自信。推广形式化验证工作方法有助于进一步推进我国IT/IC事业的蓬勃发展，将开源硬件/软件的资源和成功转化到这些关键系统领域中。