Module fp_hypotheses 

Binary32 multiply and add under a family of semantics: the hypotheses a hard floating-point block is told apart by.

IEEE 754 fixes round-to-nearest-even and leaves an implementation the rest: whether a denormal operand is read as itself or as a zero, whether a result below the normals is kept as a denormal or flushed to zero, where tininess is decided (on the exact result, after rounding to the normals’ precision with the exponent unbounded, or, as the engine’s numerics do, after rounding at the denormals’ precision), the sign a flushed zero carries, and the NaN an operation returns. A Semantics names one choice of each; fmul_verilog and fadd_verilog print the combinational unit computing it, every member of family from one generator, so two members differ exactly where their semantics do, and Semantics::mul and Semantics::add compute it in software, bit for bit what its unit computes. Semantics::ENGINE is the engine’s own arithmetic (crate::spatial::decode_engine::numerics); Semantics::IEEE is IEEE 754 with gradual underflow and the payload-propagating NaNs of an x86 core. logicaffeine_proof::sweep::distinguish tells the family apart from the pairs of SPECIALS: the members that compute one function, proven, and operand pairs on which every two that differ give different results, the vectors a hard block is measured on to say which member it is.

Structs

Semantics

One choice of everything IEEE 754 leaves to an implementation of binary32 multiply and add.

Enums

Denormals

How a denormal is read or written.

FlushSign

The sign of a result flushed to zero.

Nan

The NaN an operation returns.

Tininess

Where a result below the least normal is decided to be one.

Constants

NANS

The NaN encodings the family tries: four canonical NaNs, the first NaN operand’s payload with either default NaN for an invalid operation (an ARM core’s positive one, an x86 core’s negative one), and the default quiet NaN signed by the operands’ signs’ exclusive or (the D5005’s floating-point DSP block’s multiply).

SPECIALS

The operands every pair of which a hard block is first measured on: signed zeros, the denormals’ ends, the normals’ ends, one, infinities, quiet and signalling NaNs, a mid denormal and one above one.

Functions

fadd_verilog

A combinational binary32 add under s, ports a, b, y.

family

Every member: each choice of operand denormals, result denormals, tininess, flushed sign and NaN, the meaningless combinations folded away; Semantics::ENGINE first.

fmul_verilog

A combinational binary32 multiply under s, ports a, b, y.