Solving Constraints on the Intermediate Result of Decimal Floating-Point Operations

The draft revision of the IEEE Standard for FloatingPoint Arithmetic (IEEE P754) includes a definition for decimal floating-point (FP) in addition to the widely used binary FP specification. The decimal standard raises new concerns with regard to the verification of hardware- and software-based designs. The verification process normally emphasizes intricate corner cases and uncommon events. The decimal format introduces several new classes of such events in addition to those characteristic of binary FP. Our work addresses the following problem: Given a decimal floating-point operation, a constraint on the intermediate result, and a constraint on the representation selected for the result, find random inputs for the operation that yield an intermediate result compatible with these specifications. The paper supplies efficient analytic solutions for addition and for some cases of multiplication and division. We provide probabilistic algorithms for the remaining cases. These algo...

• Type: Conference
• Year: 2007
• Where: ARITH
• Authors: Merav Aharoni, Ron Maharik, Abraham Ziv
• Keywords: Applied Computing, ARITH 2007, Binary Fp, Binary Fp Specification, Decimal Standard Raises