A memory-efficient canonical data structure for decimal floating point arithmetic systems modeling and verification

Abstract

Decimal floating point (DFP) number representation was proposed in IEEE-754-2008 in order to overcomebinary floating point inaccuracy. Neglecting binary floating point verification has resulted in significant validity andeconomic losses. Formal verification can be a solution to similar DFP design problems. Verification techniques aiming atDFP are limited to functional methods whereas formal approaches have been neglected and traditional decision diagramscannot model DFP representation complexity. In this paper, we propose an efficient canonical data structure that canmodel DFP properties. Our novel data structure models coefficient, exponent, sign, and bias of a DFP number. Wewill prove mathematically that our data structure is canonical. We will also show that the size of the proposed datastructure will grow linearly for a DFP number for all format lengths, so our data structure can be built with a reasonableamount of memory and run time. Experimental results support our mathematical discussion for linear growth of theDFP data structure. Moreover, comparison of our data structure with integer decision diagrams reveals that our modelis also efficient for modeling integer functions when utilized as an integer level diagram.