Symbolic round-off error between floating-point and fixed-point

Abstract

Overflow and round-off error has been a research problem for decades. With the explosion of mobile and embedded devices, many software programs written for personal computer are now ported to run on embedded systems. The porting often requires changing floating-point numbers and operations to fixed-point ones and here round-off error between the two versions of the program occurs. We propose a novel approach that uses symbolic computation to produce a precise representation of the round-off error for a program. From this representation, we can analyse various aspects of the error. For example we can use optimization tools like Mathematica to find a largest round-off error, or we can use SMT solvers to check if the error is always under a given bound. The models generated by these tools can be used to make optimal test cases that cause the worst round-off error. We will show several experimental results demonstrating the above applications of our symbolic round-off error.