VERIFICATION OF THE FUTUREBUS+ CACHE COHERENCE PROTOCOL

被引：42
|
作者：
CLARKE, EM
GRUMBERG, O
HIRAISHI, H
JHA, S
LONG, DE
MCMILLAN, KL
NESS, LA
机构：
[1] CARNEGIE MELLON UNIV,SCH COMP SCI,PITTSBURGH,PA 15213
[2] TECHNION ISRAEL INST TECHNOL,DEPT COMP SCI,IL-32000 HAIFA,ISRAEL
[3] KYOTO SANGYO UNIV,DEPT INFORMAT & COMMUN SCI,KYOTO 603,JAPAN
[4] BELLCORE,MORRISTOWN,NJ 07962
来源：
FORMAL METHODS IN SYSTEM DESIGN | 1995年 / 6卷 / 02期
基金：
美国国家科学基金会;
关键词：
THE COMPUTER INDUSTRY; STANDARDS; FUTUREBUS+; MULTIPLE DATA STREAM ARCHITECTURES; INTERCONNECTION ARCHITECTURES; NETWORK PROTOCOLS; PROTOCOL VERIFICATION;
D O I：
10.1007/BF01383968
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
We used a hardware description language to construct a formal model of the cache coherence protocol described in the IEEE Futurebus+ standard. By applying temporal logic model checking techniques, we found errors in the standard. The result of our project is a concise, comprehensible and unambiguous model of the protocol that should be useful both to the Futurebus+ Working Group members, who are responsible for the protocol, and to actual designers of Futurebus+ boards.
引用
收藏
页码：217 / 232
页数：16
相关论文
共 50 条
  • [1] VERIFICATION OF THE FUTUREBUS+ CACHE COHERENCE PROTOCOL
    CLARKE, EM
    GRUMBERG, O
    HIRAISHI, H
    JHA, S
    LONG, DE
    MCMILLAN, KL
    NESS, LA
    [J]. COMPUTER HARDWARE DESCRIPTION LANGUAGES AND THEIR APPLICATIONS, 1993, 32 : 15 - 30
  • [2] THE FUTUREBUS+ PROTOCOL STACK AND PROFILES
    BEASLEY, H
    [J]. IEEE MICRO, 1990, 10 (03) : 2 - &
  • [3] FUTUREBUS+
    GALLANT, JA
    [J]. EDN, 1990, 35 (20) : 87 - &
  • [4] IEEE FUTUREBUS CACHE COHERENCE PROTOCOL AS A LOGIC PROGRAM
    ROBINSON, P
    [J]. MICROPROCESSORS AND MICROSYSTEMS, 1990, 14 (08) : 491 - 496
  • [5] FUTUREBUS+
    ALLISON, A
    [J]. SYSTEMS INTEGRATION BUSINESS, 1990, 23 (01): : 11 - 11
  • [6] FUTUREBUS+ EXPECTATIONS
    ANDREWS, W
    [J]. COMPUTER DESIGN, 1989, 28 (20): : 16 - 16
  • [7] SINGLE-CHIP FUTUREBUS+ INTERFACE SPORTS CACHE COHERENCY
    ANDREWS, W
    [J]. COMPUTER DESIGN, 1993, 32 (12): : 117 - 118
  • [8] MORE ON FUTUREBUS+
    GREINER, RJ
    [J]. EDN, 1990, 35 (26) : 29 - 29
  • [9] WILL 1994 BE THE YEAR OF FUTUREBUS+
    ANDREWS, W
    [J]. COMPUTER DESIGN, 1993, 32 (09): : 49 - &
  • [10] THE FUTUREBUS+ TELECOMMUNICATIONS PROFILE
    WIDLICKA, RA
    [J]. COMPUTER DESIGN, 1993, 32 (09): : 54 - 54
12345