هل تعرف بالتأكيد أن RISC-V RTL الخاص بك لا يحتوي على أي مفاجآت؟

نظرًا للحداثة والتعقيد النسبيين لتصميمات RISC-V RTL ، سواء كنت تشتري نواة مدعومة تجاريًا أو تقوم بتنزيل عرض مفتوح المصدر شائع ، فهناك خطر ضئيل ولكنه غير صفري يتمثل في هروب مفاجآت غير مرغوب فيها دون أن يتم اكتشافها في منتجك النهائي. بالترتيب من الاحتمالية العالية إلى المنخفضة ، ضع في اعتبارك:

• وجود خطأ غريب في حالة الزاوية - لكنه ممكن تمامًا
• أخطاء "داخل" الإرشادات المخصصة التي تقوم أنت أو البائع بإنشائها لتطبيقك
• أخطاء "عند حواف" التعليمات المخصصة - على سبيل المثال ، يتم تنفيذ التعليمات بشكل صحيح ، ولكنها تترك الجهاز بطريقة ما في حالة تالفة
• ذات صلة: ميزات جديدة غير موثقة و / أو محددة بشكل سيئ تفتح ثغرات في التصميم عن غير قصد
• تم إدخال منطق طروادة الضار خلسة عبر هجوم سلسلة التوريد

نهج التخفيف المشتركة

بطبيعة الحال ، فإن خط الدفاع الأول هو فحص الخبراء لكود RTL الوارد أو الذي يتم تطويره. من الواضح أنه يجب القيام بذلك ؛ ولكن يجب أن يكون واضحًا بنفس القدر أن هذه التقنية - كما يقولون في عالم الرياضيات - "ضرورية ولكنها ليست كافية" (حتى لو كان لديك البروفيسور باترسون نفسه راجع شفرتك).

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

خلاصة القول هي أن الطريقة الوحيدة للتأكد تمامًا من خلو RISC-V RTL من أي مفاجآت طبيعية أو خبيثة هي تطبيق طرق رسمية شاملة للتحقق من التصميم.

وقال أسهل من القيام به، أليس كذلك؟

نعم ولا: قبل 14 عامًا ، كان هذا النوع من التحليل ممكنًا فقط بواسطة الباحثين الحاصلين على درجة الدكتوراه باستخدام برامجهم اليدوية الخاصة. ولكن منذ عام 2008 ، تم تطوير الأدوات والتقنيات بشكل منتج بحيث يمكن لأي شخص على دراية بأساسيات التحقق الرسمي وكتابة معيار IEEE القياسي System Verilog Assertions (SVA) التقدم والنجاح هنا بسرعة.

عملية رسمية من ثلاث مراحل

يتضح التدفق الرسمي الموصى به على النحو التالي:

1. قم بإنشاء منضدة اختبار رسمية "تصمم" مواصفات DUT
2. حدد قيود الإدخال وعمليات التحقق التي سيتم تشغيلها مقابل DUT
3. تنفيذ التحليل

الخطوة 1 - قم بإنشاء منضدة اختبار رسمية "نموذج" لمواصفات DUT

أساس هذه المنهجية هو كتابة مجموعة من الخصائص التي تمثل سلوك كل تعليمة في تصميم RISC-V الخاص بك. تتمثل المهمة في التقاط تأثير تعليمات معينة على مخرجات IP والحالات المعمارية الداخلية (في عالم RISC-V ، هذا هو عداد البرنامج (PC) وملف التسجيل (RF)) لأي تسلسل إدخال طويل تعسفيًا. يتم ذلك باستخدام امتداد مبني لهذا الغرض لـ IEEE SVA يسمى Operational SVA. باختصار ، هذه مكتبة يتم شحنها مع أداة التحقق الرسمية من المعالج ؛ ومن وجهة نظر مهندس التحقق ، يبدو أنه مجموعة فرعية بديهية من كود SVA المألوف. يوضح الشكل 1 الهيكل العام:

تعليمات الملكية_A ؛ // الحالة المفاهيمية t ## 0 ready_to_issue () و // المشغل t ## 0 opcode == يتضمن instr_A_opc // الحالة المفاهيمية t ## 0 ready_to_issue () و // مخرجات واجهات الذاكرة // قراءة التعليمات التالية t ## 0 imem_access (instr_A_opc) و // data load / store t ## 1 dmem_access (instr_A_opc) و // السجلات المعمارية t ## 1 RF_update (instr_A_opc) و t ## 1 PC_update (instr_A_opc) endproperty 

الشكل 1: هيكل رمز SVA التشغيلي الذي يلتقط مواصفات تعليمات المعالج. [1]

بالإشارة إلى الشكل 1 ، الجانب الأيسر من مشاركة (جزء من الكود فوق الكلمة يدل) يحدد متى يكون الجهاز جاهزًا لإصدار تعليمات جديدة ، والإرشادات التي يتم إصدارها. يلتقط التأكيد القيم الحالية للحالات المعمارية ، وفي الجانب الأيمن من التضمين (جزء من الكود أقل من الكلمة يدل) ، يثبت قيمهم التالية.

بالإضافة إلى ذلك ، يجب إثبات صحة مخرجات المعالج - في هذه الحالة للتأكد من أن التعليمات تصل إلى البيانات المتوقعة ومواقع ذاكرة التعليمات. يثبت التأكيد أيضًا أن الجهاز جاهز لإصدار تعليمات جديدة في الدورة التالية. هذا أمر بالغ الأهمية لفصل التحقق من التعليمات عن تسلسل التعليمات التي يمكن أن تكون جزءًا منها. على سبيل المثال ، يمكن أن يتم تنفيذ التعليمات A بشكل صحيح ، ولكنها تترك الجهاز في حالة تالفة. قد تتسبب هذه الحالة الخاطئة في أن ينتج عن التعليمات التالية B نتائج غير صحيحة بدون خطأ من جانبها. ومن ثم ، مع نهج SVA التشغيلي ، سوف يمر تأكيد التحقق من التعليمات B ، بينما تفشل تعليمات التحقق من التأكيد A (حيث يمكن أن تستمر عمليات الذاكرة للقراءة والكتابة لعدة دورات).

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

[ملاحظة: بالنسبة لمن هم على دراية بالمحاكاة أو التغطية الوظيفية الرسمية ، فإن فكرة الاكتمال هذه لا تعتمد على مقاييس التغطية الهيكلية ، أو على إنشاء وجمع المقاييس لنموذج التغطية الوظيفية. بدلاً من ذلك (والتقدم قليلاً في الخطوات والنتائج المتبقية) ، فإن ناتج التحليل هنا يتعلق بالحصول على البراهين الكاملة لجميع الخصائص. تُظهر البراهين الكاملة أيضًا أنه لا توجد وظيفة أخرى - كانت غير محددة أو غير متوقعة (خطأ في المواصفات أو الترميز) ، أو تم إدراجها بشكل ضار - لم يتم التقاطها بواسطة هذه المجموعة من الخصائص. إعادة الصياغة ، تتمحور هذه المنهجية حول تحقيق "تغطية خطة الاختبار" بنسبة 100٪ كما تم التحقق من ذلك من خلال نتائج التحليل الرسمية الشاملة - حيث لا يوجد شيء "كامل" أكثر من الدليل الرياضي!]

الخطوة 2 - تحديد قيود الإدخال وعمليات الفحص التي سيتم تشغيلها مقابل DUT

لاستكمال خصائص المواصفات لكل تعليمة ، فإن الخطوة التالية هي تحديد قيود الإدخال وأي عمليات فحص إضافية للمخرجات. مرة أخرى ، يتم استخدام SVA التشغيلي ، حيث يحدد المستخدم الآن "خطة اكتمال" لتحديد كل من المدخلات القانونية والإشارات غير القانونية التي يجب على DUT تجاهلها. وفقًا للمثال الموضح في الشكل 2 ، هناك ثلاثة أقسام: افتراضات التحديد ، ومتطلبات التحديد ، والرسم البياني للممتلكات.

معالج الاكتمال Design_assumptions: // المدخلات محددة (imem_data_i) ؛ محدد (dmem_valid_i) ؛ إذا تم تحديد (dmem_valid_i) (dmem_data_i) endif ؛ Design_requirements: // OUTPUTS محددة (imem_read_o) ، إذا (imem_read_o) محددة (imem_addr_o) endif ؛ محدد (dmem_enable_o) ؛ إذا تم تحديد (dmem_enable_o) (dmem_rd_wr_o) ، تم تحديد (dmem_addr_o) endif ؛ // تحديد الدول المعمارية (كمبيوتر) ؛ مصممة (RF) ؛ property_graph: all_instructions: = تعليمة_نوت_أ ، تعليمات_إضافة ، تعليمات_سوب_أ ، [...] جميع التعليمات -> جميع_التعليمات ؛ الاكتمال النهائي 

الشكل 2: مثال لخطة الاكتمال بافتراضات ومتطلبات التحديد المشروط.

للتوضيح:

• إن “Design_assumptions” هو ببساطة اسم منمق لقيود قيمة المدخلات
• "متطلبات التحديد" هي تعريف للإشارات التي يجب التحقق منها (كل من إشارات خرج المعالج والحالات المعمارية)
• يعد قسم "property_graph" مجرد ربط لهذا الملف بجميع الخصائص التي تم إنشاؤها في الخطوة 1

تلخيص ما وصلنا إليه في هذه المرحلة: في الخطوة 1 ، قمت بإنشاء نموذج فعال لدورة DUT يجب إثبات صحته في جميع الأوقات وجميع المدخلات ؛ في الخطوة 2 ، تقوم بإعداد القيود وأي سلوكيات خاصة يجب البحث عنها. أضفها معًا ، وفي الواقع لديك طاولة اختبار رسمية جاهزة للتشغيل!

الخطوة 3 - تنفيذ التحليل

الهدف من جميع الأدوات الرسمية هو إثبات بشكل شامل أن جميع الخصائص صحيحة لجميع الأوقات وجميع المدخلات. في حالة التحقق من معالج RISC-V ، تعمل الأداة لإثبات أنه يمكن مطابقة أي تسلسل إدخال طويل عشوائيًا مع تسلسل فريد من SVA التشغيلي المحدد الذي يتنبأ بقيم المخرجات والحالات المعمارية.

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

في كلتا الحالتين ، عندما يتم إصلاح هذه المشكلات وتثبت الأداة جميع الخصائص ، تكون النتائج "كاملة" حقًا - أي يمكنك أن تكون متأكدًا رياضيًا من عدم وجود أخطاء في ترميز RTL - أثبت التحليل الرسمي حرفيًا عدم وجود أي أخطاء !

النتائج

أولاً ، كما هو مذكور أعلاه ، استفاد العديد من مطوري المعالجات على مر السنين من هذا التدفق [2] ، [3] ، [4].

باختبار هذه المنهجية مع RISC-V ، أجرى زملائي دراسة حالة باستخدام نواة المصدر المفتوح المشهورة Rocket Chip. على وجه التحديد ، تم فحص تكوين RV64IMAFDC - sv39 vm. هذا هو معالج أساسي 64 بت مع نظام ذاكرة ظاهري 39 بت [5] وملحقات ، مثل التعليمات المضغوطة والذرية [6]. يستخدم تطبيق RISC-V ISA مفتوح المصدر هذا خط أنابيب من خمس مراحل ، إصدار واحد ، بالترتيب مع إكمال خارج الطلب لتعليمات زمن الوصول الطويل ، مثل عمليات التقسيم أو ذاكرة التخزين المؤقت المفقودة. يدعم النواة أيضًا تنبؤ الفروع وتعديل وقت التشغيل لسجل "misa" ، مما يسمح له بإيقاف تشغيل بعض امتدادات مجموعة التعليمات.

على الرغم من أن هذه اللقطة من Rocket Chip قد تم التحقق منها على نطاق واسع وتسجيلها عدة مرات ، فقد تم تحديد أربعة سلوكيات مشبوهة غير معروفة سابقًا وإبلاغ مطوري Rocket Core RTL بها. تم اكتشاف هذه المشكلات ([7] و [8] و [9] و [10]) فقط من خلال التطبيق المنهجي لنهج التحقق الرسمي الكامل الموضح في هذه المقالة.

بالتفصيل [10] على وجه التحديد - اكتشاف أمر غير قياسي CEASE (رمز التشغيل 0x30500073) في RTL: من الواضح أن فريق Rocket Chip قد تأخر في توثيقهم (وقاموا بإصلاح هذا فورًا تقريبًا عند تقديم طلب سحب GitHub). النقطة الأكبر هي أن هذا يوضح أن المنطق المطلوب لتنفيذ تعليمات كاملة - عشرات الأسطر من التعليمات البرمجية والعديد من بوابات المنطق المركب والموضوع والموجه - يمكن أن يفلت من الكشف عن طريق الفحص البصري ، ومحاكاة RTL ، ومحاكاة مستوى البوابة ، وكلها عملية التنفيذ الخلفية ، ونماذج الأجهزة في المختبر!

لكن ماذا عن أداء هذا التدفق؟

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

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

نبذة عامة

يستخدم نهج التحقق الكامل من المعالج المستند إلى النظام والمقدم في هذه المقالة امتدادًا لـ IEEE SVA ، التشغيلي SVA ، للتحقق رسميًا من خلو RISC-V ISA من الفجوات والتناقضات. على عكس مناضد اختبار المحاكاة العشوائية المقيدة أو المحاكاة أو النماذج الأولية المادية ، فإن المجموعة الكاملة من الخصائص والقيود تكتشف بشكل شامل العديد من أنواع أخطاء RTL ، فضلاً عن وجود أكواد غير موثقة أو محددة بشكل سيئ وأحصنة طروادة الخبيثة.

مراجع حسابات

1-2019 مؤتمر GOMACTech ، البوكيرك ، نيو مكسيكو ، 28 مارس 2019: التحقق الرسمي الكامل من عناوين IP لمعالج RISC-V للأجهزة المتكاملة الموثوقة الخالية من أحصنة طروادة ، David Landoll ، وآخرون.

2 - DVCon 2007: التحقق الرسمي الكامل من TriCore2 والمعالجات الأخرى ، Infineon Gmbh.

٢٠٢٤/٢٠٢٣^st مؤتمر أتمتة التصميم (DAC): تم تطبيق التحقق الرسمي على منصة تصميم Renesas MCU باستخدام أدوات OneSpin

4 - DVCon Europe 2019: التحقق الرسمي الكامل من عائلة DSPs للسيارات ، Bosch Gmbh.

5 - دليل مجموعة تعليمات RISC-V ، المجلد الثاني: العمارة المميزة ، إصدار المستند 1.10.

6 - https://github.com/freechipsproject/rocket-chip [تمت الزيارة في 20 كانون الأول (ديسمبر) 2018]

7 - نتيجة تعليمات DIV غير مكتوبة لتسجيل ملف
https://github.com/freechipsproject/rocket-chip/issues/1752

8 - تقوم JAL و JALR بتخزين تعليمات إرجاع مختلفة لجهاز الكمبيوتر
https://github.com/freechipsproject/rocket-chip/issues/1757

9 - إعادة تشغيل أكواد العمل غير القانونية والتسبب في آثار جانبية غير متوقعة
https://github.com/freechipsproject/rocket-chip/issues/1861

10 - تم اكتشاف CEASE في التعليمات غير القياسية (رمز التشغيل 0x30500073) في RTL ، https://github.com/freechipsproject/rocket-chip/issues/1868

11 - مدونة آفاق التحقق ، كيف يمكنك القول أن التحقق الرسمي شامل ؟، جو هوبسي الثالث
https://blogs.sw.siemens.com/verificationhorizons/2021/09/16/how-can-you-say-that-formal-verification-is-exhaustive/

المصدر: https://semiengineering.com/do-you-know-for-sure-your-risc-v-rtl-doesnt-contain-any-surprises/