-
题名基于Mealy机精化关系的验证算法
- 1
-
-
作者
梁虹
金乃咏
-
机构
中国科学院软件研究所
新思科技有限公司验证组
-
出处
《计算机应用与软件》
CSCD
北大核心
2012年第8期169-172,共4页
-
文摘
与传统验证方法相比,形式验证技术因其完备性,已在数字电路设计领域中得到越来越多的关注。通过对形式验证技术和状态机的研究,在LTL公式的可实现策略基础上,提出一个基于Mealy机精化关系的验证算法,实现了一个搜索工具原型:支持算术表达式的LTL性质描述,在设计空间中搜索满足给定规范的输入输出信号。该技术可应用于定位电路设计中满足给定功能性质的代码片段。
-
关键词
形式验证
性质验证
精化
MEALY机
-
Keywords
Formal verification Property verification Refinement Mealy machine
-
分类号
TP301
[自动化与计算机技术—计算机系统结构]
-
-
题名一种基于约束求解的Verilog语言静态分析方法
被引量:1
- 2
-
-
作者
黄赛杰
陈铭松
金乃咏
-
机构
华东师范大学软件学院
新思科技有限公司验证组
-
出处
《计算机应用与软件》
CSCD
2015年第12期1-3,87,共4页
-
基金
国家自然科学基金青年项目(61202103)
上海市教育委员会科研创新项目(14ZZ047)
+1 种基金
高等学校博士学科点专项科研基金项目(20110076120025)
软硬件协同设计技术与应用教育部工程研究中心开放课题(2013001)
-
文摘
由于硬件描述语言Verilog中存在赋值语句的并发行为,对其验证一直是静态分析技术的一大挑战。针对Verilog程序的正确性问题,提出一种基于布尔约束求解的Verilog验证方法。通过分析Verilog语义特点,采用分步编码的方式对Verilog并发赋值语句进行处理。实验结果显示,该方法能有效地检测Verilog程序中设计的缺陷,并给出错误发生时程序的状态。
-
关键词
硬件设计
静态分析
模型检验
符号执行
约束求解
-
Keywords
Hardware design
Static analysis
Model checking
Symbolic execution
Constraint solving
-
分类号
TP3
[自动化与计算机技术—计算机科学与技术]
-