计算机工程与科学

作者：邓茜, 范广生, 陈立前, 李暾, 王戟

单位：国防科技大学计算机学院，湖南 长沙 410073

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

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

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

来源：2023年第12期

《计算机工程与科学》期刊编辑部

查看计算机工程与科学杂志2023年第12期