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 条
  • [31] Design of a virtual interface architecture based on IA-64
    Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China
    Qinghua Daxue Xuebao, 2006, 4 (576-579):
  • [32] Parallel checkpoint/recovery on cluster of IA-64 computers
    Zhang, YH
    Wang, DS
    Zheng, WM
    PARALLEL AND DISTRIBUTED PROCESSING AND APPLICATIONS, PROCEEDINGS, 2004, 3358 : 212 - 216
  • [33] IA-64 architecture parameter passing conventions overview
    Qi Ning
    Zhao Rongcai
    Pang Hanmin
    Dong Zehui
    ICCSE'2006: Proceedings of the First International Conference on Computer Science & Education: ADVANCED COMPUTER TECHNOLOGY, NEW EDUCATION, 2006, : 97 - 100
  • [34] Overview of IA-64 explicitly parallel instruction computing architecture
    Gepner, P
    PARALLEL PROCESSING APPLIED MATHEMATICS, 2002, 2328 : 331 - 339
  • [35] M-P ports Java']Java to IA-64
    不详
    CONTROL AND INSTRUMENTATION, 1998, 30 (05): : 27 - 27
  • [36] PA-RISC to IA-64 transparent execution, no recompilation
    Zheng, C
    Thompson, C
    COMPUTER, 2000, 33 (03) : 47 - +
  • [37] Thckpt: Transparent checkpointing of Linux processes under IA-64
    Xue, RN
    Zhang, YH
    Chen, WG
    Zheng, WM
    PDPTA '05: Proceedings of the 2005 International Conference on Parallel and Distributed Processing Techniques and Applications, Vols 1-3, 2005, : 325 - 331
  • [38] Predicate removing technique in machine emulation for IA-64 aechitecture
    Su, Ming
    Zhao, Rong-Cai
    Song, Zong-Yu
    7TH INTERNATIONAL CONFERENCE ON COMPUTER-AIDED INDUSTRIAL DESIGN & CONCEPTUAL DESIGN, 2006, : 210 - +
  • [39] 惠普英特尔联手IA-64计划
    互联网周刊, 2000, (29) : 5 - 5
  • [40] Eliminating exception constraints of Java']Java programs for IA-64
    Ishizaki, K
    Inagaki, T
    Komatsu, H
    Nakatani, T
    2002 INTERNATIONAL CONFERENCE ON PARALLEL ARCHITECTURES AND COMPILATION TECHNIQUES, PROCEEDINGS, 2002, : 259 - 268
12345