وقال تشو فنغ، لو Zhenghao، وقال تشو تشينغ

(جامعة سوتشو، وسوتشو 215006)

مع الزيادة الهائلة في رقاقة والتعقيد، والتحقق من المحاكاة لا يمكن أن تضمن اكتمال ناقلات اختبار، وخاصة بعض الشروط الحدية. طريقة التحقق رسمي لاستكمال اجتياز الفضاء حالته واكتمال جيد لا يتم تطبيق لتصميم وحدات على نطاق والصناعة والوحدات الفرعية. أما المعالج لوحدة الفاصلة العائمة، وذلك باستخدام عدد من الأدوات من الإيقاع JasperGold وحدات مفتاح التحقق رسمية للسيطرة على تدفق رمز تصحيح الخطأ (رمز تصحيح الخطأ، ECC)، وبرامج التكوين التسجيل (البرامج هندستها السجل، SAR)، و واستخدمت وحدة حساب وحدة مشتركة FPV (الملكية الرسمية التأكيد) واستنادا إلى اختبار طبيعة SEC (متسلسل التكافؤ التحقق) على أساس اختبار التكافؤ. وأظهرت النتائج أن، على أساس التحقق رسمي للتأكد من صحة تصميم يقلل بشكل كبير من التحقق دورات.

FPU؛ التحقق الرسمي؛ JasperGold؛ FPV، SEC

CLC: TN401، TP301

كود الوثيقة: A

DOI: 10.16157 / j.issn.0258-7998.2017.02.005

شكل الاقتباس الصيني: تطبيق عائمة وحدة نقطة معالج تشو فنغ، لو Zhenghao، تشو تشينغ. التحقق الرسمي التكنولوجيا الالكترونية، 2017،43 (2): 29-32.

الإنجليزية شكل الاقتباس: وقال تشو فنغ، لو Zhenghao، وقال تشو تشينغ. الفعالة طلبات رسمية في وحدة المعالجة المركزية وحدة الفاصلة العائمة .Application من تقنيات الالكترونية، 2017،43 (2): 29-32.

0 مقدمة

مع تزايد حجم وتعقيد تصميم الدوائر المتكاملة، وظيفية تصميم نظام التحقق تواجه تحديات خطيرة. ووفقا للاحصاءات، فقد تم استثمار التحقق من الوقت والجهد أكثر من 50 من تصميم كامل، واختبار وخطأ التشخيص للتكلفة أكثر من 50 من تكلفة المنتج التنفيذ. ولذلك، فإن إدخال أساليب المصادقة جديدة للتحقق من أن تصبح مهنة الساخنة والصعبة.

الطريقة التقليدية التحقق التناظرية، والبرمجيات نظام أو نموذج النظام الأساسي الأجهزة، يتم تحديد نتائج المقارنة بين ناقلات اختبار الإخراج إذا كان تصميم القياسية، والذي يعتمد إلى حد كبير على مدى اكتمال الاختبار ناقلات . عندما تواجه مع نطاق واسع التصميم والمحاكاة والتحقق تتكشف شيئا فشيئا حدوده، فمن الصعب تغطية جميع ناقلات اختبار لا يمكن ضمان تحقق النزاهة.

رسمي طرق التأكيد نظام فعال، اجتياز الفضاء الدولة بأكمله، وقادرة على تصميم التحقق الكامل، في السنوات الأخيرة من الاهتمام في هذه الصناعة. تشمل يعادل اختبار التحقق الرسمي، واختبار طبيعة ونظرية إثبات. وهو يشير إلى اختبار وظيفي التكافؤ بين أشكال مختلفة أي ما يعادل التحقق من وصف التصميم. طبيعة الاختبار باستخدام تصميم المنطق الزمني الميزات المذكورة، التي تم تصميم نظام التحقق شاملة لتلبية الاحتياجات الوظيفية. نظرية من النظام بديهية، والعمل تدريجيا على استخدام قواعد الاستدلال للتوصل إلى إثبات خصائصه مرغوب فيه، وطريقة التحقق الموظفين المهارات الرياضية والقدرة على استنباط تطالب خارج نادرا ما تستخدم من البحوث الأكاديمية. تطبيق الفعلي للمشروع في شكل دراسات التحقق من صحة، وتحسين كفاءة التحقق، دورة تطوير المنتج تقصير هو المهم.

واستنادا إلى وحدة نقطة رقاقة المعالج العائمة، JasperGold تطبيق الإيقاع أداة التحقق رسمية لمراقبة تدفق وحدة حساب وحدة مفتاح FPV وSEC كانت تستخدم للتحقق منها.

التحقق 1 SAR

هندسة البرمجيات تسجيل (برنامج هندستها السجل، SAR) في وحدة النقطة العائمة مثل منطقة تخزين مرحلة خط أنابيب الثاني. SAR عموما أربعة منافذ قراءة وأربعة منافذ الكتابة، البنك الداخلي يتكون من ثمانية كتل، كل كتلة البنك أساسا SRAM، وSRAM هو الكتابة القراءة، 128 دخول، 64 سجلات الهيكلية. SAR القراءة / الكتابة العملية، سيتم اختيار دخول المقابلة من بنك ثماني كتل في البنك، حيث البيانات التي ميناء القراءة / الكتابة. عند وصول عدة عمليات القراءة / الكتابة نفسها تظهر كتلة البنك، والصراع، وتحتاج إلى تقرير خطأ.

يستخدم طبيعة اختبار SAR في JasperGold من FPV. ويستند الاختبار الرئيسي لطبيعة العمل على طبيعة (الملكية) التحقق من الحاجة إلى كتابة طريقة المقابلة لبناء واستكمال درجة سوف تؤثر بشكل مباشر على طبيعة نتائج التحقق. لغة نظام فيريلوج لديهم ممتلكات مشتركة والبولندي (الملكية مواصفات اللغة)، يتم اعتماد JasperGold هاتين اللغتين. SAR نقطة مفتاح التحقق: (1) قراءة من خلال مساحة العنوان بأكمله؛ (2) عندما يحدث تعارض، ما إذا كان الخطأ، (3) كشف في أوضاع التشغيل المختلفة، ما اذا كان يعمل.

عندما يتم تنفيذ نقل البيانات النهاية، فإن حزم البيانات بالمرور عازلة مرور أو الذاكرة المطلوبة للتحقق من سلامة نقل البيانات. لأن الذاكرة من هذا الهيكل من السهل أن نفهم، ونادرا ما تظهر الأخطاء، وبالتالي فإن عملية التحقق من جميع مراحل المشروع لن يسبب اهتمام الجميع. ولكن بسبب حالة كبيرة من مساحة الذاكرة، مما يجعلها تحقق الرسمي لتحسين أداء عنق الزجاجة. لحل هذه المشكلة، عندما تحقق من SAR، وذلك باستخدام النموذج JasperGold توفير مسرع اللوحة برهان (رسمي لائحة إثبات مسرع، PA). PA يمكن أن الذاكرة المجردة، مع الحفاظ على معلومات كافية لضمان تحقيق نتائج دقيقة في لوحة النتائج الرسمية. وعلى وجه الخصوص عند التحقق من SAR، استبدال البنك SAR بواسطة PA، ومن أجل تبسيط التعقيد من التحقق، عند بناء تأكيدات السمة، والفكرة الأساسية هي: في غياب الصراع، فإن البيانات قرأ قراءة العملية يجب أن يكون مساويا لآخر بيانات عملية الكتابة المقابلة لعنوان الكتابة. سوف تحقق تتوافق مع القراءة تتم مقارنة البيانات البيانات والكتابة، والحدث الكشف عن الصراع، وتكوين محددة من التحقق هو مبين في الشكل.

من خلال تحليل نتائج التحقق، وجد مكتوبا في أغلفة الملكية جميع النقاط التحقق، وكلها قد ثبت. خاصة بعد استخدام PA، أثبتت تقصير كبير في الوقت المستهلك، والأداء التحقق بشكل ملحوظ. 2 و 3، لم تستخدم من قبل السلطة الفلسطينية، منفذ لSAR خلال كل مساحة العنوان للقراءة، الوقت الإجمالي لإثبات 286.41 الصورة، وبعد الاستخدام PA، الوقت اللازم لإثبات فقط 1.04 ثانية.

التحقق 2 ECC

للحفاظ على دقة واتساق البيانات، وتطفو السيطرة على خط الانابيب نقطة وحدة يدخل رمز تصحيح الخطأ (رمز تصحيح الخطأ، ECC) فحص آلية لتنفيذ الكشف عن الخطأ في المعاملات المصدر وتصحيحها على الفور، وذلك باستخدام البيانات يمكن تنفيذ شفرة ECC "الصحيح موضوع اثنين"، أي فقط عند حدوث خطأ، والخطأ يمكن تصحيح البيانات من 1 بت، 2 بت عندما تكون البيانات وجود خطأ، فقط تم الكشف عن الخطأ ولكن لا يمكن استعادتها.

، ECC التكافؤ يتم إعادة الاستفادة من البيانات الأولية والبيانات رمز تصحيح خطأ في رمز ECC قراءة أحادي المعامل XOR ولدت صناعيا وفقا لما إذا كانت البيانات الحكم خطأ قليلا متكاملة ومندمجة باستخدام بت تصحيح الخطأ للإخراج. يتم فحص ECC تصحيح الخطأ ECC الانتعاش إلى أن تكون صحيحة استنادا إلى بيانات تصحيح الخطأ، عندما متلازمة بيانات أكبر من واحد، خطأ غير قابل للاسترداد.

يتم تنفيذ الاختيار ECC ECC والانتعاش في مراحل مختلفة من خط أنابيب من وحدتين، مستقلة ومترابطة. عندما يكون البيانات إشارة خطأ من خلال وحدة الاختيار ECC وعالية الانتاج، البيانات أن تكون هي التي تحرك خطأ التصحيح وتصحيح الخطأ رموز ECC إلى وحدة نمطية الانتعاش لتحديد ما إذا كان تصحيح الخطأ والبيانات يمكن استردادها. إذا تم التحقق من وحدات اثنين، رمز تصحيح الخطأ لإنتاج الآليات المعقدة التي تعتمد على إشارة الدخل ويزيد من صعوبة التحقق. لذلك، يتم توصيل الوحدتين مباشرة إلى وحدة التحقق وظيفة من خلال مقارنة بيانات المدخلات والبيانات لتصحيح الخطأ.

4، دائرة الجمع بين التصميم تنفيذ اختباري وتصحيح الخطأ في إدخال البيانات، والوصول إلى وحدة توليد البيانات وحدة توليد خطأ لتوليد تصحيح رمز الخطأ ECC الاختيار على إشارة المدخلات، وإدخال إشارة إلى خاصية تجنب وصف آلية معقدة لتوليد رمز تصحيح الخطأ. خطأ توليد البيانات وحدة إشارة حقن الخطأ المحدد على أساس عدد المدخلات من نمط الخطأ ه، 0 أخطاء، والخطأ إشارة المسمية بت محددة البيانات مقلوب. الاختيار ECC، ECC استعادة وتوليد ECC وحزمة وحدة توليد خطأ ككل، وتنفيذ تصميم اختبار الطبيعة.

لكتلة ECC جنبا إلى جنب، وبيانات عن نوع مختلف من الخطأ، وهناك ثلاثة أنواع الممتلكات للتفتيش. في حال عدم وجود أخطاء البيانات، الخطأ إشارة خرج هو 0، 1 'قليلا عندما تكون البيانات وجود خطأ، وإخراج خطأ، فإن البيانات غير قابل للاسترداد البيانات تصحيح الخطأ 0 وإدخال البيانات على قدم المساواة، 2 بت من البيانات وجود خطأ، خطأ الانتاج (1) وإشارة البيانات هو غير قابل للاسترداد. الجيل خطأ المنطق، عندما هو المطلوب لإنتاج 2 بعض الأخطاء، فمن الضروري لضمان مختلفة بعض الشيء مقلوب مرتين، أي خطأ 0! = 1 خطأ. بت البيانات المنطق خط أنابيب الفعلي هو 128 بت، منها موصوفة 64 بت البيانات من ارتفاع وانخفاض 64 بت التحقق الممتلكات.

سوف JasperGold تعبر عن مساحة الدولة، تستغرق وقتا طويلا للتحقق نتيجة عرض 101 ق، وثبت أن تحتوي على جميع سمات وصف التصميم، وصفت وحدة الاختيار ECC "II عينة" وظيفة ECC حدة انتعاش "واحد صحيح" تنفيذها.

3 التكافؤ المشترك حدة التدقيق

النقطة العائمة وحدة حسابية مناسبة لوحدة التحقق الرسمية، ولا سيما اختبار التكافؤ. قام التكافؤ التحقق من العمل الرئيسي هو تطوير النموذج المرجعي يلبي مواصفات تصميم نموذج مرجعي يمكن كتابة مع مرونة التطبيقات في لغات مختلفة. صناعة التيار أداة التحقق رسمية يعتمد فقط فيريلوج HDL وVHDL، RTL إلى RTL التكافؤ فحص وضعت أكثر نضجا، لديه مستوى الكمال نسبيا. JasperGold المستخدمة في هذا الدعم ورقة VHDL وفيريلوج HDL لغتين، وهناك بعض أدوات دعم لغة C، ولكن أقل C إلى RTL التكافؤ فحص تطوير التطبيقات ليست ناضجة جدا.

عندما الحساب IP النقطة العائمة تصميم الوحدة والتنمية والتعددية الأولى من وحدات مشتركة الأساسي لعملية IP تم توحيد التصميم، ودعوة موحدة مشتركة بعد كل تصميم وحدة IP. ولذلك، فإن النقطة العائمة وحدة حسابية من وحدة التوثيق المشتركة أول IP التصديقات، ثم التحقق من صحة كل IP. لاعتبارات عملية المشروع، عندما وحدات مشتركة للمصادقة، وذلك لأن وحدة وظيفية مشتركة نفذت بسيط نسبيا، منخفضة التعقيد، وبالتالي فإن وحدة باستخدام النموذج المرجعي المشترك مكتوب في فيريلوج HDL. عملية التحقق من صحة IP، منذ عالية التعقيد IP، وتطوير النموذج المرجعي المناسب من عبء العمل الثقيل التحقق الرسمي وحصة محاكاة نموذج مرجعي موحد التي وضعتها لغة C. منذ JasperGold لا يدعم C إلى RTL التحقق من التكافؤ، واستخدام منصات التحقق الأخرى لوقت التحقق من صحة IP.

تستخدم معادلة مشتركة وحدة فحص JasperGold المجلس الأعلى للتعليم، بما في ذلك الأفعى، وطارح، ناقل دوري، الأصفار البادئة، وضاغط 2/4، مستدير (مستدير) وحدات. في إعداد النموذج المرجعي، بالإضافة إلى التأكد من أن يمكن أن تكون متكاملة، ولكنها تحتاج أيضا إلى النظر في وظائف مناسبة.

ويبين الشكل 5 شكل مستدير من تقرير التحقق، يمكن أن ينظر إليه، مقارنة مع المحاكاة، والوقت لإثبات ما يقرب من الصفر تحقق زيادة كبيرة في سرعة. أيضا هذه الميزة هي أكثر وضوحا عند التحقق من IP كامل، و في كل نقطة وحدة حسابية عائمة لالتكافؤ فحص IP، بالإضافة إلى وحدة تتكاثر وظيفة إضافية يتطلب تغييرات إشارة خاصة نموذج ، مما بما في ذلك وحدة نمطية المفرق، العد التنازلي وحدة التقييم وتكون قادرة على تتلاقى بسرعة نسبيا، والحد بشكل كبير دورة التحقق.

4 موجز

وتصف هذه الورقة تطبيق وحدة محددة الفاصلة العائمة في التحقق رسميا من التحقق وظيفية. وأظهرت النتائج أن، بالمقارنة مع محاكاة التناظرية والتحقق رسميا من بنية معقدة بدون منصة التحقق والكتابة كميات هائلة من التحفيز اختبار، يقلل كثيرا من الجهد للتحقق، مع تحسين الموثوقية وتقصير دورة التحقق.

مراجع

LAM W.Hardware التحقق من تصميم: المحاكاة والنهج الرسمي القائم على طريقة .US: برنتيس هول PTR 2005.

جي يون لين، هوا شين، الخ التحقق الرسمي غودسون المعالجات الدقيقة 2 من العائمة ميزة تقسيم نقطة بحوث الحاسب والتنمية، 2006 (10): 1835-1841.

JACOBI C، W KAI، PARUTHI V، وآخرون al.2005 تصميم وأتمتة واختبار في مؤتمر أوروبا ومعرض (تاريخ 2005) .Munich 2005.