FPBench 2.0 defines the meaning of the following properties:

:name

A string name for the benchmark. If a name is needed and not provided, we recommend using the body expression.

:description

A string description for the benchmark and its inputs. We recommend describing the physical meaning and units of inputs when applicable.

:cite

A list of symbols that describe the sources of the benchmark. We recommend making available a BibTeX file which uses the same symbols as keys.

:precision

Describes the floating-point precision used for rounding, using a list naming a precision family and its parameters, or using a short-hand symbol synonymous with such a list.

(float e nbits)

An IEEE-754 binary floating-point value with e exponent bits and nbits total bits. binary32 and binary64 are common shorthands, for (float 8 32) and (float 11 64) respectively.

(posit es nbits)

Posits with es exponent bits and nbits total bits. Common shorthands include posit8 for (posit 0 8), posit16 for (posit 1 16), posit32 for (posit 2 32), and posit64 for (posit 3 64).

(fixed scale nbits)

Fixed point, with nbits total bits and a scale factor of 2 ^ scale. One bit will store the sign, using two's complement. For example, (fixed 0 8) can represent the 8-bit integers from -128 to 127, while (fixed -8 8) can represent magnitudes from -128/128 to 127/128 in steps of 1/128. Overflow behavior is determined by the overflow property.

real

A special precision for arbitrary real numbers, where no rounding takes place.

integer

A special precision for mathematical integers, where no rounding takes place. Implementations should assume that all values with this precision are indeed integers: if a non-integer value is computed, implementations can signal an error.

Where no :precision property is specified, implementations should assume a sane default, such as binary64 or possibly real depending on the application domain.

:round

The floating-point rounding mode used for rounding. Expected to be one of the IEEE 754 modes nearestEven, nearestAway, toPositive, toNegative, or toZero.

:overflow

The rounding behavior to use when a fixed-point value overflows. Possible values include:

infinity

Produce a floating-point-like infinity on overflow.

clamp

Clamp the value to the largest representable magnitude.

wrap

Wrap the significand using two's complement arithmetic.

:pre

A precondition on inputs to the benchmark. Tools should not use points that fail the precondition to determine the accuracy of the benchmark. It is expected to be an expression that returns a boolean value. A rounding context can be given explicitly for the expression, but if it is not, the default rounding context is assumed to have real precision rather than the overall properties specified for the FPCore.

:spec

A real-valued function approximated by the benchmark. If not provided, then it is assumed to be the body of the benchmark. As with preconditions specified with :pre, a rounding context can be provided explicitly, but it is assumed to have real precision rather than the overall properties specified for the FPCore.

:alt

An alternative formulation of the same benchmark. These alternative formulations could be more accurate or less accurate, or optimized for different hardware, or be the output of an automated tool like a compiler or a synthesizer. To describe the precise manner in which something is an alternative, the :description annotation can be used, but this is not required. A single FPCore expression could have multiple :alt values to represent multiple alternative formulations. Unlike :spec, which is usually assumed to have real precision and thus be unrealizable, :alt is assumed to have the same precision as the overall FPCore and be realizable, though different in some way from the main body expression.

:math-library

The library used in the source to implement floating-point operations. It is expected to be a symbol identifying a library implementation and version, such as gnu-libm-2.34.

Additionally, properties prefixed by the name of a tool (such as :xxx-foobar) are reserved for definition by that tool. Only that tool may define the meaning of those properties; other tools should not depend on the meaning of those properties, nor must the defining tool keep the meaning constant.