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

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

Key words: software analysis and verification, hardware verification, synthesis semantics, program transformation