RISC-V微控制器形式化方法研究

电力物联网系统内大量部署了嵌入式微控制器。在航天恒星自主研发的输配电杆塔稳定性监视系统的地面通信节点中，必须保证起核心作用的嵌入式微控制器的功能正确性。由于验证处理器功能正确和完备性与其它ASIC电路相比更为困难，本文分析了一种基于RISC-V指令集的微控制器形式化验证方法。该方

顺应我国经济社会的发展要求，对公共电力基础设施适应高新技术产业提出了“智能化”的更高要求[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]。