Coverage-Driven RTL Assertion Generation with Formal Exploration and Neuro-Symbolic Refinement

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

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

بمجرد حصول النظام على هذه السلوكيات التي يصعب العثور عليها، ينتقل إلى مرحلة التوليد. فهو يستخدم تقنية تسمى "التخليق الموجه نحو بناء الجملة" (syntax-guided synthesis) لإنشاء قواعد سلامة أولية بناءً على البيانات المرصودة. ومع ذلك، أدرك الباحثون أن هذه المرحلة الأولى نادراً ما تكون مثالية. ولإصلاح ذلك، قدموا حلقة تنقيح تعمل كمحرر صارم. يقيس النظام مدى قدرة مجموعة القواعد الحالية على اكتشاف التغييرات في التصميم عن طريق حقن أخطاء صغيرة متعمدة، تُعرف باسم "الموتانت" (mutants)، في الكود. وإذا فشلت القواعد في رصد "الموتانت"، يعرف النظام بالضبط أي سلوك ظل دون فحص. بعد ذلك، يستعين بنموذج لغوي كبير لاقتراح قاعدة جديدة مصممة خصيصاً لتغطية تلك الفجوة. وإذا كانت القاعدة المقترحة معيبة منطقياً، فإن نموذجاً لغوياً ثانياً لا يتجاهلها؛ بل يحلل الخطأ ويبني مجموعة متخصصة من التعليمات، أو "القواعد النحوية" (grammar)، لتوجيه محلل رمزي لإصلاح القاعدة. وهذا يخلق دورة يقترح فيها النظام، ويفحص، ويصلح التأكيدات حتى تصبح وفيرة وقوية.

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

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