SHF: Small: Formal Verification of SQRT and Divider Circuits

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

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.