Symbolic Round-Off Error between Floating-Point and Fixed-Point

Abstract

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