Formal Verification of IA-64 Division Algorithms
Formal Verification of IA-64 Division Algorithms
复制标题
IA-64 除法算法的形式验证
DOI：
10.1007/3-540-44659-1_15
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
J. Harrison
中科院分区：
文献类型：
--
作者：
J. Harrison
IA-64体系结构将浮点和整数部门变成软件。为了确保正确性和最大效率，英特尔提供了许多推荐的算法，这些算法可以称为子例程或由编译器和汇编语言程序员夹住。所有这些算法均已使用HOL Light Theorem示意剂进行正式验证。除了提高我们对算法的信心水平外，正式的验证过程还使人们对基本理论有了更好的了解，从而可以提高一些显着的效率。
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.