Arithmetic operations debugging and verification

تنقيح العمليات الحسابية والتحقق منها

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.

تتحدث جودة متجهاتنا عن نفسها فقد اكتشفت أخطاء في عدد من التصميمات:

  • في كل التصميمات العشرية64 والعشرية128 لسيلميندز. في الواقع بدأ هذا المشروع للتحقق من صحة هذه التصميمات خاصة وتم إصلاح المشاكل التي وجدت.
  • في عمليتي الجذر التربيعي والضرب المدمج مع الجمع في برنامج decNumber الذي طوره الدكتور مايك كاوليشو أثناء عمله مع أي بي إم. أبلغنا عن أخطاء الضرب المدمج مع الجمع في يوليو وأغسطس 2010 و عن الجذر التربيعي في ديسمبر 2010 وكل هذه الأخطاء كانت في الإصدار 3.68.
  • في عملية الضرب المدمج مع الجمع العشرية128 في برنامج إنتل للحسابات العشرية الذي طوره الدكتور ماريوس كورنيا لعمله في إنتل. أبلغنا عن الأخطاء في يوليو 2011 في الإصدار 2.0 وتم إصلاحها في الإصدار 2.0-التحديث الأول في أغسطس 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.

تاريخ المشروع

بدأ هذا المشروع في نوفمبر 2009 في قسم هندسة الإلكترونيات والاتصالات الكهربية بكلية الهندسة في جامعة القاهرة ولا يزال العمل جاريا فيه.

نشأ المشروع من خلال أبحاث مشتركة مع شركة سيلميندز ممولة من برنامج الأبحاث والتطوير والابتكار التابع لوزارة التعليم العالي والبحث العلمي المصرية والاتحاد الأوروبي. مكننا مشروع بحثي آخر مع شركة سيلميندز ممول من وزارة الاتصالات وتكنولوجيا المعلومات المصرية من استكمال العمل.

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:

[2] Amr Sayed-Ahmed, Hossam A. H. Fahmy, and Rodina Samy. Verification of decimal floating-point fused-multiply-add operation. In The Ninth ACS/IEEE International Conference on Computer Systems and Applications, (AICCSA), Sharm El-Sheikh, Egypt, December 2011.
[1] Amr Sayed-Ahmed, Hossam A. H. Fahmy, and Mahmoud Hassan. Three engines to solve verification constraints of decimal floating-point operations. In Forty-Fourth Asilomar Conference on Signals, Systems, and Computers, Asilomar, California, USA, November 2010.

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.

Operation Number of vectors Covered models
Add
2010_07_d64_add.zip(03MB), 2010_07_d64_add.md5sum 0136356 cancel, clamping, overflow, result, rounding, shift, sticky, trailing, type
2011_09_d128_add.zip(35MB), 2011_09_d128_add.md5sum 1247467 cancel, carry, overflow, result, rounding, shift, sticky, trailing, type
Mul
2010_07_d64_mul.zip(02MB), 2010_07_d64_mul.md5sum 0096853 clamping, overflow, result, rounding, sticky, trailing, type, underflow
2011_10_d128_mul.zip(34MB), 2011_10_d128_mul.md5sum 1103450 clamping, nines, overflow, result, rounding, sticky, trailing, type, underflow, zeros
FMA
2010_07_d64_fma.zip(11MB), 2010_07_d64_fma.md5sum 0425599 cancel, clamping, overflow, result, rounding, shift, sticky, trailing, type, underflow
2011_02_d64_fma.zip(14MB), 2011_02_d64_fma.md5sum 0502069 cancel, carry, clamping, overflow, result, rounding, shift, sticky, trailing, type, underflow
2011_09_d128_fma.zip(180MB), 2011_09_d128_fma.md5sum 4388066 cancel, carry, clamping, overflow, result, rounding, shift, sticky, trailing, type, underflow
Div
2011_03_d64_div.zip(03MB), 2011_03_d64_div.md5sum 0146148 nines, overflow, result, rounding, sticky, trailing, type, underflow, zeros
2011_10_d64_div.zip(17MB), 2011_10_d64_div.md5sum 0798816 nines, overflow, rounding, sticky, trailing, underflow, zeros
2011_04_d128_div.zip(12MB), 2011_04_d128_div.md5sum 0341808 nines, overflow, result, rounding, sticky, trailing, type, underflow, zeros
2011_11_d128_div.zip(62MB), 2011_11_d128_div.md5sum 1665375 nines, overflow, rounding, sticky, trailing, type, underflow, zeros
Sqrt
2011_03_d64_sqrt.zip(01MB), 2011_03_d64_sqrt.md5sum 0057833 nines, result, rounding, sticky, trailing, type, zeros
2011_04_d128_sqrt.zip(06MB), 2011_04_d128_sqrt.md5sum 0199025 nines, result, rounding, sticky, trailing, type, zeros