SHF: Small: Formal Verification of SQRT and Divider Circuits

SHF：小：SQRT 和分压器电路的形式验证

• 批准号: 2006465
• 负责人: Maciej Ciesielski
• 金额: $ 40万
• 依托单位: University of Massachusetts Amherst
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-10-01 至 2024-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2006465&HistoricalAwards=false
• 关键词: SHF; Small; Formal; Verification; SQRT

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.

该项目的目的是开发有效的技术来验证实施复杂算术操作的集成电路，例如除法和平方根函数。这些功能在许多工程和科学应用中起着重要作用，例如计算机算术，密码学，人工智能和其他特殊用途计算。它们是要实施和验证的最复杂的算术操作，并且证明此类电路正确实施所需的算术操作至关重要。基于模拟的传统验证方法无法跟上由数千万晶体管组成的电路的复杂性。 此类设计提倡的最有前途的方法是正式验证，在该验证中，通过数学推理在全球范围内证明了电路的特性。尽管有许多正式方法可以验证分区算法的正确性和生成的体系结构，但需要验证此类电路的实际硬件实现。 该项目开发了有效的验证技术，结合了符号计算机代数和逻辑合成的进步。 该项目的成功实施将有助于开发用于硬件分析和验证的最先进的电子设计自动化（EDA）工具。它将有助于提高设计生产力，并进一步促进学术界与行业之间的合作。该项目将通过教育学生并强调形式方法在工程实践中的重要性，从而产生重要的教育影响。它还将教育工程师如何建模复杂问题并将正式验证技术应用于大规模系统设计。该项目涉及旨在在整数和分数算术中运行的门级隔板和方形循环的验证。分数分隔线特别令人感兴趣，因为它们是大多数科学计算中使用的浮点分裂的重要组成部分。该项目提出的验证方法是研究人员早期开发的代数练习模型的扩展，并且已经成功地应用于整数和Galois-field乘数。这种新颖的方法称为硬件重写：该电路附加了硬件组件，该硬件组件实现了所需函数的倒数以及模拟电路必须满足的其他算术约束的电路。然后，使用标准合成工具对这种构造的电路进行逻辑合成。如果原始电路正确实现了所需的算术函数，则合成的硬件将减少到冗余状态。当综合工具无法将电路降低到这样的状态时，可以使用标准布尔可满足（SAT）技术证明或反驳冗余。该方法可以扩展到具有已知功能规格的其他算术功能。该奖项反映了NSF的法定任务，并且使用基金会的知识分子优点和更广泛的影响审查标准，被认为值得通过评估来获得支持。

项目成果

Formal Methods in Arithmetic Circuit Verification: a Brief History and Challenges

算术电路验证中的形式化方法：简史和挑战

• 发表时间: 2023
• 期刊: Digital system design series
• 作者: Ciesielski, Maciej

Efficient Formal Verification and Debugging of Arithmetic Divider Circuits

算术除法器电路的高效形式验证和调试

• 发表时间: 2023
• 期刊: ICCAD IEEEACM International Conference on ComputerAided Design
• 作者: Dasari, Jiteshri;Ciesielski, Maciej
• 通讯作者: Ciesielski, Maciej

Functional Verification of Arithmetic Circuits: Survey of Formal Methods

算术电路的功能验证：形式方法综述

• DOI: 10.1109/ddecs54261.2022.9770161
• 发表时间: 2022
• 期刊: 25th International Symposium on Design and Diagnostics of Electronic Circuits and Systems
• 作者: Ciesielski, Maciej;Yasin, Atif;Dasari, Jiteshri
• 通讯作者: Dasari, Jiteshri

Formal Verification of Restoring Dividers made Fast and Simple

恢复分频器的形式验证变得快速而简单

• 发表时间: 2023
• 期刊: Proceedings Design Automation Conference
• 作者: Dasari, Jiteshri;and Ciesielski, Maciej
• 通讯作者: and Ciesielski, Maciej

Formal Verification of Divider Circuits by Hardware Reduction

通过硬件简化对分压器电路进行形式验证

• DOI: 10.1109/smacd58065.2023.10192137
• 发表时间: 2023
• 期刊: Analysis and Simulation Methods and Applications to Circuit Design (SMACD-2023
• 作者: Yasin, Atif;Su, Tiankai;Pillement, Sebastien;Ciesielski, Maciej
• 通讯作者: Ciesielski, Maciej