التحقق الوظيفي
التحقق الوظيفي هو مهمة التأكد من مطابقة تصميم المنطق للمواصفات. [ 1 ] يسعى التحقق الوظيفي إلى الإجابة عن السؤال: "هل يؤدي هذا التصميم المقترح الغرض المرجو منه؟" [ 2 ] يُعد هذا الأمر معقدًا ويستغرق الجزء الأكبر من الوقت والجهد (حتى 70% من وقت التصميم والتطوير) [ 1 ] في معظم مشاريع تصميم الأنظمة الإلكترونية الكبيرة. يُعد التحقق الوظيفي جزءًا من عملية التحقق من التصميم الشاملة ، والتي، بالإضافة إلى التحقق الوظيفي، تأخذ في الاعتبار الجوانب غير الوظيفية مثل التوقيت والتخطيط والطاقة. [ 3 ]
خلفية
على الرغم من أن عدد الترانزستورات ازداد بشكل كبير وفقًا لقانون مور ، إلا أن عدد المهندسين والوقت اللازمين لتصميمها ازدادا بشكل خطي فقط . ومع ازدياد تعقيد الترانزستورات، ازداد أيضًا عدد أخطاء البرمجة. وتنتج معظم أخطاء البرمجة المنطقية عن الإهمال في البرمجة (12.7%)، وسوء التواصل (11.4%)، وتحديات البنية الدقيقة (9.3%). [ 1 ] ولذلك، تم تطوير أدوات أتمتة تصميم الإلكترونيات (EDA) لمواكبة تعقيد تصميم الترانزستورات. وقد تم إدخال لغات برمجة مثل Verilog و VHDL بالتزامن مع أدوات EDA. [ 1 ]
يُعد التحقق الوظيفي صعبًا للغاية نظرًا للعدد الهائل من حالات الاختبار المحتملة حتى في التصميمات البسيطة. غالبًا ما يكون هناك أكثر منيتطلب التحقق الشامل من تصميم ما 1080 اختبارًا محتملاً، وهو عدد يستحيل تحقيقه خلال العمر الافتراضي. هذا الجهد يعادل التحقق من البرامج ، وهو من المسائل الصعبة حسابيًا (NP-hard ) أو حتى أصعب، ولم يُعثر على حلٍّ فعال في جميع الحالات.
عملية واستراتيجية التحقق
خطة التحقق
يسترشد مشروع التحقق الوظيفي بخطة تحقق. تُعد هذه الخطة وثيقة أساسية تُشكل مخططًا تفصيليًا للمشروع بأكمله. وهي وثيقة قابلة للتحديث، تُنشأ في المراحل الأولى من دورة التصميم، وتُعتبر بالغة الأهمية لتحديد نطاق المشروع وتتبع التقدم المحرز. تتضمن الخطة عادةً ما يلي: [ 4 ]
- نطاق التحقق: قائمة بميزات التصميم والوظائف التي تحتاج إلى التحقق منها.
- المنهجية: التقنيات (مثل المحاكاة، والتقليد، والمنهجيات الرسمية) والمنهجيات المعيارية (مثل UVM ) التي سيتم استخدامها.
- الموارد: فريق الهندسة، وأدوات تصميم الدوائر الإلكترونية ، والبنية التحتية الحاسوبية المطلوبة.
- معايير النجاح: أهداف تغطية محددة يجب تحقيقها لاعتبار عملية التحقق مكتملة.
مقاييس التغطية
لقياس مدى اكتمال عملية التحقق، يعتمد المهندسون على مقاييس التغطية . [ 4 ] تُعرف عملية تحقيق أهداف التغطية المحددة مسبقًا باسم "إغلاق التغطية". وهناك نوعان رئيسيان من التغطية:
- تغطية الكود: يقيس هذا المقياس مدى شمولية اختبار كود لغة وصف الأجهزة (HDL). ويتضمن مقاييس مثل تغطية العبارات، وتغطية الفروع، وتغطية التبديل.
- التغطية الوظيفية: يقيس هذا ما إذا كانت الوظائف المقصودة، كما هو موضح في خطة التحقق، قد تم اختبارها. يحدد المهندسون سيناريوهات محددة أو قيم بيانات ذات أهمية، وتتتبع أداة التحقق ما إذا تم تطبيق هذه الحالات.
مستويات التجريد في التحقق
لا يُعد التحقق الوظيفي مهمةً واحدةً متجانسة، بل هو عملية مستمرة تُطبَّق على مستويات مختلفة من تجريد التصميم أثناء تطوير الشريحة. هذا النهج الهرمي ضروري لإدارة التعقيد الهائل لأنظمة SoC الحديثة. [ 5 ] [ 4 ]
- التحقق على مستوى الوحدة/الكتلة: هذا هو المستوى الأكثر دقة، حيث يتم اختبار وحدات التصميم الفردية (مثل وحدة FIFO واحدة، أو وحدة حساب ومنطق، أو وحدة فك تشفير) بشكل منفصل. الهدف هو التحقق بدقة من وظائف جزء صغير من التصميم قبل دمجه في نظام أكبر. [ 5 ]
- التحقق على مستوى النظام الفرعي/الملكية الفكرية: في هذه المرحلة، تُدمج وحدات متعددة لتشكيل وحدة وظيفية أكبر، تُعرف غالبًا بالنظام الفرعي أو نواة الملكية الفكرية (مثل وحدة تحكم ذاكرة كاملة أو نواة معالج). يركز التحقق على هذا المستوى على الوظائف المُدمجة والتفاعلات بين الوحدات المُدمجة. من الاستراتيجيات الشائعة في هذه المرحلة استخدام النماذج السلوكية، وهي تمثيلات وظيفية عالية المستوى للوحدة. تُحاكي هذه النماذج بشكل أسرع من كود RTL المُفصّل، وتسمح ببدء التحقق قبل اكتمال التصميم النهائي، مما يُساعد على صياغة مواصفات الواجهة واكتشاف الأخطاء مبكرًا. [ 4 ]
- التحقق على مستوى الشريحة/النظام على رقاقة: بمجرد توفر جميع الأنظمة الفرعية ووحدات الملكية الفكرية، يتم دمجها لتشكيل النظام الكامل على رقاقة (SoC). يركز التحقق الوظيفي على مستوى الرقاقة على التحقق من صحة الاتصال والتفاعلات بين جميع هذه الوحدات الرئيسية. تُجرى عمليات محاكاة على مستوى النظام لإثبات واجهات الربط بين الدوائر المتكاملة الخاصة بالتطبيقات (ASICs) والتحقق من حالات أخطاء البروتوكول المعقدة. [ 4 ]
- التحقق على مستوى النظام: يُمثل هذا أعلى مستوى من التجريد، حيث يتم اختبار وظائف الشريحة المُتحقق منها ضمن سياق نظام كامل، يشمل غالبًا شرائح أخرى وأجهزة طرفية وبرمجيات. تُعد محاكاة الأجهزة تقنية بالغة الأهمية في هذه المرحلة، إذ تسمح سرعتها العالية بتشغيل برمجيات حقيقية، مثل برامج تشغيل الأجهزة أو حتى تشغيل نظام تشغيل كامل على التصميم. يوفر هذا "تنوعًا كبيرًا في المحفزات" يصعب تكراره في المحاكاة، وهو فعال للغاية في اكتشاف الأخطاء على مستوى النظام. [ 4 ]
منهجيات التحقق
نظراً لاستحالة إجراء اختبار شامل، يتم استخدام مزيج من الأساليب لمعالجة مشكلة التحقق. وتُصنف هذه الأساليب بشكل عام إلى أساليب ديناميكية، وثابتة، وهجينة.
التحقق الديناميكي (القائم على المحاكاة)
يتضمن التحقق الديناميكي تنفيذ نموذج التصميم باستخدام مجموعة معينة من محفزات الإدخال والتحقق من مخرجاته للتأكد من صحة السلوك. وهذا هو النهج الأكثر استخدامًا على نطاق واسع. [ 1 ]
- محاكاة المنطق : تُعدّ هذه التقنية أساس التحقق الوظيفي، حيث يتم محاكاة نموذج برمجي للتصميم. ويتم إنشاء بيئة اختبار لتوليد المحفزات، وإدخالها في التصميم، ومراقبة المخرجات، والتحقق من صحتها.
- المحاكاة والنمذجة الأولية باستخدام FPGA: تعمل هذه التقنيات المدعومة بالأجهزة على تحويل التصميم إلى منصة أجهزة قابلة لإعادة التكوين (محاكي أو لوحة FPGA ). وهي تعمل بسرعة تفوق سرعة المحاكاة بأضعاف مضاعفة، مما يسمح بإجراء اختبارات أكثر شمولاً باستخدام برامج حقيقية، مثل تشغيل نظام التشغيل. [ 5 ]
- تسريع المحاكاة: يستخدم هذا أجهزة ذات أغراض خاصة لتسريع أجزاء من محاكاة المنطق.
تُعد منصة اختبار المحاكاة الحديثة بيئة برمجية معقدة. وتشمل المكونات الرئيسية مولدًا لإنشاء المحفزات (غالبًا باستخدام تقنيات عشوائية مقيدة)، وبرنامج تشغيل لترجمة المحفزات إلى إشارات على مستوى الدبوس، وشاشة مراقبة لمراقبة المخرجات، ومدقق (أو لوحة نتائج) للتحقق من صحة النتائج مقابل نموذج مرجعي.
التحقق الثابت
يقوم التحقق الثابت بتحليل التصميم دون تنفيذه باستخدام متجهات الاختبار: [ 1 ]
- التحقق الرسمي : يستخدم هذا الأسلوب طرقًا رياضية لإثبات أو دحض استيفاء التصميم لمتطلبات رسمية محددة (خصائص) دون الحاجة إلى متجهات اختبار. يمكنه إثبات خلو التصميم من بعض الأخطاء، ولكنه محدود بمشكلة تضخم فضاء الحالة.
- التدقيق اللغوي : يتضمن ذلك استخدام إصدارات خاصة بلغة وصف الأجهزة (HDL) من أدوات التدقيق اللغوي للتحقق من انتهاكات أسلوب البرمجة الشائعة، وأخطاء بناء الجملة، والهياكل التي يحتمل أن تكون إشكالية في الكود.
التقنيات الهجينة
تجمع هذه الأساليب بين تقنيات تحقق متعددة لتحقيق نتائج أفضل. على سبيل المثال، يمكن استخدام الأساليب الرسمية لإنشاء اختبارات محددة تستهدف الحالات الشاذة التي يصعب الوصول إليها، والتي يتم تشغيلها بعد ذلك في بيئة محاكاة أكثر قابلية للتوسع. [ 6 ]
مكونات البيئات المحاكاة
تتكون بيئة المحاكاة عادةً من عدة أنواع من المكونات:
- يُنشئ المُولِّد متجهات إدخال تُستخدم للبحث عن حالات الشذوذ الموجودة بين الهدف (المواصفات) والتنفيذ (كود لغة وصف الأجهزة). يستخدم هذا النوع من المُولِّدات مُحلِّل SAT من نوع NP-complete ، والذي قد يكون مُكلفًا حسابيًا. تشمل الأنواع الأخرى من المُولِّدات المتجهات المُنشأة يدويًا والمُولِّدات القائمة على الرسوم البيانية (GBMs). تُنشئ المُولِّدات الحديثة مُحفزات عشوائية مُوجَّهة وعشوائية مُوجَّهة إحصائيًا للتحقق من أجزاء عشوائية من التصميم. تُعد العشوائية مهمة لتحقيق توزيع عالٍ على المساحة الهائلة لمُحفزات الإدخال المُتاحة. ولتحقيق هذه الغاية، يُقلِّل مُستخدمو هذه المُولِّدات عمدًا من متطلبات الاختبارات المُولَّدة. ويتمثل دور المُولِّد في ملء هذه الفجوة عشوائيًا. تسمح هذه الآلية للمُولِّد بإنشاء مُدخلات تكشف عن أخطاء لا يبحث عنها المُستخدم مُباشرةً. كما تُحَيِّز المُولِّدات المُحفزات نحو حالات التصميم الشاذة لزيادة الضغط على المنطق. يخدم التحيُّز والعشوائية أهدافًا مُختلفة، وهناك مُفاضلات بينهما، لذلك تمتلك المُولِّدات المُختلفة مزيجًا مُختلفًا من هذه الخصائص. بما أن مدخلات التصميم يجب أن تكون صحيحة، ويجب الحفاظ على العديد من الأهداف (مثل التحيز)، فإن العديد من المولدات تستخدم تقنية حل مشكلة إرضاء القيود (CSP) لتلبية متطلبات الاختبار المعقدة. يتم نمذجة صحة مدخلات التصميم ومجموعة أدوات التحيز. تستخدم المولدات القائمة على النموذج هذا النموذج لإنتاج المحفزات الصحيحة للتصميم المستهدف.
- تقوم برامج التشغيل بترجمة المحفزات التي ينتجها المولد إلى المدخلات الفعلية للتصميم قيد التحقق. تُنشئ المولدات مدخلات على مستوى عالٍ من التجريد، أي كمعاملات أو لغة تجميع . ثم تقوم برامج التشغيل بتحويل هذه المدخلات إلى مدخلات تصميم فعلية كما هو محدد في مواصفات واجهة التصميم.
- يُنتج برنامج المحاكاة مخرجات التصميم بناءً على حالته الراهنة (حالة القلابات) والمدخلات المُدخلة. ويحتوي البرنامج على وصف لقائمة توصيلات التصميم، والذي يُنشأ عن طريق توليف لغة وصف الأجهزة (HDL) إلى قائمة توصيلات على مستوى البوابات المنطقية.
- يقوم جهاز المراقبة بتحويل حالة التصميم ومخرجاته إلى مستوى تجريد المعاملات بحيث يمكن تخزينها في قاعدة بيانات "لوحات النتائج" ليتم فحصها لاحقًا.
- يتحقق المدقق من صحة محتويات لوحات النتائج. في بعض الحالات، يُنشئ المُولِّد نتائج متوقعة بالإضافة إلى المدخلات. في هذه الحالات، يجب على المدقق التحقق من تطابق النتائج الفعلية مع النتائج المتوقعة.
- يتولى مدير التحكيم إدارة جميع المكونات المذكورة أعلاه معًا.
التحقق من صحة مجالات التصميم المتخصصة
التحقق من انخفاض استهلاك الطاقة
تستخدم أنظمة SoC الحديثة تقنيات متطورة لإدارة الطاقة بهدف ترشيد استهلاكها، مثل التحكم في الطاقة ونطاقات الجهد المتعددة. ويُعدّ التحقق من الأداء الصحيح لهذه الميزات الموفرة للطاقة مهمةً رئيسيةً تتضمن ضمان عزل حالات المنطق وحفظها واستعادتها بشكل صحيح أثناء عمليات إيقاف التشغيل وإعادة التشغيل. ويتم ذلك عادةً من خلال تحديد الغرض من الطاقة بتنسيق موحد، مثل تنسيق الطاقة الموحد (UPF)، الذي يوجه أدوات التحقق. [ 4 ]
التحقق من عبور نطاق الساعة (CDC)
غالبًا ما تحتوي أنظمة SoC المعقدة على نطاقات تردد متعددة تعمل بشكل غير متزامن. ويُعدّ نقل البيانات بشكل موثوق بين هذه النطاقات مصدرًا شائعًا لأخطاء الأجهزة الدقيقة. يركز التحقق من نطاقات التردد (CDC) على تحديد وضمان صحة دوائر التزامن المستخدمة عند هذه الحدود غير المتزامنة لمنع مشكلات مثل عدم الاستقرار وتلف البيانات . وتُعدّ أدوات التحليل الثابت المتخصصة وأدوات التحقق الرسمي ضرورية لإجراء تحقق شامل من نطاقات التردد (CDC). [ 4 ]
الاتجاهات الناشئة
التعلم الآلي في التحقق الوظيفي
يُستخدم التعلّم الآلي في جوانب مختلفة من التحقق الوظيفي لتحسين الكفاءة والفعالية. تستطيع نماذج التعلّم الآلي تحليل مجموعات البيانات الضخمة الناتجة عن عملية التحقق لتحديد الأنماط والتنبؤات. تشمل التطبيقات الرئيسية ما يلي: [ 7 ]
- توليد الاختبارات الآلية : توجيه عملية توليد المحفزات لإنشاء اختبارات من المرجح أن تختبر الأجزاء غير المُتحقق منها من التصميم.
- التنبؤ بالأخطاء وتحديد موقعها: تحليل بيانات التصميم للتنبؤ بالوحدات المعرضة للأخطاء أو للمساعدة في تحديد السبب الجذري للفشل.
- تحليل التغطية: تحسين عملية تحقيق أهداف التغطية من خلال التنبؤ بالاختبارات الأكثر فعالية في سد ثغرات التغطية المتبقية، وبالتالي تقليل طول اختبارات الانحدار.
التحقق من أمان الأجهزة
مع ازدياد اندماج الأنظمة الإلكترونية في التطبيقات الحيوية (مثل الذكاء الاصطناعي والسيارات)، أصبح ضمان أمن الأجهزة جزءًا أساسيًا من عملية التحقق. ويجري الآن تكييف هذه العملية للكشف عن الثغرات الأمنية بالإضافة إلى الأخطاء الوظيفية. ويشمل ذلك اختبار التهديدات مثل: [ 8 ]
- برامج التجسس على الأجهزة : هي تعديلات خبيثة ومخفية على التصميم، قادرة على إنشاء ثغرة أمنية أو التسبب في تعطل النظام في ظروف معينة. يجب أن تسعى عمليات التحقق إلى كشف هذه الوظائف غير المقصودة والضارة.
- هجمات القنوات الجانبية : هي ثغرات أمنية تسمح بتسريب المعلومات عبر خصائص فيزيائية مثل استهلاك الطاقة أو الانبعاثات الكهرومغناطيسية. وبينما كانت هذه الهجمات تُعتبر تقليديًا مشكلة ما بعد تصنيع الرقاقة، يُستخدم الآن التحقق قبل تصنيعها لتحليل التصاميم بحثًا عن مدى قابليتها لمثل هذه الهجمات.
انظر أيضاً
مراجع
- 1 2 3 4 5 6 مولينا، أ؛ كاديناس، أ (8 سبتمبر 2006). " التحقق الوظيفي: المناهج والتحديات" . البحوث التطبيقية لأمريكا اللاتينية . 37. ISSN 0327-0793 . مؤرشف من الأصل في 16 أكتوبر 2022. تم الاسترجاع في 12 أكتوبر 2022 .
- ↑ رضائيان، بنافشه؛ رودريغز، د. يواكيم؛ راث، ألكسندر و. "منهجية المحاكاة والتحقق من الدوائر المتكاملة للسيارات ذات الإشارات المختلطة" . جامعة لوند، قسم الهندسة الكهربائية وتكنولوجيا المعلومات .
- ↑ ستراود، تشارلز إي؛ تشانغ، ياو تشانغ (2009). "الفصل 1 - مقدمة" . التحقق من التصميم . ص 1-38 . doi : 10.1016/B978-0-12-374364-0.50008-4 . ISBN 978-0-12-374364-0أُرشف من المصدر الأصلي بتاريخ ١٢ أكتوبر ٢٠٢٢. تم الاطلاع عليه بتاريخ ١١ أكتوبر ٢٠٢٢ .
- 1 2 3 4 5 6 7 8 ميهتا، أشوك ب. (2018). التحقق من التصميم الوظيفي لـ ASIC/SoC . doi : 10.1007/978-3-319-59418-7 . ISBN 978-3-319-59417-0.
- 1 2 3 إيفانز، أدريان؛ سيلبرت، آلان؛ فركوفنيك، غاري؛ براون، ثين؛ دوفريسن، ماريو؛ هول، جيفري؛ هو، تونغ؛ ليو، يينغ (1998-05-01). "التحقق الوظيفي من الدوائر المتكاملة الخاصة بالتطبيقات الكبيرة" . وقائع المؤتمر السنوي الخامس والثلاثين حول أتمتة التصميم - مؤتمر DAC '98 . نيويورك، نيويورك، الولايات المتحدة الأمريكية: رابطة آلات الحوسبة. الصفحات 650-655 . doi : 10.1145/277044.277210 . ISBN 978-0-89791-964-7.
- ↑ بهادرا، جايانتا؛ عبادير، مجدي س.؛ وانغ، لي-سي.؛ راي، سانديب (مارس 2007). "دراسة استقصائية للتقنيات الهجينة للتحقق الوظيفي". مجلة IEEE لتصميم واختبار الحواسيب . 24 (2): 112-122 . رمز Bibcode : 2007IDTC...24..112B . doi : 10.1109/MDT.2007.30 . ISSN 1558-1918 .
- ↑ أ.، إسماعيل، خالد؛ غني، محمد عبد العبد (يناير 2021). "دراسة استقصائية حول خوارزميات التعلم الآلي التي تُحسّن عملية التحقق الوظيفي" . الإلكترونيات . 10 (21): 2688. doi : 10.3390/electronics10212688 . ISSN 2079-9292 .
{{cite journal}}: صيانة CS1: أسماء متعددة: قائمة المؤلفين ( رابط ) - ↑ أو، إيما؛ باكوود، جاك؛ أويستين، مايكل. "الاتجاهات المستقبلية في التحقق من تصميم الدوائر المتكاملة الخاصة بالتطبيقات: تقارب التعلم الآلي وأمن الأجهزة لأنظمة الذكاء الاصطناعي" . researchgate.net .
- التحقق من الدوائر الإلكترونية
- المنطق في علوم الحاسوب
