| 韩俊刚,王岩冰,沈武威.用XYZ／E语言描述和验证硬件的行为.软件学报,1996,7(11):676-682 |
| 用XYZ／E语言描述和验证硬件的行为 |
| DESCRIBING AND VERIFYING THE BEHAVIOR OF HARDWARE IN XYZ/E LANGUAGE |
| 修订日期：1995-09-26 |
| DOI： |
| 中文关键词: 时态逻辑 硬件描述语言 形式化方法 |
| 英文关键词:Temporal logic hardware description language formal design method. |
| 基金项目:本文研究得到国家自然科学基金资助. |
|
| 摘要点击次数: 3353 |
| 全文下载次数: 2892 |
| 中文摘要: |
| 本文考虑用时态逻辑语言ＸＹＺ／Ｅ描述硬件行为的可行性．作为实例，用ＸＹＺ／Ｅ语言描述了一个基于微处理器的容错计算机系统，这种描述可以在ＸＹＺ系统上执行，从而可对系统进行模拟．特别有意义的是利用ＸＹＺ／ＶＥＲＩ验证子系统对所期望的性质进行了形式化证明．本文还将ＸＹＺ／Ｅ描述与相应的ＶＨＤＬ（ＶＨＳＩＣｈａｒｄｗａｒｅｄｅｓｃｒｉｐｔｉｏｎｌａｎｇｕａｇｅ）描述进行了比较．从中可以看出时态逻辑语言的描述具有其独特的优点. |
| 英文摘要: |
| The necessities of VLSI design by formal method lead to consider the feasibility of specifying hardware behavior using temporal logic language XYZ/E which is the basis of the CASE tool system XYZ. A microprocessor based fault tolerant computer system is described behaviorally, simulated by executing the description on XYZ system, and the intended properties have been formally verified by using the XYZ/VERI. The comparison between XYZ/E and VHDL(VHSIC hardware description language) has been made. The results have shown that XYZ/E is promising for the research of formal method for hardware design. |
|
HTML 下载PDF全文 查看/发表评论 下载PDF阅读器 |
