Verification of fixed-point datapaths with comparator units using Constrained Arithmetic Transform (CAT)

Arithmetic Transform (AT) [1, 16, 17] is an efficient spectral technique, to analyze range and precision of fixed-point polynomial datapaths, among other methods including AA [4, 15] and SMT [5]. However, the major inefficiency of AT is that it cannot handle the datapaths with comparator units, which imply the non-arithmetic if-statements. This paper presents the approach, Constrained Arithmetic Transform (CAT), to perform range and precision analysis of fixed-point datapaths with comparator units. A custom branch-and-bound search is also introduced to provide more cutting branches and perform faster analyses of range and precision, by making use of safe and negligible overestimations. Experimental results prove the efficiency of our approach.