SWATI: Synthesizing Word-Lengths Automatically Using Testing and Induction

Susmit Jha and Sanjit A. Seshia

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2013-7
February 8, 2013

http://www.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-7.pdf

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 citation:

@techreport{Jha:EECS-2013-7,
    Author = {Jha, Susmit and Seshia, Sanjit A.},
    Title = {SWATI: Synthesizing Word-Lengths Automatically Using Testing and Induction},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2013},
    Month = {Feb},
    URL = {http://www.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-7.html},
    Number = {UCB/EECS-2013-7},
    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.}
}

EndNote citation:

%0 Report
%A Jha, Susmit
%A Seshia, Sanjit A.
%T SWATI: Synthesizing Word-Lengths Automatically Using Testing and Induction
%I EECS Department, University of California, Berkeley
%D 2013
%8 February 8
%@ UCB/EECS-2013-7
%U http://www.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-7.html
%F Jha:EECS-2013-7