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

摘要

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