基于C语言程序分析验证技术的Verilog代码验证方法  

A Verilog code verification method based on C program analysis and verification techniques

作　　者：邓茜 范广生 陈立前[1] 李暾[1] 王戟[1] DENG Xi;FAN Guang-sheng;CHEN Li-qian;LI Tun;WANG Ji(College of Computer Science and Technology,National University of Defense Technology,Changsha 410073,China)

机构地区：[1]国防科技大学计算机学院,湖南长沙410073

出　　处：《计算机工程与科学》2023年第12期2146-2154,共9页Computer Engineering & Science

基　　金：国家重点研发计划(2022YFA1005101);国家自然科学基金(62032024)。

摘　　要：传统的硬件验证方法将RTL设计综合成门级网表并使用SAT求解器进行验证,没有有效利用其字级结构,导致部分性质不能验证。近年来,软件分析验证技术和SMT求解技术取得了长足的发展,为将最新的软件分析验证技术迁移到硬件验证上来,提出一种基于C语言程序分析验证技术的Verilog代码验证方法。首先设计一个基于综合语义的Verilog到C的转换系统;然后使用当前软件分析验证领域典型的技术与工具对转换后的C语言程序进行分析验证,以判定原Verilog代码是否满足性质断言。实验结果表明了将C语言程序分析验证技术迁移到Verilog代码验证上的可行性和有效性。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 integrated 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 feasibility and effectiveness of migrating C program analysis and verification techniques to Verilog code verification.

关 键 词：软件分析与验证 硬件验证 综合语义 程序转换 

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