Computer Science

Computer Science ›› 2023, Vol. 50 ›› Issue (11A): 230200112-6.doi: 10.11896/jsjkx.230200112

• Computer Software & Architecture • Previous Articles     Next Articles

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

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

CLC Number: 

  • 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.
[1] ZHENG Hong, QIAN Shihui, LIU Zerun, DU Wen. Formal Verification of Supply Chain Contract Based on Coloured Petri Nets [J]. Computer Science, 2023, 50(6A): 220300220-7.
[2] RAN Dan, CHEN Zhe, SUN Yi, YANG Zhi-bin. SCADE Model Checking Based on Program Transformation [J]. Computer Science, 2021, 48(12): 125-130.
[3] JI Cheng-yu,ZHU Xue-feng. Study on Optimization of Design Pattern Combination Operation [J]. Computer Science, 2020, 47(3): 19-24.
[4] CAI Yong, QIAN Jun-yan, PAN Hai-yu. Approximate Safety Properties in Metric Linear Temporal Logic [J]. Computer Science, 2020, 47(10): 309-314.
[5] XIA Nu-nu, YANG Jin-ji, ZHAO Gan-sen, MO Xiao-shan. Formal Verification of Cloud-aided Lightweight Certificateless Authentication Protocol Based on Probabilistic Model [J]. Computer Science, 2019, 46(8): 206-211.
[6] HAN Ying-jie, ZHOU Qing-lei, ZHU Wei-jun. Survey on DNA-computing Based Methods of Computation Tree Logic Model Checking [J]. Computer Science, 2019, 46(11): 25-31.
[7] ZHOU Nv-qi, ZHOU Yu. Multi-objective Verification of Web Service Composition Based on Probabilistic Model Checking [J]. Computer Science, 2018, 45(8): 288-294.
[8] LI Yun-chou,YIN Ping. Research of Model Checking Application on Aerospace TT&C Software [J]. Computer Science, 2018, 45(6A): 523-526.
[9] LEI Li-hui and WANG Jing. Parallelization of LTL Model Checking Based on Possibility Measure [J]. Computer Science, 2018, 45(4): 71-75.
[10] NIE Kai, ZHOU Qing-lei, ZHU Wei-jun and ZHANG Chao-yang. Modeling for Three Kinds of Network Attacks Based on Temporal Logic [J]. Computer Science, 2018, 45(2): 209-214.
[11] YANG Hong, HONG Mei, QU Yuan-yuan. Approach of Mutation Test Case Generation Based on Model Checking [J]. Computer Science, 2018, 45(11A): 488-493.
[12] ZHAO Ying, PAN Hua, ZHANG Yun-meng, MO Qi, DAI Fei. Modeling and Behavior Verification for Collaborative Business Processes [J]. Computer Science, 2018, 45(11A): 597-602.
[13] LIU Shuang, WEI Ou, GUO Zong-hao. Infinite-horizon Optimal Control of Genetic Regulatory Networks Based on Probabilistic Model Checking and Genetic Algorithm [J]. Computer Science, 2018, 45(10): 313-319.
[14] DU Yi, HE Yang and HONG Mei. Application of Probabilistic Model Checking in Dynamic Power Management [J]. Computer Science, 2018, 45(1): 261-266.
[15] GAO Wan-ling, HONG Mei, YANG Qiu-hui and ZHAO He. Efficiency Analysis of Different Statistical Algorithms on Statistical Model Checking [J]. Computer Science, 2017, 44(Z6): 499-503.
Viewed
Full text


Abstract

Cited
  Shared   
  Discussed   
No Suggested Reading articles found!
渝ICP备16013121号-4
Add:18# Honghu West Rd., Yubei ,Chongqing,China    Post Code: 401121
Tel: 023-63500828/023-67039612/023-67039623
E-mail: jsjkx12@163.com
Powered by Beijing Magtech Co., Ltd.