Arithmetic operations debugging and verification

• Project description
• Sample of bugs found
• Project history
• Project members
• Publications
• Test vectors
  • Syntax
  • Decimal operations

Project description

We aim to produce high quality test vectors for the various arithmetic operations. A test vector is the set of inputs (operands and rounding direction if needed) and the corresponding correct outputs (result and flags if any). High quality means that the test vectors are not just randomly selected but they are rather directed to uncover potential problems in the design. The project started with the verification of floating point operations.

The quality of our work speaks of itself. Our test vectors discovered bugs in several designs:

• in all the decimal64 and decimal128 designs of SilMinds floating point arithmetic operations. In fact this project started in order to verify those specific designs which were subsequently corrected.
• in the FMA and Sqrt operations of the decimal floating point library decNumber developed by Dr. Mike Cowlishaw while at IBM. We reported the FMA errors in July and August of 2010 and the SQRT error in December 2010 all against version 3.68.
• in the FMA for decimal128 in the Intel decimal floating-point math library developed by Dr. Marius Cornea from Intel. We reported the errors in July 2011 against version 2.0 which was subsequently fixed in version 2.0 update 1 of August 2011.

Project history

This research project started in November 2009 at the Electronics and Electrical Communications Department, Faculty of Engineering, Cairo University. This project is still under progress.

It grew out of collaboration on a research project with SilMinds funded by the RDI program of the Egyptian Ministry of Higher Education and the European Union. A sequel joint project with SilMinds funded by the ITAC program of the Egyptian Ministry of Communications and Information Technology allowed us to continue the work.

Project group members

Current members working on the project are:

• Amr Abdel-Fatah Sayed-Ahmed - Main Researcher
• Hossam A. H. Fahmy - Project Supervisor

Publications

Amr finished his MSc thesis in June 2011.

So far, two papers are published:

Try our test vectors

The first work on our test vectors was inspired by the FPGen project of IBM. The test vectors files follow the same syntax as in that project. Specifically, each line represents a single test vector with parts separated by spaces as follows:

1. The type and precision: d64 for Decimal64, or d128 for Decimal128.
2. The operation: + for add, - for subtract, * for multiply, / for divide, *+ for fused multiply-add, *- for fused multiply-subtract, or V for square root.
3. The rounding mode: > for (positive infinity), < for (negative infinity), 0 for (zero), =0 for (nearest, ties to even), or h> (nearest, ties away from zero).
4. The data for input operands: sign_significand_E_exp. Where the sign is either + or -, the significand is a string of decimal digits, exp is the value of the unbiased exponent written as an integer number.
   • SNaN numbers are represented using the string S.
   • QNaN numbers are represented using the string Q.
   • Infinities are represented using the string +inf or -inf.
5. A "->" sign, to separate inputs from results.
6. The data for output operand: sign_significand_E_exp. Where the sign is either + or -, the significand is a string of decimal digits, exp is the value of the unbiased exponent written as an integer number.
   • SNaN numbers are represented using the string S.
   • QNaN numbers are represented using the string Q.
   • Infinities are represented using the string +inf or -inf.
7. Exceptions that occur due to the operation: x (inexact), u (underflow), o (overflow), z (division by zero) and i (invalid).

Decimal FP operations

For an explanation of the relevant models used to generate the test vectors please refer to the publications section, especially the MSc thesis of Amr Sayed-Ahmed.

Each zip file below archives a directory with files for the operation indicated by the file name and dated as in the name as well. The md5sum files hold checksum values for the corresponding files. The DecTool of SilMinds is able to parse our files and generate the corresponding hexadecimal or binary strings necessary for circuit simulation.

The files provided below with test vectors for the decimal FP operations are copyrighted to Amr Sayed-Ahmed and Hossam A. H. Fahmy. They are provided as is without any implied warranties. The persons who download the files are free to use them for any purpose under their own responsibilities. The copyright owners provide the files in the hope that they will be useful to others but give no guarantees. We would appreciate if you reference our work and give us credit for it.