التحقق من الدوائر الرقمية. نظرة عامة

سأحاول التحدث بشكل عام حول التحقق من الدوائر الرقمية.

التحقق في هذا المجال هو عملية هامة تتطلب مشاركة المهندسين ذوي الخبرة. على سبيل المثال ، يجب على أخصائي التحقق الذي يعمل على الأنظمة التي تحتوي على وحدة المعالجة المركزية ، كقاعدة عامة ، امتلاك لغات البرمجة ولغات الأوامر (Tcl ، و bash ، و Makefile ، وما إلى ذلك) ، ولغات البرمجة (C ، C ++ ، المجمّع) ، HDL / HDVL (SystemVerilog [10 ، الملحق C - تاريخ اللغة] [11] ، Verilog ، VHDL) ، المنهجيات والأطر الحديثة (UVM).

تبلغ نسبة الوقت المستغرق في التحقق ما بين 70 إلى 80٪ من إجمالي وقت المشروع. أحد الأسباب الرئيسية لهذا الاهتمام هو أنه لا يمكنك إصدار "تصحيح" للرقاقة بعد وضعه في مرحلة الإنتاج ، ولا يمكنك إلا إصدار "أخطاء السيليكون" (لا ينطبق هذا على مشاريع FPGA / FPGA).

بواسطة الدوائر الرقمية ، أعني:

• الكتل الوظيفية المعقدة / الملكية الفكرية (SFB / IP) ؛
• رقائق مخصصة الدوائر المتكاملة (ASIC) المخصصة
• الدارات المتكاملة للمنطق القابل للبرمجة / صفيف بوابة البرمجة القابلة للبرمجة (FPGA) ؛
• أنظمة على رقاقة / نظام على الكريستال (SoC / SoC) ؛
• إلخ

مشاكل التحقق الفعلي

يمكن تقييم الحالة الحالية والاتجاهات في مجال التحقق من خلال التحديات والمشكلات التالية التي تواجهها [6]:

• حجم كائن التحقق (OB) ينمو باستمرار. حتى متحكم صغير نوع IC هو مجموعة من العشرات من وحدات فرعية ، في كثير من الأحيان مع وظائف معقدة. الشهادات المرحلية الكبيرة عبارة عن مجمعات يمكن أن يوجد فيها ما يصل إلى عشرات المليارات من الترانزستورات ، ولا يمكن إلا لخطة واحدة لإدارة الطاقة أن تتجاوز بعض المعالجات في التعقيد [8] ؛
• من المستحيل وضع مواصفات لنظام IMS في بداية المشروع ومتابعته فقط في المستقبل ، بل يتغير باستمرار خلال عملية التطوير (العميل يغير المتطلبات ، والمشاكل التقنية أو إيجاد حلول أكثر مثالية تجبر على إعادة النظر في النهج ، وما إلى ذلك). بناءً على ذلك ، ينبغي أن تدرك جميع العمليات ديناميات تغييرات المواصفات وأن يتم تعديلها وفقًا للمتطلبات ؛
• في كثير من الأحيان ، تعمل عدة فرق بعيدة عن بعضها البعض على التحقق من المشروع ، ويمكن أن يصل عددها إلى عشرات الأشخاص ؛
• يصل عدد الاختبارات الفردية وأنواعها إلى عدد كبير ، ويجب جمع نتائجها وتحليلها ؛
• تتطلب نمذجة الأنظمة الرقمية كثيرًا من وقت الكمبيوتر ؛
• يعتمد مدى اكتمال أهداف الاستعداد المحددة للمشروع إلى حد كبير على كفاءة الحدس والمتخصصين في التحقق ؛
• على الرغم من وجود مؤشرات تغطية المشروع مع الاختبارات (المقاييس) ، فإن الطريقة الوحيدة لإكمال التحقق هي أن تقرر تعليقه ، استنادًا إلى الاستنتاجات التالية: يجب وضع المال أو الوقت المستغرق في مرحلة المشروع في الإنتاج ، يبدو أنها وصلت إلى تغطية الكود 100 ٪ ، لقد تم الاختبار لمدة أسبوع الآن ولم نعثر على أي أخطاء ، إلخ.

أنواع التحقق

يمكن تقسيم التحقق من الدوائر الرقمية إلى الأنواع الرئيسية التالية:

1. وظيفية (التحقق الوظيفي) - الاسم يتحدث عن نفسه ، ويمكنك التحقق مما إذا كان النظام الخاص بك يؤدي وظائفه بشكل صحيح ؛
2. التحقق الرسمي - يحدد هذا التحقق معادلة تمثيلات النظام الخاص بك في المراحل المختلفة من مسار التصميم أو تنفيذ البيانات الموضوعة في الكود المصدري:
   
   • فحص التكافؤ (مثل RTL-to-RTL ، RTL-to-Gate ، Gate-to-Gate) ؛
   • فحص الممتلكات (فحص النموذج) (يتحقق من الخصائص (التأكيدات) المحددة في الكود باستخدام SVA (على سبيل المثال)).
3. تحليل الكود الثابت - التحقق من الكود المصدري وفقًا للمعايير الرسمية للامتثال لقواعد استخدام اللغة والإنشاءات الخاصة بها. في كثير من الأحيان ، يتم إرسال قواعد التحقق المكونة إلى RMM [4]. يشار عادةً إلى برامج التحقق من ذلك على أنها lint أو linter ؛
4. التحقق المادي - يتضمن بشكل أساسي فحوصات DRC و LVS و PERC ، إلخ. ، يتم فحص الأداء المادي للنظام للتأكد من الامتثال للمعايير التكنولوجية والامتثال للتمثيلات المادية والمنطقية ، إلخ. تكوين الشيكات يعتمد بشكل كبير على التكنولوجيا. عادةً ما يتم إجراء التحقق المادي بواسطة مهندس أو فريق تصميم طوبولوجي.
5. النماذج الأولية - استخدام FPGA للتحقق الوظيفي [18].

التحقق الوظيفي في نطاق كل العمل هو الأكثر أهمية ويتطلب مشاركة بشرية مباشرة.

يتطلب تحليل الشفرة الثابتة التكوين الأولي فقط للأدوات ، والتي تتوافق مع قواعد التصميم الداخلي التي اعتمدتها الشركة ، ثم تعمل الأداة على أنها توفر "إرشادات قيمة" للمطورين ولا تتطلب إشرافًا مستمرًا.

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

أمثلة أدوات التحقق

أمثلة على أدوات التحقق من الدائرة الرقمية (المسار الرقمي على القمة):

• أدوات إدارة التحقق
  
  • Mentor Graphics - إدارة التحقق من Questa
  • الإيقاع - vManager
  • سينوبسيس - فيردي ، مدير تنفيذ VC ("ExecMan")
• وظيفية - عادة المحاكاة
  
  • معلمه الرسومات - ModelSim ، QuestaSim
  • الإيقاع - قاطع ، Xcelium
  • سينوبسيس - VCS
  • برنامج مجاني من المطورين المستقلين - المحاكيات Verilator، Icarus [5]
• رسمي
  
  • معلمه الرسومات - رسمي برو ، كويستا التحقق الرسمي
  • الإيقاع - JasperGold ، Conformal LEC ، منهاج التحقق الرسمي
  • سينوبسيس - شكلي ، VC الرسمي
• تحليل كود ثابت
  
  • معلمه الرسومات - كويستا التحقق التلقائي
  • الإيقاع - هال ، JasperGold
  • سينوبسيس - SpyGlass ينت
• التحقق المادي
  
  • معلمه الرسومات - العيار
  • الإيقاع - بيغاسوس ، نظام التحقق المادي ،
  • سينوبسيس - هرقل ، مصدق IC

طرق التحقق الوظيفية

التحقق الوظيفي - عبارة عن مجموعة من الاختبارات ، وسأسمح لنفسي بشرط أن أقسم إلى ثلاث مجموعات (هذه ليست عقيدة ، إنها من تجربة شخصية):

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

يمكن أتمتة المرحلتين الأوليين باستخدام UVC / VIP (مكون التحقق العالمي / IP للتحقق) وبسرعة كبيرة يمكنك زيادة حجم الاختبارات المختلفة ، بما في ذلك تلك التي يتم إنشاؤها تلقائيًا. المرحلة الثالثة هي "تحفة" في التحقق ، هذه المرحلة تتطلب مقاربة وتجربة غير عادية ، من الصعب للغاية الأتمتة ، لأنه معظم الحالات هي خوارزمية منفصلة ، وربما برنامج نصي ل CAD أو تعليمات للشيكات "اليدوية".

أنواع مقاييس التحقق الوظيفية

المقاييس هي مؤشرات على تغطية اختبار المشروع. هناك حاجة إليها لفهم الاختبارات الأخرى التي يجب تطويرها للتحقق من المواقف المحتملة ومقدار الوقت الذي يستغرقه التحقق [16].

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

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

أنواع المقاييس [3]:

• طلاء وظيفي . يوضح مقدار اختبار وظيفة OB. يمكن تحديد معايير هذه التغطية من خلال خطة الاختبار وإدخال إنشاءات خاصة (covergroup [1]) في بيئة الاختبار و / أو OM ، ومراقبة ما إذا كان قد تم تنفيذ وظيفة / إجراء معين أم لا ، وما إذا كانت البيانات قد تغيرت بطريقة معينة ، وما إلى ذلك. يمكن جمع المعلومات من التصاميم المضمنة في شفرة المصدر تلقائيًا بواسطة CAD.
• تغطية التعليمات البرمجية - تغيير حالة إنشاء التعليمات البرمجية المصدر أثناء الاختبارات. يتم جمعها تلقائيا بواسطة CAD ، لا يتطلب إدخال أي هياكل في شفرة المصدر. على سبيل المثال:
  
  • سجلات التبديل (تبديل التغطية) ؛
  • نشاط كل سطر من التعليمات البرمجية (تغطية الخط) ؛
  • نشاط التعبيرات (تغطية البيان) ، في الواقع - هذا هو تغطية الخط ، ولكن يمكن تتبع التعبيرات التي تزيد عن سطر واحد في المحرر ؛
  • نشاط مقطع الشفرة داخل بيان أو إجراء شرطي (تغطية كتلة) ، وتغيير في تغطية البيان ؛
  • نشاط جميع فروع البيانات الشرطية مثل if ، case ، بينما ، كرر ، إلى الأبد ، من أجل ، حلقة (Branch Branchage) ؛
  • تغيير جميع الحالات (صواب ، خطأ) التعبيرات المنطقية للمكون (تغطية التعبير) ؛
  • حالة الجهاز الدولة (تغطية الجهاز المحدود الحالة).
• تغطية المطالبات . تعد العبارات عبارة عن تصميمات لغوية خاصة تتتبع مختلف الأحداث والتسلسلات ، ووفقًا لمعايير محددة ، تحدد قانونية حدوثها.

طرق التحقق الوظيفية

طريقة الاختبارات الموجهة (DTM)

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

التحقق المدفوع بالتغطية ، والتحقق من التشغيل المتري (CDV ، MDV) [17]

مفهوم إنشاء اختبارات تهدف إلى تحقيق "تغطية اختبار" معينة للمواد العضوية. يعتمدون على المقاييس لفهم الاختبارات التي يجب إضافتها إلى خطة التحقق من أجل تحقيق أهداف جاهزية المشروع.
تحتاج إلى استخدام أدوات تحليل التغطية لمعرفة أي شيء آخر لإضافته إلى خطة التحقق. في الواقع ، إذا بدأت في ضبط خطة التحقق في DTM ، بالاعتماد على "تغطية الشفرة" على الأقل ، فيمكننا بالفعل افتراض أن DTM قد تحولت بسلاسة إلى CDV.

التحقق العشوائي المقيد (CRV)

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

1. تنفيذ "التأكيد" في جميع النقاط المهمة في الكود المصدري للـ OB وبيئة الاختبار ؛
2. لتطوير مولدات من التأثيرات والسيناريوهات العشوائية لعملهم ، أي التأثيرات عشوائية ، لكن لها حدود في النطاق (ليس لدينا وقت لتصنيف كل شيء) ، ترتيب الإيداع ، إلخ.

التأكيد القائم على التأكيد [9] (ABV)

التحقق مع البيانات. ربما ، هذه ليست حتى طريقة مستقلة ، ولكن بعض المكونات أو المكونات الأساسية لما سبق.

هناك مشكلة مهمة في ABV وهي كيفية توزيع التأكيدات ، أي منها يتم وضعه بشكل أفضل في الكود المصدري للـ OB ، والتي يجب أن تكون في بيئة الاختبار.

تجدر الإشارة إلى أن لغة Verilog لا تحتوي على تأكيدات في المعيار (يمكن إنشاؤها باستخدام تصميمات اللغة الأساسية ، ولكن هناك حاجة إلى توجيهات لبرنامج المزج بحيث لا تتعامل مع تحويلها). تظهر التأكيدات فقط في معيار SystemVerilog ، وكانت أيضًا في الأصل في VHDL و e.

أقترح عليك أن تتعرف على توصيات المتخصصين ، بما في ذلك Clifford Cummings [12 ، مقالات حول SVA] بشأن توزيع الأعمال على كتاباتهم ، وكذلك المواد الموجودة على ABV على موقع Verification Academy على الويب [13].

مراجع

1. IEEE Std 1800TM-2012. معيار IEEE لـ SystemVerilog - تصميم الأجهزة الموحد ومواصفاته ولغة التحقق
2. كلايف ماكسفيلد. تصميم FPGA. العمارة والأدوات والأساليب. مسار المقاتل الشاب. ISBN 978-5-94120-147-1 (RUS) ، ردمك 0-7506-7604-3 (ENG)
3. أكاديمية التحقق. تغطية كتاب الطبخ. تغطية اختبار برو
4. مايكل كيتنغ ، بيير بريكود. إعادة استخدام دليل المنهجية لتصاميم النظام على رقاقة. اطبع ISBN 1-4020-7141-8 ، الكتاب الإلكتروني ISBN 0-306-47640-1
5. قائمة CAD المرخصة والموزعة بحرية
6. معلمه الرسومات. مثال للإحصائيات حول الحالة الحالية ونطاق التحقق
7. WikiChip. شيبس ويكيبيديا
8. ويكيبيديا. بيانات معممة حول عدد الترانزستورات في IC
9. هاري فوستر ، آدم كرولنيك ، ديفيد لاسي. تأكيد يعتمد على التصميم. طباعة رقم ISBN 1-4020-8027-1 ، كتاب إلكتروني ISBN 1-4020-8028-X
10. ستيوارت ساذرلاند ، سيمون دافيدمان ، بيتر فليك. SystemVerilog للتصميم. طباعة ISBN-10: 0-387-33399-1 ، الكتاب الإلكتروني ISBN-10: 0-387-36495-1
11. كريس سبير ، جريج تومبوش. SystemVerilog للتحقق. طباعة ISBN: 978-1-4614-0714-0 ، الكتاب الإلكتروني ISBN: 978-1-4614-0715-7
12. أمة الله تصميم. أوراق
13. أكاديمية التحقق. بالطبع ABV
14. دولوس. مواد مفيدة على الإنترنت والكتب المرجعية
15. براكاش راشينكار ، بيتر باترسون ، لينا سينغ. نظام على رقاقة التحقق. المنهجية والتقنيات. طباعة ISBN: 0-792-37279-4 ، eBook ISBN: 0-306-46995-2
16. أكاديمية التحقق. المقاييس في شركة نفط الجنوب التحقق
17. دولوس. منهجية التحقق المدفوعة بالتغطية
18. دوغ آموس ، أوستن ليسيا ، رينيه ريختر. دليل منهجية النماذج الأولية المستندة إلى FPGA: أفضل الممارسات في تصميم النماذج الأولية (FPMM). رقم ISBN: 978-1617300042. تحميل مجانا من موقع سينوبسيس