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. | VNU Journal of Science: Comp. Science & Com. Eng. Vol. 30, No. 3 (2014) 12–21 Symbolic Round-Off Error between Floating-Point and Fixed-Point Anh-Hoang Truong, Huy-Vu Tran, Bao-Ngoc Nguyen VNU University of Engineering and Technology, 144 Xuan Thuy, Cau Giay, Hanoi, Vietnam 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. c 2014 Published by VNU Journal of Science. Manuscript communication: received 13 September 2013, revised 25 March 2014, accepted 25 March 2014 Corresponding author: Anh Hoang Truong, hoangta@ Keywords: Round-Off Error, Symbolic Execution, Fixed-Point, Floating-Point 1. Introduction Software Failure [3]. Traditional round-off error [1] is the difference between the real result and the approximate result that a computer generates. As computers may or may not be equipped with floating-point units (FPU), they may use different numbers representations: floating-point or fixed-point, respectively. In addition, the two types of computers usually have different precisions in their mathematical operations. As a result, .
