一种基于约束求解的Verilog语言静态分析方法

摘要

由于硬件描述语言Verilog中存在赋值语句的并发行为,对其验证一直是静态分析技术的一大挑战.针对Verilog程序的正确性问题,提出一种基于布尔约束求解的Verilog验证方法.通过分析Verilog语义特点,采用分步编码的方式对Verilog并发赋值语句进行处理.实验结果显示,该方法能有效地检测Verilog程序中设计的缺陷,并给出错误发生时程序的状态.