The floating-point research community has developed many tools that
authors of numerical software can use to test, analyze, or improve their code.
They are listed here in alphabetical order and categorized into three general
types: 1) dynamic tools, 2) static
tools, 3) commercial tools, and 4)
miscellaneous. You can find tutorials for some of these
tools at fpanalysistools.org, and
many of the reduced-precision tools were compared in a
2020 survey by authors from
the Polytechnic University of Milan.
Miscellaneous
- CompCert
- CompCert is a compiler that has been formally verified to preserve
floating-point semantics using Coq.
-
- Fbench / Ffbench
- Fbench and Ffbench are two floating-point performance benchmarks by
John Walker (Fourmilab).
-
- FLiT: Floating-point Litmus Tests
- FLiT is a test infrastructure for detecting variability in floating-point
code due to differences in compilers and execution environments. It is currently
developed and maintained by Michael Bentley at the University of Utah.
-
- FPBench
- FPBench is a community benchmark project for floating-point examples.
-
- FPHPC Bechmark Suite
- This is a collection of programs containing floating-point arithmetic
with the immediate goal of aiding the development and evaluation of
floating-point precision and correctness analysis tools. The long-term goal
is to support and enable the scaling of such tools to provide insights for
high-performance computing (HPC) applications. This collection aims to
address the "middle ground" between real-valued expressions (such as those
contained in the FPBench collection) and full HPC applications.
-
- FPVM
- FPVM is a floating-point virtual machine proposed and prototyped by
Peter Dinda and others at Northwestern University. The goal is to allow an
existing application binary to be extended to support alternative
arithmetic systems. The current implementation combines static binary
analysis with trap-and-emulate execution.
-
- KLEE
- KLEE is a symbolic execution virtual machine built on LLVM with a
benchmark suite of example floating-point programs. There is also a
fork
that supports reasoning over floating-point constraints.
-
- Posit libraries
- Posits are the newest iteration on
John Gustafson's Unum representation
(see below). Unlike Unums, Posits have a fixed overall width but the number
of exponent and significand bits vary according to a run-length-encoded
"regime" field. It provides higher accuracy and a greater dynamic range than
identically-sized IEEE formats.
-
- S3FP
- Another project from the University of Utah (see FPTaylor and FPTuner
above), S3FP is a tool for finding floating-point inputs that will maximize
error.
-
- SOAP
- SOAP (Structural Optimisation of Arithmetic Programs) is a tool for
optimizing FPGA-based implementations of floating-point code.
-
- Sollya
- Sollya is a library and environment for safe floating-point
development, specifically intended to aid the development of math
library functions.
-
- Unum library
- Unums ("universal numbers") are a novel binary representation for real
numbers by John Gustafson that exactly
quantifies the uncertainty of a stored value. It extends IEEE floating-point by
making both the exponent and signficand fields variable-sized, and it adds an
"exact" bit that is set if the number is exact and unset if the number
represents a range between representable numbers. It provides a way to obtain
mathematically-rigorous results in numeric code at the cost of computational
efficiency.
-
- VFLOAT
- VFLOAT is a a variable-precision floating-point library for FPGAs, developed
and maintained by Miriam Leeser at Northeastern University.
-
This list is primarily maintained for the FPTalks research community by
Mike Lam.
If you are developing or are maintaining a floating-point tool, or know of a
tool that isn't on the list, please
email the list.