高性能CPU研发能够离开定理证明器吗

发信人: lingcore (), 信区: CSArch
标  题: 高性能CPU研发能够离开定理证明器吗
发信站: 水木社区 (Tue Feb  1 07:28:39 2011), 站内

2003年，我曾写过一篇关于定理证明器在CPU验证中的应用情况的综述。在那个时候，人们对定理证明大都抱有怀疑的眼光。8年过后，情况发生了巨大变化。我也没有想到，关于这方面的研究进展，会放到程序语言大会POPL上来报告。

今年POPL的给人印象最深的不是语言研究的进展，而是定理证明的实用化。

第一个特邀报告是关于一个C编译器的正确性证明，这个编译器在一组程序例子上的性能可以同GCC –O3性能相比美。POPL中另的一篇文章是关于微软和MIT进行的关于操作系统正确性的定理证明。在两个卫星会议的特邀报告则是INTEL和AMD这两个公司中定理证明器的使用情况。

定理证明器的开发从1980年左右开始，至今已有30多年。最早的一批定理证明器都进行了硬件验证工作。但是，定理证明真正受到工业界的重视则应归功于INTEL公司的一个价值几百亿美元的芯片设计错误。

1998年，一个教授发现了INTEL芯片浮点运算中的一个错误。这一发现迫使INTEL收回一大批芯片，导致该公司几百亿美元的损失。自此之后，INTEL建立了形式验证组，开始了形式验证的实验性工作；2000年，形式验证组同设计组结合在一起；2006年，在算术部件的开发中，形式验证取代了传统的模拟测试！

这里所谈的形式验证不是使用商用软件（比如FORMALITY）进行的电路等价性验证，那些验证工具所处理的问题相对而言比较简单。INTEL公司所作的是复杂大电路的高层验证。这些验证不是EDA公司出售的商用软件能够解决的。

INTEL采用的是把基于符号模拟的模型检查同交互式定理证明相结合的技术。模型检查是一种自动化的证明方法，但是它自身尚不足以用于证明复杂的性质。为了解决这个问题，INTEL开发了一种专用的函数式语言reFLect，用它来描述证明策略，实现复杂的证明任务。目前，reFLect语言在证明过程中发挥了多种作用：

1.    算法的高级描述；
2.    证明策略的描述和实现；
3.    电路的模拟执行；
4.    用内嵌的符号模拟程序进行自动证明；

INTEL公司的定理证明器和reFLect语言细节目前尚未公开。

当INTEL浮点电路错误事件发生之后，AMD公司找到了奥斯汀大学的J. MOORE教授。

Moore教授长期进行定理证明研究，他同Boyer共同开发的定理证明器是最早的定理证明器之一。该证明器最初称为Boyer-Moore证明器，现在的名称是ACL2。在AMD公司找他们之前，该证明器已经被用于证明许多著名的数学定理。而且也被用于软件和硬件验证，包括算术电路证明，微处理器正确性的证明，汇编器，小型编译器，小型操作系统的证明。

这次AMD公司来找MOORE教授为的是浮点运算器的问题。AMD为了节省芯片面积，把一部分浮点操作用软件实现。但是，由于时间紧迫，AMD没有太多的时间对这一变动进行大量的测试，INTEL事件更给了AMD很大的震动。所以AMD找MOORE教授寻求帮助。后者不负所望，用定理证明验证了新版浮点运算实现的正确性。从此以后，AMD公司也把定理证明融入了设计流程。证明人员和设计人员在一起合作工作。

结论 计算机科学正在进入一个定理证明器时代。用定理证明器证明系统软件和硬件的正确性不仅可行，而且将成为必须。做一个高性能CPU虽然困难，但更难的是做一个可靠的CPU，而且还要在短时间完成，在商业竞争中生存下去。这就是INTEL和AMD采用定理证明技术的原因。然而，定理证明是一个需要长期积累的技术。在INTEL和AMD中从事这项工作的人进行了20-30年的开发，大量细节并不公开。