Search In this Thesis
   Search In this Thesis  
العنوان
Binary floating point arithmetic verification using a standard language to solve constraints /
الناشر
Khaled Mohamed Abdelmaksoud Nouh ,
المؤلف
Khaled Mohamed Abdelmaksoud Nouh
هيئة الاعداد
باحث / Khaled Mohamed Abdelmaksoud Nouh
مشرف / Hossam A. H. Fahmy
مشرف / Ibrahim Mohamed Qamar
مشرف / Ashraf M. Salem
تاريخ النشر
2016
عدد الصفحات
104 P. ;
اللغة
الإنجليزية
الدرجة
ماجستير
التخصص
الهندسة الكهربائية والالكترونية
تاريخ الإجازة
18/3/2017
مكان الإجازة
جامعة القاهرة - كلية الهندسة - Electronics and Communication
الفهرس
Only 14 pages are availabe for public view

from 121

from 121

Abstract

Verification of floating point (FP) units is a difficult task to achieve, and the cost of post-production bugs is severe. This is due to dealing with a large bit stream of inputs; simulation based verification fails to cover all possible input combinations and hence does not guarantee a 100% bug free design. On the other hand, formal methods are efficient in verification of FP arithmetic, yet they require creating a formal model, they cannot work on an optimized version of a design and may fail with complex designs due to state space explosion. Our framework provides a new verification methodology that uses a constraint based random technique to generate test vectors for validating binary FP arithmetic instructions. The constraints used in our verification are written in system verilog (SV) language and can be solved with any SV constraint solver tool. For every arithmetic operation, the written constraints couple the operands, intermediate results, rounding direction and the result evaluation to comply with the FP IEEE standard (IEEE Std 754-2008). The new proposal is generic and can be used to verify any software or hardware binary FP design/library. Also, it proves feasibility and usefulness in finding bugs for various binary FP arithmetic operations for single and double precision formats