计算机科学

计算机科学 ›› 2023, Vol. 50 ›› Issue (11A): 230200112-6.doi: 10.11896/jsjkx.230200112

• 计算机软件&体系架构 • 上一篇    下一篇

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

杨柳1,2,3, 范洪宇1,2,3, 李东方4, 贺飞1,2,3   

  1. 1 清华大学软件学院 北京 100084
    2 教育部信息系统安全重点实验室 北京 100084
    3 北京国家信息科学与技术研究中心 北京 100084
    4 北京计算机技术及应用研究所 北京 100854
  • 发布日期:2023-11-09
  • 通讯作者: 贺飞(hefei@tsinghua.edu.cn)
  • 作者简介:(529244170@qq.com)
  • 基金资助:
    国家重点研发计划课题(2018YFB1308601);国家自然科学基金(62072267,62021002);国防基础科学科研计划(XX2020204B028)

IC3 Hardware Verification Algorithm Based on Variable Hiding Abstraction

YANG Liu1,2,3, FAN Hongyu1,2,3, LI Dongfang4, HE Fei1,2,3   

  1. 1 School of Software,Tsinghua University,Beijing 100084,China
    2 Key Laboratory for Information System Security,Ministry of Education,Beijing 100084,China
    3 Beijing National Research Center for Information Science and Technology,Beijing 100084,China
    4 Beijing Institute of Computer Technology and Applications,Beijing 100854,China
  • Published:2023-11-09
  • About author:YANG Liu,born in 1997,master.Her main research interests include predicate abstraction based on reinforcement learning and hardware model checking.
    HE Fei,born in 1980,Ph.D,associate professor,Ph.D supervisor.His main research interests include program verification,model checking,and automated reasoning.
  • Supported by:
    National Key Research and Development Program of China(2018YFB1308601),National Natural Science Foundation of China(62072267,62021002) and National Defense Basic Scientific Research Program of China(XX2020204B028).

PDF (PC)

187

摘要： 随着硬件设计复杂性和规模的大幅度提升,硬件验证工作更加具有挑战性。模型检验技术作为一种自动化验证技术,可以自动构建反例路径,也因此成为硬件验证领域内最重要的研究方向之一。IC3算法是近些年来最成功的比特级别的硬件验证算法。为了提高验证的规模和效率,硬件验证算法设计逐渐从底层的比特级向更高的抽象级别转变。研究目标是设计一个新型有效的字级IC3算法。针对研究目标,提出了一种将变量隐藏抽象和隐式抽象结合的字级IC3算法IC3VA。该方法尝试将变量隐藏抽象和IC3算法相结合,并设计了对应的泛化和精化方案。在开源社区和硬件验证大赛收集的测试集上和基于谓词抽象的方法进行对比,实验结果显示了基于变量隐藏抽象的IC3算法的有效性。

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

Abstract: 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.

Key words: Hardware verification, IC3 algorithm, Formal method, Model checking, Variable hiding abstraction

中图分类号: 

  • TP301.2
[1]CLARK E M.Model checking[C]//17th Foundations of Software Technology and Theoretical Computer Science.Springer Berlin Heidelberg,1997:54-56.
[2]CLARK EM,JOOST P K.Principles of model checking [M].MIT Press,2008.
[3]BRADLEY A R.SAT-based model checking without unrolling[C]//12th Verification,Model Checking,and Interpretation(VMCAI),2011:70-87.
[4]BRADLEY A R.Understanding ic3[C]//15th Theory and Application of Satisfiability Testing-SAT.2012:1-14.
[5]EEN N,MISHCHENKO A,BRAYTON R.Efficient implementation of property directed reachability[C]//2011 Formal Me-thods in Computer-Aided Design(FMCAD).IEEE,2011:125-134.
[6]CIMATTI A,GRIGGIO A,MOVER S,et al.IC3 Modulo Theories via Implicit Predicate ion[C]//International Conference on Tools and Algorithms for the Construction and Analysis of Systems(TACAS).2014:46-61.
[7]CLARKE E,GRUMBERG O,JHA S,et al.Counterexample-guided abstraction refinement [C]//Proceedings ofComputer Aided Verification:12th International Conference(CAV 2000).2000:154-169.
[8]GRAF S,SAIDI H.Construction of abstract state graphs with PVS[C]//CAV.1997:72-83.
[9]LONG D E.Model checking,abstraction,and compositional verification [M].Carnegie Mellon University,1993.
[10]KURSHAN R P.Computer-aided verification of coordinatingprocesses [M]// Computer-Aided Verification of Coordinating Processes.Princeton University Press,2014.
[11]HASSAN Z,BRADLEY A R,SOMENZI F.Better generalization in IC3[C]//2013 Formal Methods in Computer-Aided Design.IEEE,2013:157-164.
[12]GOEL A,SAKALLAH K.Empirical evaluation of ic3-basedmodel checking techniques on verilog rtl designs[C]//Design,Automation & Test in Europe Conference & Exhibition(DATE).IEEE,2019:618-621.
[13]JAIN H,KROENING D,SHARYGINA N,et al.VCEGAR:Verilog counterexample guided abstraction refinement[C]//Tools and Algorithms for the Construction and Analysis of Systems[C]//13th International Conference(TACAS 2007).2007:583-586.
[14]MUKHERJEE R,TAUTSCHNIG M,KRONENING D.v2c-Averilog to C translator[C]//22nd International Conference Tools and Algorithms for the Construction and Analysis of Systems(TACAS 2016).2016:580-586.
[15]IRFAN A,CIMATTI A,GRIGGIO A,et al.Verilog2SMV:A tool for word-level verification[C]//2016 Design,Automation &Test in Europe Conference & Exhibition(DATE).IEEE,2016:1156-1159.
[16]PREINER M,BIERE A,FROLEYKS N.Hardware model checking competition[EB/OL].https://fmv.jku.at.hwmcc20.
[17]YOSYS.Yosys open synthesis suite[EB/OL].https://www.yosyshq.com/about.
[18]WOLF C,GLASER J,KEPLER J.Yosys-a free Verilog synthesis suite[C]//Proceedings of the 21st Austrian Workshop on Microelectronics(Austrochip).2013:97.
[19]CIMATTI A,GRIGGIO A,TONETTA S.The VMT-LIB language and tools [J].arXiv:2109.12821,2021.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
地址：重庆市渝北区洪湖西路18号    邮编：401121  
电话：023-63500828（编辑部） 023-67039612（会议/专题） 023-67039623（财务/发票）
E-mail：jsjkx12@163.com
本系统由北京玛格泰克科技发展有限公司设计开发