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

摘要

电力物联网系统内大量部署了嵌入式微控制器。在航天恒星自主研发的输配电杆塔稳定性监视系统的地面通信节点中，必须保证起核心作用的嵌入式微控制器的功能正确性。由于验证处理器功能正确和完备性与其它ASIC电路相比更为困难，本文分析了一种基于RISC-V指令集的微控制器形式化验证方法。该方案具有形式化验证的一般优点：基于开源的工具链，搭建简单，自动化程度高，适用于低成本微控制器的功能验证解决方案。 Embedded microcontrollers are widely deployed within power IoT system. It’s vital to guarantee functional correctness of the embedded microcontroller, which acts as core component in self-developed IoT ground communication node of transmission tower stability monitor by Spacestar. Since verifying the functional correctness and completeness of a processer differs from those of ASIC designs, a formal verification method for RISC-V based microcontroller is analyzed in this paper. This method incorporates the common merits of formal verification, based on open sourced tool chain. It is easily set up and highly automated, applicable as functional verification solution for low-cost microcontrollers.