Synthesis of Optimal Fixed-Point Implementations of Numerical Software Routines

Susmit Jha and Sanjit A. Seshia. Synthesis of Optimal Fixed-Point Implementations of Numerical Software Routines. In Proc. Sixth International Workshop on Numerical Software Verification (NSV), April 2013.

Download

[pdf] 

Abstract

In this paper, we present an automated technique SWATI: Synthesizing Wordlengths Automatically Using Testing and Induction, which uses a combination of Nelder-Mead optimization based testing, and induction from examples to automatically synthesize optimal fixedpoint implementation of numerical routines. The design of numerical software is commonly done using floating-point arithmetic in design-environments such as Matlab. However, these designs are often implemented using fixed-point arithmetic for speed and efficiency reasons especially in embedded systems. The fixed-point implementation reduces implementation cost, provides better performance, and reduces power consumption. The conversion from floating-point designs to fixed-point code is subject to two opposing constraints: (i) the word-width of fixed-point types must be minimized, and (ii) the outputs of the fixed-point program must be accurate. In this paper, we propose a new solution to this problem. Our technique takes the floating-point program, specified accuracy and an implementation cost model and provides the fixed-point program with specified accuracy and optimal implementation cost. We demonstrate the effectiveness of our approach on a set of examples from the domain of automated control, robotics and digital signal processing.

BibTeX

@inproceedings{jha-nsv13,
  author    = {Susmit Jha and Sanjit A. Seshia},
  title     = {Synthesis of Optimal Fixed-Point Implementations of Numerical Software Routines},
 booktitle = {Proc. Sixth International Workshop on Numerical Software Verification (NSV)},
 month = "April",
 year = {2013},
 abstract = {In this paper, we present an automated technique SWATI: Synthesizing 
Wordlengths Automatically Using Testing and Induction, which uses a combination 
of Nelder-Mead optimization based testing, and induction from examples 
to automatically synthesize optimal fixedpoint implementation of numerical routines. 
The design of numerical software is commonly done using floating-point 
arithmetic in design-environments such as Matlab. However, these designs are 
often implemented using fixed-point arithmetic for speed and efficiency reasons 
especially in embedded systems. The fixed-point implementation reduces implementation 
cost, provides better performance, and reduces power consumption. 
The conversion from floating-point designs to fixed-point code is subject to two 
opposing constraints: (i) the word-width of fixed-point types must be minimized, 
and (ii) the outputs of the fixed-point program must be accurate. In this paper, 
we propose a new solution to this problem. Our technique takes the floating-point 
program, specified accuracy and an implementation cost model and provides the 
fixed-point program with specified accuracy and optimal implementation cost. 
We demonstrate the effectiveness of our approach on a set of examples from the 
domain of automated control, robotics and digital signal processing.},
}