基于时态逻辑的硬件设计形式化验证技术--模型检验1

• 作者: 杜惠敏 郝克刚 郭建 韩俊刚
• 来源期刊: 小型微型计算机系统
• 学科: 工学
• 关键词: 时态逻辑 CTL BDD 模型检验 符号模型检验
• 年，卷（期）: 2001,（5）
• 页码范围: 521-524
• 页数: 4页
• 分类号: TP301.1
• 字数: 4020字
• 语种: 中文
• DOI: 10.3969/j.issn.1000-1220.2001.05.003

摘要

通过对时态逻辑的研究来探讨时态逻辑在硬件设计形式化验证上的应用,同时对布尔函数在计算机内的表示二叉判定图(BDD)进行了进一步地分析,最后给出了一个时态逻辑对硬件设计进行验证的例子.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	韩俊刚	西安邮电学院ASIC中心	113	703	14.0	20.0
2	郝克刚	西北大学计算机科学系	122	1609	23.0	34.0
3	郭建	西安邮电学院ASIC中心	9	48	4.0	6.0
4	杜惠敏	西北工业大学计算机科学系	1	23	1.0	1.0