An efficient algorithm of performing range analysis for fixed-point arithmetic circuits based on SAT checking

Allocating bit-widths is a necessary step in high-level synthesis. The main disadvantages of past methods, such as dynamic analysis or affine arithmetic, lie in low efficiency and coarse results which may lead to huge execution time and unnecessary additional bits for representation. In this paper, an algorithm is based on static analysis is proposed to perform range analysis and allocate integer bit-widths for an arithmetic datapath. The efficient algorithm can calculate the error bound between the exact range and the obtained range.