Formal verification of IA-64 division algorithms

被引：0
|
作者：
Harrison, J [1 ]
机构：
[1] Intel Corp, Hillsboro, OR 97124 USA
来源：
THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS | 2000年 / 1869卷
关键词：
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
The IA-64 architecture defers floating point and integer division to software. To ensure correctness and maximum efficiency, Intel provides a number of recommended algorithms which can be called as subroutines or inlined by compilers and assembly language programmers. All these algorithms have been subjected to formal verification using the HOL Light theorem prover. As well as improving our level of confidence in the algorithms, the formal verification process has led to a better understanding of the underlying theory, allowing some significant efficiency improvements.
引用
收藏
页码：233 / 251
页数：19
相关论文
共 50 条
  • [21] C++ exception handling for IA-64
    de Dinechin, C
    USENIX ASSOCIATION PROCEEDINGS OF THE FIRST WORKSHOP ON INDUSTRIAL EXPERIENCES WITH SYSTEMS SOFTWARE (WIESS 2000), 2000, : 67 - 75
  • [22] IA-64的霸主之路漫漫
    林润华
    微电脑世界, 1999, (40) : 7 - 7
  • [23] Cycles to recycle: Garbage collection on the IA-64
    Hudson, RL
    Moss, JEB
    Subramoney, S
    Washburn, W
    ACM SIGPLAN NOTICES, 2001, 36 (01) : 101 - 110
  • [24] ILP-based instruction scheduling for IA-64
    Kästner, D
    Winkel, S
    ACM SIGPLAN NOTICES, 2001, 36 (08) : 145 - 154
  • [25] Verified optimizations for the Intel* IA-64 architecture
    Grundy, J
    THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2000, 1869 : 215 - 232
  • [26] The Intel IA-64 compiler code generator
    Bharadwaj, J
    Chen, WY
    Chuang, W
    Hoflehner, G
    Menezes, K
    Muthukumar, K
    Pierce, J
    IEEE MICRO, 2000, 20 (05) : 44 - 53
  • [27] SVR5计划支持IA-64
    每周电脑报, 1997, (42) : 27 - 27
  • [28] OS and compiler considerations in the design of the IA-64 architecture
    Zahir, R
    Ross, J
    Morris, D
    Hess, D
    ACM SIGPLAN NOTICES, 2000, 35 (11) : 212 - 221
  • [29] Clock generation and distribution for the first IA-64 microprocessor
    Tam, S
    Rusu, S
    Desai, UN
    Kim, R
    Zhang, J
    Young, I
    IEEE JOURNAL OF SOLID-STATE CIRCUITS, 2000, 35 (11) : 1545 - 1552
  • [30] 走向IA-64——记惠普第一个面向IA-64的N系列机诞生
    黄盛萍
    微电脑世界, 1999, (16) : 43 - 45
12345