未找到相关数据
用XYZ／E语言描述和验证硬件的行为
被引：5
作者：
韩俊刚
王岩冰
沈武威
机构：
[1] 西安邮电学院
[2] 山东师范大学
[3] 中国科学院软件研究所
来源：
关键词：
时态逻辑，硬件描述语言，形式化方法;
D O I：
10.13328/j.cnki.jos.1996.11.006
中图分类号：
TP312 [程序语言、算法语言];
学科分类号：
081202 ;
0835 ;
摘要：
本文考虑用时态逻辑语言ＸＹＺ／Ｅ描述硬件行为的可行性．作为实例，用ＸＹＺ／Ｅ语言描述了一个基于微处理器的容错计算机系统，这种描述可以在ＸＹＺ系统上执行，从而可对系统进行模拟．特别有意义的是利用ＸＹＺ／ＶＥＲＩ验证子系统对所期望的性质进行了形式化证明．本文还将ＸＹＺ／Ｅ描述与相应的ＶＨＤＬ（ＶＨＳＩＣｈａｒｄｗａｒｅｄｅｓｃｒｉｐｔｉｏｎｌａｎｇｕａｇｅ）描述进行了比较．从中可以看出时态逻辑语言的描述具有其独特的优点
引用
收藏
页码：37 / 43
页数：7
相关论文