Visualization of Floating Point Invertibility Conditions

The following images visualize the invertibility of simple floating point equations. An invertibility condition is a quantifier-free formula that is equivalent to one with a single existentially quantified variable x. We visualize invertibility coniditions by displaying the truth value of this formula over the dimensions of its free variables, where floating point values are ordered. For example:

There are 227 values of floating point (3,5), i.e. 3 exponent bits and 5 significand bits. Thus, the invertibility condition is visualized as a 227x227 image, where white is true and black is false. Each pixel was computed via a satisfiability query of the form x+c_s=c_t for fixed constants c_s,c_t. For further details, see our CAV 2019 paper.

Images

Images for floating point equations for 3 bits exponent, 5 bits significand (227x227) can be found here:

Higher resolutions for four common floating point equations for 4 bits exponent, 9 bits significand (7683x7683) can be found here:

Example showing 5 bits exponent, 6 bits significand (1987x1987):

Floating Point (5,6) addition RNE (exists x. x+s=t).

Videos

The following is a visualization for fused-multiply-add. The invertibility condition has three free variables, and thus is visualized as a 227 frame video with resolution 227x227:

Floating Point (3,5) fused multiply add (exists x. fma(x,s,t)=r).

Note that we are unaware of a closed form solution for the above visualized formula. The following is a video showing the difference between a candidate solution for the above invertibility condition, where false positive points are given in red, false negative points given in blue:

Candidate invertibility condition for Floating Point (3,5) fused multiply add.