RISC-V微控制器形式化方法研究
Research on Formal Verification Method of RISC-V Microcontroller
DOI: 10.12677/CSA.2020.106129, PDF,   
作者: 潘 越, 程子敬：航天恒星科技有限公司，北京
关键词: 微控制器；RISC-V；形式化验证；电子设计自动化；Microcontroller； RISC-V； Formal Verification； EDA
摘要: 电力物联网系统内大量部署了嵌入式微控制器。在航天恒星自主研发的输配电杆塔稳定性监视系统的地面通信节点中，必须保证起核心作用的嵌入式微控制器的功能正确性。由于验证处理器功能正确和完备性与其它ASIC电路相比更为困难，本文分析了一种基于RISC-V指令集的微控制器形式化验证方法。该方案具有形式化验证的一般优点：基于开源的工具链，搭建简单，自动化程度高，适用于低成本微控制器的功能验证解决方案。
Abstract: 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.
文章引用：潘越, 程子敬. RISC-V微控制器形式化方法研究[J]. 计算机科学与应用, 2020, 10(6): 1252-1258. https://doi.org/10.12677/CSA.2020.106129

参考文献

[1] 徐晓寅. 信息通信技术支撑泛在电力物联网建设[J]. 通信电源技术, 2019, 36(12): 186-187.
[2] 周小艳, 何为, 胡国辉. 基于ZigBee无线传感器网络的变电站人员定位的改进算法研究[J]. 电力系统保护与控制, 2013, 41(17): 56-62.
[3] 柏钰昇. 关于智能电网对智慧城市的支撑作用的分析[J]. 工业设计, 2017(9): 130-131.
[4] 余贻鑫. 智能电网实施的紧迫性和长期性[J]. 电力系统保护与控制, 2019, 47(17): 1-5.
[5] 李易. 泛在电力物联网在电力系统中应用的展望[J]. 科技创新与应用, 2019(22): 175-176.
[6] 雷思磊. RISC-V架构的开源处理器及SoC研究综述[J]. 单片机与嵌入式系统应用, 2017, 17(2): 56-60+76.
[7] 刘益青, 高伟聪, 魏鹏, 等. 基于MCU + DSP多处理器构架的微机保护硬件平台设计[J]. 电力系统保护与控制, 2010, 38(10): 89-91+95.
[8] 李其高. 面向IoT终端设备的RISC-V微控制器设计与分析[J]. 单片机与嵌入式系统应用, 2018, 18(3): 64-66+69.
[9] 贾琳, 樊晓桠. 32位RISC微处理器流水线设计[J]. 计算机工程与应用, 2005(14): 115-117.
[10] 郑飞君, 严晓浪, 葛海通, 等. 使用布尔可满足性的组合电路等价性验证算法[J]. 电子与信息学报, 2005(4): 651-654.
[11] Wintersteiger, C.M., Hamadi, Y. and De Moura, L. (2013) Efficiently Solving Quantified Bit-Vector Formulas. Formal Methods in System Design, 42, 3-23. [Google Scholar] [CrossRef] 
[12] Kovásznai, G., Fröhlich, A. and Biere, A. (2016) Complexity of Fixed-Size Bit-Vector Logics. Theory of Computing Systems, 59, 323-376. [Google Scholar] [CrossRef] 
[13] Olivo, O. and Emerson, E.A. (2011) A More Efficient BDD-Based QBF Solver. In: International Conference on Principles and Practice of Constraint Programming, Springer, Berlin, 675-690. [Google Scholar] [CrossRef] 
[14] 朱峰, 鲁征浩, 朱青. 形式化验证在处理器浮点运算单元中的应用[J]. 电子技术应用, 2017, 43(2): 29-32.
[15] 郭莹. 布尔可满足性问题研究综述[J]. 软件导刊, 2017, 16(5): 204-206.
[16] 王翀, 吕荫润, 陈力, 等. SMT求解技术的发展及最新应用研究综述[J]. 计算机研究与发展, 2017, 54(7): 1405-1425.
[17] Bouton, T., De Oliveira, D.C.B., Déharbe, D., et al. (2009) veriT: An Open, Trustable and Efficient SMT-Solver. In: International Conference on Automated Deduction, Springer, Berlin, 151-156. [Google Scholar] [CrossRef] 
[18] 李东泽, 曹凯宁, 曲明, 等. 五级流水线RISC-V处理器软硬件协同仿真验证[J]. 吉林大学学报(信息科学版), 2017, 35(6): 612-616.