韩俊刚,王岩冰,沈武威.用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. |
基金项目:本文研究得到国家自然科学基金资助. |
|
摘要点击次数: 3496 |
全文下载次数: 2981 |
中文摘要: |
本文考虑用时态逻辑语言XYZ/E描述硬件行为的可行性.作为实例,用XYZ/E语言描述了一个基于微处理器的容错计算机系统,这种描述可以在XYZ系统上执行,从而可对系统进行模拟.特别有意义的是利用XYZ/VERI验证子系统对所期望的性质进行了形式化证明.本文还将XYZ/E描述与相应的VHDL(VHSIChardwaredescriptionlanguage)描述进行了比较.从中可以看出时态逻辑语言的描述具有其独特的优点. |
英文摘要: |
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阅读器 |