面向敏捷硬件设计的符号模拟器设计与实现

计算机工程与科学 ›› 2021, Vol. 43 ›› Issue (12): 2098-2104.

面向敏捷硬件设计的符号模拟器设计与实现

邹鸿基，李暾，罗丹，方雨德

（国防科技大学计算机学院,湖南长沙 410073）

收稿日期:2020-09-21 修回日期:2021-01-11 接受日期:2021-12-25 出版日期:2021-12-25 发布日期:2021-12-21
基金资助:
国家自然科学基金（U19A2062）

A symbolic simulator for agile hardware design

ZOU Hong-ji，LI Tun，LUO Dan,FANG Yu-de

（College of Computer Science and Technology,National University of Defense Technology,Changsha 410073,China）

Received:2020-09-21 Revised:2021-01-11 Accepted:2021-12-25 Online:2021-12-25 Published:2021-12-21

摘要/Abstract

摘要： 敏捷硬件设计方法中，RTL建模常使用自定义的描述语言，并将设计转换为某种中间格式，为设计验证带来了新挑战。符号模拟技术是(限界)模型检验、等价性检查和测试生成等验证技术的基础，为构建敏捷硬件设计方法验证技术基础，针对PyRTL语言及其中间格式，设计并实现了一个符号模拟器。介绍了符号模拟器的设计原理、转换规则等关键技术。实验结果表明了所实现的符号模拟器的正确性。

关键词: 符号模拟器, PyRTL, 敏捷硬件设计, 验证

Abstract: In the agile hardware design methodology, a domain specific hardware description language is often used for RTL modeling. This novel situation brings new challenges for design verification. In order to support design verification techniques such as (bounded) model checking and equivalence checking, a symbolic simulator is designed and implemented for PyRTL and its intermediate representations. This paper introduces the design principle, conversion rules and other key technologies of our symbol simulator. The experimental results show the correctness of the implemented symbol simulator.

Key words: symbolic simulator, PyRTL, agile hardware design, verification

邹鸿基, 李暾, 罗丹, 方雨德. 面向敏捷硬件设计的符号模拟器设计与实现[J]. 计算机工程与科学, 2021, 43(12): 2098-2104.

ZOU Hong-ji, LI Tun, LUO Dan, FANG Yu-de. A symbolic simulator for agile hardware design[J]. Computer Engineering & Science, 2021, 43(12): 2098-2104.

参考文献［5］

［1］	Lee Y,Andrew W,Henry C,et al.An agile approach to building RISC-V microprocessors［J］. IEEE Micro,2016,36(2):8-20.
［2］	Bahr R, Barrett C, Bhagdikar N, et al.Creating an agile hardware design flow［C］∥Proc of the 57th ACM/EDAC/IEEE Design Automation Conference 2020,2020:1-6.
［3］	Lattner C,Adve V.LLVM:A compilation framework for lifelong program analysis & transformation［C］∥Proc of International Symposium on Code Generation and Optimization,
20	04:75-86.
［4］	Clow J,Tzimpragos G,Dangwal D,et al.A pythonic approach for rapid hardware prototyping and instrumentation［C］∥Proc of the 27th International Conference on Field Programmable Logic and Applications (FPL),2017:1-7.
［5］	Deng Shu-jun,Wu Wei-min,Bian Ji-nian.Hybrid satisfiability solving for RTL verification ［J］.Journal of Computer-Aided Design & Computer Graphics,2007,19(3):273-278.(in Chinese)
［6］	Izraelevitz A M,Koenig J,Li P,et al.Reusability is FIRRTL ground:Hardware construction languages,compiler frameworks,and transformations［C］∥Proc of
20	07 IEEE/ACM International Conference on Computer-Aided Design,2017:209-216.
［7］	Daly R,Truong L,Hanrahn P.Invoking and linking generat- ors from multiple hardware languages using CoreIR［C］∥Proc of the 1st Workshop on Open-Source EDA Technology,
20	18:11.1-11.5.
［8］	Schuiki F,Kurth A,Grosser T,et al.LLHD:A multi-level intermediate representation for hardware description languages［C］∥Proc of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI),2020:258-271.
［9］	The satisfiability modulo theories library［EB/OL］.［2020-07-16］. http://smtlib.cs.uiowa.edu.
［10］	de Moura L,Bjrner N.Z3:An efficient SMT solver［C］∥Proc of the 14th Tools and Algorithms for the Constructionand Analysis of Systems,2008:337-340.
［11］	Barrett C W,Conway C L,Deters M,et al.CVC4［C］∥Proc of the 23rd International Conference on Computer Aided Verification (CAV’11),2011:171-177.
［12］	Niemetz A,Preiner M,Biere A.Boolector 2.0:System description［J］.Journal on Satisfiability,Boolean Modeling and Computation (JSAT),2015,9:53-58.
	附中文参考文献：
［5］	邓澍军,吴为民,边计年.RTL 验证中的混合可满足性求解［J］ .计算机辅助设计与图形学学报,2007,19(3):273-278.

[1]	刘永梅, 王国辉, 关永, 张景芝, 施智平, 董璐. 格林定理的形式化及其初步应用[J]. 计算机工程与科学, 2023, 45(07): 1178-1187.
[2]	白先平, 姚袭欣, 陈香兰, 刘翀, 李曦. 基于时间自动机的AADL端到端流规约验证方法[J]. 计算机工程与科学, 2023, 45(05): 810-819.
[3]	罗莉, 石伟, 何鸿君, 潘国腾, 王蕾, 龚锐. 一种面向IO Die的敏捷验证方法[J]. 计算机工程与科学, 2023, 45(04): 571-576.
[4]	汪铮, 黄容, 吴茂文, 孙寅涵, 孙志刚. OpenEmulator:一种面向TSN芯片验证的联合仿真平台[J]. 计算机工程与科学, 2023, 45(03): 411-419.
[5]	寇广岳, 魏国珩, 平源, 刘鹏. RFID安全认证协议综述[J]. 计算机工程与科学, 2023, 45(01): 77-84.
[6]	王雨露, 李飞, 杨震, 黄山, 张罡, 詹曙, . 基于深度前馈神经网络的多因子人体表面积计算模型[J]. 计算机工程与科学, 2023, 45(01): 119-126.
[7]	陈强, 谭林, 王云丽, 肖靖. 工业区块链中基于CUDA的数据并行处理方法[J]. 计算机工程与科学, 2022, 44(12): 2102-2110.
[8]	牛淑芬, 张美玲, 周思玮, 闫森. 面向移动终端的密文可验证属性基可搜索加密方案[J]. 计算机工程与科学, 2022, 44(11): 1941-1950.
[9]	李辉, 巨鹏锦, 计永兴. 多路系统Cache一致性验证中的错误追踪定位技术[J]. 计算机工程与科学, 2022, 44(07): 1171-1180.
[10]	陈小帆, 杨智杰, 彭凌辉, 王世英, 周干, 李石明, 康子扬, 王耀, 石伟, 王蕾. 一种类脑处理器片上网络的验证框架[J]. 计算机工程与科学, 2022, 44(05): 769-778.
[11]	阮鸥, 陈吉晨, 毛浩. 一种高效的SM2数字签名批量验证算法[J]. 计算机工程与科学, 2021, 43(07): 1236-1242.
[12]	郭辉, 黄立波, 郑重, 隋兵才, 王永文. Proto-Perf：快速精确的通用处理器原型系统性能评估方法[J]. 计算机工程与科学, 2021, 43(04): 579-585.
[13]	罗莉, 周宏伟, 周理, 潘国腾, 周海亮, 刘彬. 一种多核处理器直连接口QoS的设计与验证[J]. 计算机工程与科学, 2021, 43(04): 620-627.
[14]	何森, 迟万庆. 一种操作系统内存初始化优化算法[J]. 计算机工程与科学, 2020, 42(10高性能专刊): 1784-1790.
[15]	郑小宇, 刘冬梅, 杜益宁, 周子健, 邱玫媚, 朱鸿. 模式驱动的系统安全性设计的验证[J]. 计算机工程与科学, 2020, 42(07): 1197-1207.