Optimization Techniques for Verification of Out-of-Order Execution Machines
المؤلف
المصدر
Journal of Electrical and Computer Engineering
العدد
المجلد 2010، العدد 2010 (31 ديسمبر/كانون الأول 2010)، ص ص. 1-7، 7ص.
الناشر
Hindawi Publishing Corporation
تاريخ النشر
2010-09-08
دولة النشر
مصر
عدد الصفحات
7
التخصصات الرئيسية
العلوم الهندسية و تكنولوجيا المعلومات
تكنولوجيا المعلومات وعلم الحاسوب
الملخص EN
We develop two optimization techniques, flush-machine and collapsed flushing, to improve the efficiency of automatic refinement-abased verification of out-of-order (ooo) processor models.
Refinement is a notion of equivalence that can be used to check that an ooo processor correctly implements all behaviors of its instruction set architecture (ISA), including deadlock detection.
The optimization techniques work by reducing the computational complexity of the refinement map, a function central to refinement proofs that maps ooo processor model states to ISA states.
This has a direct impact on the efficiency of verification, which is studied using 23 ooo processor models.
Flush-machine, is a novel optimization technique.
Collapsed flushing has been employed previously in the context of in-order processors.
We show how to apply collapsed flushing for ooo processor models.
Using both the optimizations together, we can handle 9 ooo models that could not be verified using standard flushing.
Also, the optimizations provided a speed up of 23.29 over standard flushing.
نمط استشهاد جمعية علماء النفس الأمريكية (APA)
Srinivasan, Sudarshan K.. 2010. Optimization Techniques for Verification of Out-of-Order Execution Machines. Journal of Electrical and Computer Engineering،Vol. 2010, no. 2010, pp.1-7.
https://search.emarefa.net/detail/BIM-477762
نمط استشهاد الجمعية الأمريكية للغات الحديثة (MLA)
Srinivasan, Sudarshan K.. Optimization Techniques for Verification of Out-of-Order Execution Machines. Journal of Electrical and Computer Engineering No. 2010 (2010), pp.1-7.
https://search.emarefa.net/detail/BIM-477762
نمط استشهاد الجمعية الطبية الأمريكية (AMA)
Srinivasan, Sudarshan K.. Optimization Techniques for Verification of Out-of-Order Execution Machines. Journal of Electrical and Computer Engineering. 2010. Vol. 2010, no. 2010, pp.1-7.
https://search.emarefa.net/detail/BIM-477762
نوع البيانات
مقالات
لغة النص
الإنجليزية
الملاحظات
Includes bibliographical references
رقم السجل
BIM-477762
قاعدة معامل التأثير والاستشهادات المرجعية العربي "ارسيف Arcif"
أضخم قاعدة بيانات عربية للاستشهادات المرجعية للمجلات العلمية المحكمة الصادرة في العالم العربي
تقوم هذه الخدمة بالتحقق من التشابه أو الانتحال في الأبحاث والمقالات العلمية والأطروحات الجامعية والكتب والأبحاث باللغة العربية، وتحديد درجة التشابه أو أصالة الأعمال البحثية وحماية ملكيتها الفكرية. تعرف اكثر