SHF: Small: Formal Verification of SQRT and Divider Circuits

点击翻译按钮获取中文摘要

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.