计算机工程与科学2023，Vol.45Issue(12)：2146-2154,9.DOI:10.3969/j.issn.1007-130X.2023.12.006
基于C语言程序分析验证技术的Verilog代码验证方法
A Verilog code verification method based on C program analysis and verification techniques
摘要
Abstract
Traditional hardware verification methods synthesize RTL designs into gate-level netlists and use SAT solvers for verification,without effectively leveraging their word-level structure,resulting in the inability to verify some properties.In recent years,software analysis and verification techniques and SMT solving technology have made significant progress.To migrate the latest software analysis and verification techniques to hardware verification,a Verilog code verification method based on C program analysis and verification technology is proposed.First,a Verilog-to-C translation system based on inte-grated semantics is designed,and then typical techniques and tools in the current software analysis and verification field are used to analyze and verify the converted C program,in order to determine whether the original Verilog code satisfies the property assertion.Experimental results demonstrate the feasibili-ty and effectiveness of migrating C program analysis and verification techniques to Verilog code verifica-tion.关键词
软件分析与验证/硬件验证/综合语义/程序转换Key words
software analysis and verification/hardware verification/synthesis semantics/program transformation分类
信息技术与安全科学引用本文复制引用
邓茜,范广生,陈立前,李暾,王戟..基于C语言程序分析验证技术的Verilog代码验证方法[J].计算机工程与科学,2023,45(12):2146-2154,9.基金项目
国家重点研发计划(2022YFA1005101) （2022YFA1005101）
国家自然科学基金(62032024) （62032024）
