Verifying the SRT Division Algorithm Using Theorem Proving Techniques
Verifying the SRT Division Algorithm Using Theorem Proving Techniques
复制标题
使用定理证明技术验证 SRT 除法算法
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
Xudong Zhao
中科院分区：
文献类型：
--
作者：
E. Clarke;S. German;Xudong Zhao
我们验证与英特尔奔腾处理器中的SRT分裂电路的正确性。电路及其正确性条件被形式化为实数上的一组代数关系。应用定理证明技术进行硬件验证的主要障碍是需要详细的用户指导。在本示例中，我们使用称为Analytica的强大定理供体中克服了对详细的证明指导的需求。 Analytica使用符号代数技术来执行本文中的证据，而指导的指导远不如现有的通用定理牺牲者对代数推理所需的。
We verify the correctness of an SRT division circuit similar to the one in the Intel Pentium processor. The circuit and its correctness conditions are formalized as a set of algebraic relations on the real numbers. The main obstacle to applying theorem proving techniques for hardware verification is the need for detailed user guidance of proofs. We overcome the need for detailed proof guidance in this example by using a powerful theorem prover called Analytica. Analytica uses symbolic algebra techniques to carry out the proofs in this paper with much less guidance than existing general purpose theorem provers require for algebraic reasoning.