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

• 作者: 金乃咏 陈铭松 黄赛杰
• 来源期刊: 计算机应用与软件
• 学科: 工学
• 关键词: 硬件设计 静态分析 模型检验 符号执行 约束求解
• 年，卷（期）: 2015,（12）
• 所属期刊栏目: 软件技术与研究
• 页码范围: 1-3,87
• 页数: 4页
• 分类号: TP3
• 字数: 3800字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-386x.2015.12.001

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈铭松	华东师范大学软件学院	4	1	1.0	1.0
2	黄赛杰	华东师范大学软件学院	1	1	1.0	1.0