A hybrid arithmetic transform for precision analysis of floating-point polynomial specifications

Precision analysis of floating-point polynomial data-flow-graphs in terms of the error measure Maximum Mismatch (MM) is a challenging verification problem in computer arithmetic and embedded systems. In this paper by pairing the spectral technique Arithmetic Transform (AT) with Interval Arithmetic (IA), we introduce a static analysis to compute an overestimation of MM for floating-point polynomial specifications. The proposed analysis is applicable to fixed-point designs as well. We compare our solution with Affine Arithmetic (AA), the Gappa tool, which uses IA, as well as simulation-based methods, on a set of polynomial benchmarks. Experiments show that our analysis results in much lower overestimations of MM compared to previous work.