SHF: Small: Formal Verification of SQRT and Divider Circuits

该项目的目标是开发有效的技术来验证集成电路，实现复杂的算术运算，如除法和平方根函数。这些函数在许多工程和科学应用中起着重要作用，例如计算机算术，密码学，人工智能和其他特殊用途的计算。它们是要实现和验证的最复杂的算术运算中的一些，并且证明这样的电路正确地实现期望的算术运算是最重要的。传统的基于仿真的验证方法已经不能满足由数千万个晶体管组成的电路的复杂性。 对于这种设计，最有前途的方法是形式验证，其中通过数学推理全局地证明电路的属性。虽然有一个主机的正式方法，可以验证除法算法和所得到的架构的正确性，有必要验证这种电路的实际硬件实现。 这个项目开发了有效的验证技术，结合了联合收割机的符号计算机代数和逻辑综合的进步。 该项目的成功实施将有助于开发用于硬件分析和验证的最先进的电子设计自动化（EDA）工具。它将有助于提高设计生产力，并将进一步促进学术界和工业界之间的合作。该项目将通过教育学生和强调正式方法在工程实践中的重要性，产生重要的教育影响。它也将教育工程师如何模拟复杂的问题，并将形式验证技术应用于大规模系统设计。该项目解决了门级分频器和平方根电路的验证，设计用于整数和分数运算。分数除法器特别令人感兴趣，因为它们是大多数科学计算中使用的浮点除法的重要组成部分。该项目提出的验证方法是研究人员早期开发的代数重写模型的扩展，并已成功应用于整数和伽罗瓦域乘法器。这种新颖的方法被称为硬件重写：电路被附加了一个硬件组件，实现所需函数的逆，并与电路，模拟额外的算术约束，必须由电路满足。然后使用标准合成工具对这样构造的电路进行逻辑合成。如果原始电路正确地实现了所需的算术功能，则合成的硬件会减少到冗余状态。当合成工具不能将电路简化到这种状态时，可以使用标准的布尔可满足性（SAT）技术来证明或反驳冗余。该方法可以扩展到具有已知功能规范的其他算术函数。该奖项反映了NSF的法定使命，并且通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The goal of the project is to develop efficient techniques to verify integrated circuits that implement complex arithmetic operations, such as division and square root functions. These functions play a major role in many engineering and scientific applications, such as computer arithmetic, cryptography, artificial intelligence, and other special-purpose computations. They are some of the most complex arithmetic operations to implement and to verify, and proving that such circuits correctly implement the desired arithmetic operations is of prime importance. Traditional verification methods based on simulation cannot keep up with the complexity of those circuits that are composed of tens of millions of transistors. The most promising approach advocated for such designs is formal verification, where properties of the circuit are proved globally by mathematical reasoning. While there is a host of formal methods that can verify correctness of the division algorithms and the resulting architectures, there is a need to verify actual hardware implementation of such circuits. This project develops efficient verification techniques that combine advances of symbolic computer algebra and logic synthesis. Successful implementation of the project will contribute to the development of the state-of-the-art electronic design automation (EDA) tools for hardware analysis and verification. It will help increase design productivity and will further the collaboration between academia and industry. The project will have an important educational impact by educating students and emphasizing the importance of formal methods in engineering practice. It will also educate engineers how to model complex problems and apply formal-verification techniques to large-scale system design.The project addresses the verification of gate-level dividers and square-root circuits, designed to operate in both integer and fractional arithmetic. The fractional dividers are of particular interest since they are essential components of the floating point division used in most scientific computations. The verification approach proposed for this project is an extension of the algebraic-rewriting model developed earlier by the investigator and already successfully applied to integer and Galois-Field multipliers. This novel method is termed hardware rewriting: the circuit is appended with a hardware component that implements the inverse of the desired function and with the circuit that emulates additional arithmetic constraints that must be satisfied by the circuit. Such a constructed circuit is then subjected to logic synthesis using standard synthesis tools. If the original circuit correctly implements the required arithmetic function, the synthesized hardware reduces to a redundant state. When the synthesis tool is not able to reduce the circuit to such a state, the redundancy can be proved or disproved using standard Boolean satisfiability (SAT) techniques. The method can be extended to other arithmetic functions with known functional specifications.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.