من المواصفة إلى الخصائص الرسمية: الذكاء الاصطناعي يسرّع التحقق من تصميم الرقائق لكن لا يلغي المهندس

تقترب نماذج اللغة الكبيرة من تنفيذ واحدة من أكثر المهام إزعاجاً في التحقق من تصميم الرقائق: تحويل المواصفات المكتوبة باللغة الطبيعية إلى مجموعة من الخصائص الرسمية التي يمكن استخدامها للحكم على صحة تنفيذ RTL. وتوضح مقابلات أجراها Brian Bailey في Semiconductor Engineering أن الأدوات الحالية تستطيع إنتاج مسودة أولية مفيدة، لكنها لا تزال بعيدة عن إنشاء مجموعة مكتملة يمكن اعتمادها من دون مراجعة هندسية مكثفة.

تكمن أهمية هذا التطور في أن كتابة الخصائص تمثل منذ سنوات عنق زجاجة في التحقق الرسمي. وتُستخدم خصائص SystemVerilog، التي تُعرف عند إدراجها في بيئة التحقق باسم assertions، لوصف العلاقات المنطقية والزمنية بين الإشارات، مثل سلوك إعادة الضبط، والمصافحات، وشروط one-hot، وفحوص السلامة الأساسية. وعندما تكون هذه الخصائص مكتملة ودقيقة، يمكن استخدامها لمقارنة سلوك تنفيذ RTL بالمواصفة، من دون الارتباط بطريقة بناء التصميم.

ما الذي تستطيع الأدوات فعله اليوم؟

يمكن لأداة تعتمد على نموذج لغة كبير قراءة وثيقة مواصفات أو معيار بروتوكول أو حتى تعليقات داخل RTL، ثم اقتراح مسودة من خصائص SVA. ويقول Ashish Darbari، الرئيس التنفيذي لشركة Axiomise، إن هذا الاستخدام يكون أكثر قابلية للتطبيق عندما تستند المواصفات إلى معايير مستقرة لا تتغير كثيراً. وفي هذه الحالة، تخفف الأداة الجزء المتكرر من كتابة الشيفرة الأولية، بدلاً من أن تتولى عملية التحقق كاملة.

وتحاول بعض الأساليب تحسين دقة النماذج عبر إنشاء knowledge graph، أي رسم بياني للمعرفة يخزن الكيانات والعلاقات بينها. وقد تتضمن العقد إشارة أو وحدة أو متطلباً أو منفذاً، بينما تصف الحواف علاقات مثل «يقود» و«يعيد الضبط» و«يستجيب لـ». وبدلاً من استرجاع مقاطع نصية تبدو مرتبطة بالطلب، يمكن للنظام الرجوع إلى حقائق وروابط محددة، ما يقلل احتمال اختراع اسم إشارة أو إساءة فهم علاقة بين مكونات التصميم. ويشير المصدر إلى بحث بعنوان RAG-SVA in the Landscape of LLM-Based Assertion Generation لـ Cohen وChibani في هذا السياق.

المشكلة تبدأ قبل الذكاء الاصطناعي

لا تستطيع الأداة استخراج ما لم يُكتب أو يُحسم أصلاً. ويقول Ravindra Aneja، مدير هندسة التطبيقات في Synopsys، إن المواصفة المثالية لم تكن أمراً متاحاً خلال العقود الثلاثة الماضية؛ فكثيراً ما يبدأ التطوير قبل اكتمال التوثيق، وقد لا توجد مواصفة كاملة في بعض المشاريع، خصوصاً في التصاميم المشتقة أو عندما تتغير المتطلبات أثناء العمل.

هذه المشكلة لا تتعلق بالصياغة فقط، بل بإدارة التغيير. فقد يضيف فريق التسويق ميزة جديدة أو يعدل متطلباً قائماً، وعلى فريق التصميم والتحقق تحديد أثر ذلك التغيير. ويرى Abhi Kolpekwa، نائب الرئيس الأول والمدير العام في Siemens EDA، أن تحويل المواصفة إلى خصائص يحتاج إلى «ذكاء سياقي» يتابع تاريخ التغييرات وسياقها، لا إلى وكيل يولد نصاً جديداً في كل مرة.

خطر الثقة الزائفة

أكبر قيود النهج الحالي أن الخاصية قد تكون صحيحة نحوياً، فتُترجم وتنجح أدوات التحقق في إثباتها، لكنها لا تختبر السلوك المقصود فعلاً. ويحذر Darbari من أن خاصية ضعيفة أو vacuous قد تنجح بسهولة لأنها تسمح بسلوكيات كثيرة، أو لأنها تستخدم الإشارة الخطأ، أو لأنها تحتوي على شرط سابق مفقود أو مفرط التقييد. لذلك فإن «الإثبات الأخضر» لا يعني أن التصميم خالٍ من الأخطاء؛ فالدليل لا يكون أقوى من الخاصية التي جرى إثباتها.

ويضيف المصدر أن النماذج تميل إلى أداء أفضل في التغطية البنيوية والنحوية من فهم النية المعمارية وسبب وجود القاعدة. ولهذا قد تتحول قراءة النموذج غير الدقيقة للمواصفة إلى قطعة تبدو رسمية وصارمة، بينما تخفي فجوة في المتطلبات. وإذا انتقلت هذه الفجوة إلى أعمال مثل FMEDA أو ملفات السلامة أو أدلة الاعتماد المرتبطة بـ ISO 26262 وISO 21434، فقد يمتد أثرها إلى ما هو أبعد من مشروع التحقق الأصلي.

كما تبرز مسألة فصل التصميم عن التحقق. تشير Kaye Mao، قائدة تصميم المنتجات في Normal Computing، إلى ضرورة تقييد ما يمكن للوكلاء الوصول إليه من مواد المشروع، لأن السماح للوكيل باستخدام التصميم نفسه لتوليد حالات الاختبار قد يقوض استقلالية عملية التحقق.

ما الذي يتغير عملياً؟

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

من منظور certi.news، التغيير الحقيقي ليس استبدال مهندس التحقق، بل نقل مركز الثقل من كتابة الخصائص إلى تقييمها وتتبع مصدرها. ويوصي Darbari بالتعامل مع الخصائص المولدة باعتبارها مسودات لا مخرجات معتمدة، وبإنشاء بوابة مراجعة قبل إدخالها في regression suite. كما ينبغي تسجيل مصدر كل خاصية: فقرة المواصفة أو المتطلب أو عنصر RTL الذي أنتجها، حتى يتمكن المهندس من التحقق من المطابقة.

قد يخفض هذا النهج حاجز الدخول أمام مهندسي التحقق الراغبين في استخدام formal verification، كما يقول Yaron Ilani، مهندس حلول التحقق في Normal Computing. لكن ذلك لا يحسم سؤال العائد على الاستثمار. فـ Kaye Mao ترى أن وقت التحقق من مخرجات الوكيل يجب احتسابه ضمن الكلفة، بينما يشير Arvind Srinivasan، رئيس مهندسي الحلول في Normal Computing، إلى أن التوسع لا يتعلق بالحساب وحده، بل باكتمال البيانات وكلفة المراجعة البشرية.

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