摘要
由于硬件描述语言Verilog中存在赋值语句的并发行为,对其验证一直是静态分析技术的一大挑战。针对Verilog程序的正确性问题,提出一种基于布尔约束求解的Verilog验证方法。通过分析Verilog语义特点,采用分步编码的方式对Verilog并发赋值语句进行处理。实验结果显示,该方法能有效地检测Verilog程序中设计的缺陷,并给出错误发生时程序的状态。
The verification of hardware description language（ HDL） Verilog has always been a big challenge of static analysis technology duo to the concurrent behaviour of assignment statements existed in it. In light of the issue of Verilog program correctness,we proposed a Boolean constraint solving-based Verilog verification approach. By analysing the semantic features of Verilog,we adopted the way of step-bystep coding to process the concurrent assignment statements of Verilog. Experimental result demonstrated that this approach was able to effectively detect the design bugs in Verilog program,and showed the program status when error occurred.
出处
《计算机应用与软件》
CSCD
2015年第12期1-3,87,共4页
Computer Applications and Software
基金
国家自然科学基金青年项目(61202103)
上海市教育委员会科研创新项目(14ZZ047)
高等学校博士学科点专项科研基金项目(20110076120025)
软硬件协同设计技术与应用教育部工程研究中心开放课题(2013001)
关键词
硬件设计
静态分析
模型检验
符号执行
约束求解
Hardware design
Static analysis
Model checking
Symbolic execution
Constraint solving
