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

被引：4

作者：

郭建

杜惠敏

韩俊刚

郝克刚

机构：

[1] 西安邮电学院ASIC中心!陕西西安

[2] 西北工业大学计算机科学系!陕西西安

[3] 西北大学计算机科学系!陕西西安

来源：

小型微型计算机系统 | 2001年 / 05期

关键词：

时态逻辑; CTL; BDD; 模型检验; 符号模型检验;

D O I：

暂无

中图分类号：

TP302 [设计与性能分析];

学科分类号：

081201 ;

摘要：

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

引用

页码：521 / 524

页数：4

共 5 条

[1]

基于时态逻辑的形式化验证. 郭建. 西北大学 . 1999

[2]

形式验证综述〔C〕. 贝劲松. 第七届全国数字系统设计自动化学术会议论文集 . 1996

[3]

Computer_ aided Verification 〔J〕. E.M.Clarke,R.P.Kurshan. IEEE Spectrum . 1996

[4]

Graph based algorithms for BooleanfunctionManipulation. R.E.Bryant. IEEETransactionComputers . 1986

[5]

Symbolic Model Checking for Sequential Circuit Verification〔J〕. J.R.Burch,E.M.Clarke,D.E.long,K.L .Mc Millan,D.L .Dill. IEEE Transactions on Computers . 1994

← 1 →