一种基于变量隐藏抽象的IC3硬件验证算法  

IC3 Hardware Verification Algorithm Based on Variable Hiding Abstraction

作　　者：杨柳 范洪宇[1,2,3] 李东方 贺飞 YANG Liu;FAN Hongyu;LI Dongfang;HE Fei(School of Software,Tsinghua University,Beijing 100084,China;Key Laboratory for Information System Security,Ministry of Education,Beijing 100084,China;Beijing National Research Center for Information Science and Technology,Beijing 100084,China;Beijing Institute of Computer Technology and Applications,Beijing 100854,China)

机构地区：[1]清华大学软件学院,北京100084 [2]教育部信息系统安全重点实验室,北京100084 [3]北京国家信息科学与技术研究中心,北京100084 [4]北京计算机技术及应用研究所,北京100854

出　　处：《计算机科学》2023年第S02期783-788,共6页Computer Science

基　　金：国家重点研发计划课题(2018YFB1308601);国家自然科学基金(62072267,62021002);国防基础科学科研计划(XX2020204B028)。

摘　　要：随着硬件设计复杂性和规模的大幅度提升,硬件验证工作更加具有挑战性。模型检验技术作为一种自动化验证技术,可以自动构建反例路径,也因此成为硬件验证领域内最重要的研究方向之一。IC3算法是近些年来最成功的比特级别的硬件验证算法。为了提高验证的规模和效率,硬件验证算法设计逐渐从底层的比特级向更高的抽象级别转变。研究目标是设计一个新型有效的字级IC3算法。针对研究目标,提出了一种将变量隐藏抽象和隐式抽象结合的字级IC3算法IC3VA。该方法尝试将变量隐藏抽象和IC3算法相结合,并设计了对应的泛化和精化方案。在开源社区和硬件验证大赛收集的测试集上和基于谓词抽象的方法进行对比,实验结果显示了基于变量隐藏抽象的IC3算法的有效性。As the complexity and scale of hardware designs have increased significantly,hardware verification has become more challenging.Model checking techniques,as an automated verification technique,can automatically construct counterexample paths and thus become one of the most important research directions in the field of hardware verification.The IC3 algorithm is the most successful hardware verification algorithm at the bit level in recent years.In order to improve the scale and efficiency of verification,the design of hardware verification algorithms is gradually shifting from the bottom bit level to a higher abstraction level.The research goal is to design a new effective word-level IC3 algorithm.Aimed at this research goal,a word-level IC3 algorithm that speaks of a combination of variable hidden abstraction and implicit abstraction,called IC3VA,is proposed.The approach attempts to combine variable hiding abstraction and IC3 algorithm,and designs a corresponding generalization and refinement scheme.It is compared with the predicate abstraction-based approach on a test set collected by the open-source community and a hardware verification competition.Experimental results show the effectiveness of the IC3 algorithm based on variable hiding abstraction.

关 键 词：硬件验证 IC3算法 形式化方法 模型检验 变量隐藏抽象 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]