SHF: Small: Formalisms, Implementations, and Verification Procedures for Alternatives to Floating Point

实数的高效准确表示是计算机科学中的一个基础性问题。浮点数被广泛用于使用有限位数来逼近实数。考虑到需要良好的性能和关于四舍五入误差或使用浮点表示的特殊条件的推理方面的挑战，社区有兴趣探索可能的替代方案。假设表示法是最近提出的IEEE-754浮点表示法的替代方案。这个项目开发了一些技术、工具和程序来确定POST是否是浮点数的可行替代方案。该项目的影响如下：(1)使程序员能够有效地使用命题编写正确的程序；(2)在生成高性能数学库和命题自动推理方面取得基础进展；(3)影响科学计算领域的专家并减轻他们对正确性和准确性的担忧；(4)教育研究生、本科生和高中生基础抽象和推理技术。在相同位数的情况下，命题表示可以表示比浮点表示更多的实数。根据配置的不同，它可以表示浮点所能表示的每个实值。定金社区正在试图找到定金在精度、性能或存储方面优于浮点的特定应用。这个项目开发技术、工具和过程来推断用POITS编写的应用程序的可行性、性能和准确性。对于性能，该项目开发了用于位置表示的高性能数学库，并探索了对位置运算的硬件支持。为了推断计算的准确性，研究人员开发了快速影子执行的技术，将假设执行与实数执行进行比较。为了能够使用POSITS对程序进行自动推理，该项目开发了一种可与可满足性模理论求解器一起使用的POSITS理论。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Efficient and accurate representation of real numbers is a foundational question in computer science. A floating-point number is widely used to approximate a real number using a finite number of bits. Given the need for good performance and challenges in reasoning about rounding errors or exceptional conditions with the floating-point representation, there is interest in the community to explore possible alternatives to it. The Posit representation is a recently proposed alternative to the IEEE-754 floating point representation. This project develops techniques, tools, and procedures to determine whether Posit is a viable alternative to floating point. This project's impacts are the following: (1) enable programmers to effectively write correct programs using Posits, (2) make foundational advances for generating high-performance math libraries and automated reasoning for Posits, (3) influence domain experts in scientific computing and alleviate their concerns about correctness and accuracy, and (4) educate graduate, undergraduate, and high-school students on foundational abstractions and reasoning techniques.The Posit representation can represent more real numbers than the floating-point representation given the same number of bits. Depending on the configuration, it can represent every real value that floating point can. The Posit community is attempting to find specific applications where a Posit outperforms floating point in accuracy, performance, or storage. This project develops techniques, tools, and procedures to reason about the feasibility, performance, and accuracy of applications written with Posits. Specifically for performance, the project develops high performance math libraries for the Posit representation and explores hardware support for Posit operations. To reason about the accuracy of computation, the investigators develop techniques for fast shadow execution that compares a Posit execution to an execution with real numbers. To enable automated reasoning for programs using Posits, the project develops a theory of Posits usable with satisfiability modulo theory solvers.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.