HDLC IP核的形式化验证  

Formal Verification of HDLC IP Core

作　　者：李东方 刘诗宇 王志昊 王纪[1] 宋小敬 沈炜 LI Dong-fang;LIU Shi-yu;WANG Zhi-hao;WANG Ji;SONG Xiao-jing;SHEN Wei(Institute 706,Second Academy of CASIC,Beijing 100854,China)

机构地区：[1]中国航天科工集团第二研究院706所,北京100854

出　　处：《中国电子科学研究院学报》2022年第11期1078-1086,共9页Journal of China Academy of Electronics and Information Technology

基　　金：国防基础科研计划资助(XX2020204B028)。

摘　　要：目前,高级数据链路控制(High-Level Data Link Control, HDLC)协议控制器在航天型号中依然应用广泛,通常以IP核的形式被集成在通信部件中。但是近年,多个经过仿真验证的HDLC IP核在航天型号运行过程中出现了触发概率极小的功能错误,导致数据帧丢失、通信功能失效甚至任务失败。在仅依靠仿真无法保证验证充分性的背景下,采用形式化验证方法进行功能验证。本文依据HDLC国际标准分析同步传输模式关键功能,将关键功能拆分为属性描述,并根据属性编写断言,从而建立HDLC协议同步传输模式关键功能用例集,并以正在航天型号中使用的某HDLC IP核为例,使用形式化验证工具进行验证实验,发现了此前从未发现的两处设计缺陷。针对这些设计缺陷,分析了其触发原理和可能造成的危害。Currently,HDLC protocol controllers are still widely used in aerospace equipments,usually in the form of IP cores which are integrated in the communication component FPGAs.However,in recent years,several simulation-verified HDLC IP cores have shown corner functional errors during the operation of aerospace equipments,resulting in frame loss,communication or even mission failure.In the context that the adequacy of verification cannot be guaranteed by simulation method alone,this paper adopts a formal verification method for functional verification.This paper analyzes the key functions of synchronous transmission mode based on HDLC international standards,splits the key functions into property descrip-tions,and writes assertions based on the properties,so as to establish an assertion set of HDLC protocol.Taking an HDLC IP core being used in an aerospace equipment as an example,this paper conducts verifi-cation experiments using formal verification tools and finds two design flaws that have never been found before.For these design flaws,the paper analyzes the triggering paths and the possible problems may be caused.

关 键 词：功能验证 形式化验证 IP核 HDLC协议控制器 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]