NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration
تقدم هذه الورقة NeuroAbs، وهو إطار عمل عصبي-رمزي يستفيد من النماذج اللغوية الكبيرة (LLMs) لتحديد إشارات RTL والتمثيل الرمزي القائم على أشجار الإعراب المجردة (AST)، مدمجاً مع التحقق من السلامة القائم على حل المشكلات الموجه بالمنطق (SMT) وصقل آلية التحقق من الخطأ عبر التكرار (CEGAR)، وذلك لأتمتة تجريد RTL وتسريع عملية التحقق من خصائص الأجهزة بشكل كبير.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
في العالم الخفي للإلكترونيات الحديثة، تُبنى الرقائق التي تشغل هواتفنا وسياراتنا وحواسيبنا من مليارات المفاتيح الصغيرة. وقبل تصنيع هذه الرقائق، يجب على المهندسين إثبات أنها ستعمل تماماً كما هو مخطط لها، بغض النظر عن التعليمات التي تتلقاها. وتُعرف هذه العملية، المعروفة باسم التحقق الرسمي (formal verification)، بأنها فحص رياضي صارم يضمن خلو التصميم من العيوب الخفية. ومع ذلك، مع ازدياد تعقيد هذه التصاميم، تصبح مهمة فحصها هائلة؛ إذ إن العدد الهائل للحالات التي يمكن أن تدخل فيها الشريحة كبير جداً لدرجة أن أكثر الحواسيب قوة تكافح لاستكشافها جميعاً في وقت معقول. ولحل هذه المشكلة، غالباً ما يستخدم المهندسون تقنية تسمى التجريد (abstraction)، والتي تبسط التصميم المعقد عبر إزالة التفاصيل التي لا تهم لاختبار معين، تماماً مثل النظر إلى خريطة لمدينة تُظهر فقط الطرق الرئيسية اللازمة لرحلة محددة مع تجاهل كل شارع جانبي وزقاق.
لسنوات طويلة، تطلب إنشاء هذه النماذج المبسطة إما عملاً يدوياً مضنياً من قبل خبراء بشريين أو اعتمد على قواعد جامدة ومبرمجة مسبقاً غالباً ما تغفل عن الفروق الدقيقة لتصميم معين. ويقدم نهج جديد يسمى "NeuroAbs" مساراً مختلفاً، حيث يجمع بين قوة التعرف على الأنماط للذكاء الاصطناعي والمنطق الصارم للرياضيات الرسمية. يستخدم هذا الأسلوب النماذج اللغوية الكبيرة — وهي أنظمة ذكاء اصطناعي متطورة مدربة على كميات هائلة من النصوص — لفهم القصد وراء تصميم الأجهزة والخاصية المحددة التي يجب أن يستوفيها. يحدد الذكاء الاصطناعي الأجزاء غير الضرورية من الدائرة بالنسبة للاختبار الحالي ويقترح كيفية تبسيطها. ومع ذلك، ولأن الذكاء الاصطناعي قد يرتكب أخطاء أحياناً أو يقترح تغييرات تكسر المنطق، فإن النظام لا يثق في الذكاء الاصطنا الاصطناعي بشكل أعمى. بدلاً من ذلك، يعمل كإطار عمل عصبي-رمزي (neuro-symbolic framework)، حيث يقترح الذكاء الاصطناعي التغييرات ويقوم محرك رياضي صارم ومنفصل بالتحقق فوراً مما إذا كانت تلك التغييرات آمنة. وإذا كان التبسيط مفرطاً بحيث يخاطر بإخفاء خطأ حقيقي، يقوم النظام تلقائياً بتنقيح النموذج، وتقشير طبقات التبسيط بما يكفي لاستعادة الدقة دون فقدان فوائد السرعة.
اختبر الباحثون وراء "NeuroAbs" إطار عملهم على عدة تصميمات لمعالجات حقيقية ومكونات طرفية، بما في ذلك واجهة اتصال شائعة تُستخدم في العديد من الأجهزة. ووجدوا أن النظام نجح في تحديد فرص لتبسيط المنطق التي فاتتها الطرق التقليدية القائمة على القواعد. فعلى سبيل المثال، عند التحقق من تعليمات معينة في معالج، أدرك الذكاء الاصطناعي أن المنطق الذي يتعامل مع تعليمات أخرى غير ذات صلة يمكن استبداله بأمان بقيمة نائبة عامة. سمح هذا لمحرك التحقق بالتركيز فقط على الأجزاء ذات الصلة من الدائرة. وفي التجارب، سرّع هذا النهج بشكل كبير الوقت المطلوب لإثبات صحة التصميم. وعندما دمج الباحثون "NeuroAbs" مع أدوات التحقق عالية الأداء الموجودة، انخفض الوقت اللازم للوصول إلى برهان رسمي بنسبة تقارب النصف في كثير من الحالات. وحتى عندما لم يكن البرهان الكامل ممكناً ضمن المهلة الزمنية، سمحت النماذج المبسطة للنظام باستكشاف سلوك الدائرة بعمق أكبر بكثير، مما كشف عن أخطاء محتملة كانت ستظل مخفية لولا ذلك.
يعتمد نجاح هذا الأسلوب على التوازن الدقيق بين مرونة الذكاء الاصطناعي ودقة المنطق الرسمي. يحلل النظام أولاً التصميم وسيناريو الاختبار المحدد لتحديد الإشارات الحرجة. ثم يستخدم الذكاء الاصطناعي لإعادة كتابة الكود في تلك المناطق المحددة، مستبدلاً الحسابات المعقدة بقيم مجردة أبسط. ومن الأهمية بمكان أن كل عملية إعادة كتابة تخضع لفحص رياضي صارم لضمان أنها لا تغير السلوك الأساسي للشريحة بطريقة قد تبطل الاختبار. وإذا فشل الفحص، يستخدم النظام حلقة تغذية راجعة لتحديد الجزء المحدد الذي تسبب في المشكلة ويعيد ذلك الجزء إلى شكله الأصلي. تضمن هذه العملية التكرارية أن يكون النموذج النهائي بسيطاً بما يكفي للتحقق منه بسرعة ودقيقاً بما يكفي للوثوق به. وتظهر النتائج أن هذا النهج الهجين يمكنه التعامل مع أنواع متنوعة من منطق الأجهزة، من العمليات الحسابية البسيطة إلى هياكل التفرع المعقدة، مما يجعله أداة قوية للجيل القادم من تصميم الرقائق.
من خلال أتمتة إنشاء هذه النماذج المبسطة، يعالج "NeuroAbs" عقبة رئيسية في هندسة الأجهزة. سابقاً، كان قرار ما يجب تبسيطه وكيفية القيام بذلك يعتمد بشكل كبير على الحدس البشري أو القواعد الثابتة التي لا تستطيع التكيف مع كل تحدٍ فريد للتصميم. يوضح هذا الإطار الجديد أن الذكاء الاصطناعي يمكن توجيهه بفعالية لأداء هذه المهام، بشرط أن يكون مرتكزاً على نظام يتحقق من كل خطوة. وتشير النتيات إلى أن مستقبل التحقق من الأجهزة قد يكمن في مثل هذه الأنظمة التعاونية، حيث تتولى الآلات القيام بالعمل الشاق المتمثل في التعرف على الأنماط والاقتراح، بينما يضمن الانضباط الرياضي سلامة وصحة المنتج النهائي. ومع استمرار نمو تعقيد تصميمات الرقائق، تقدم أدوات مثل "NeuroAbs" طريقة واعدة لمواكبة هذا النمو، مما يضمن أن الأجهزة التي نعتمد عليها مبنية على أساس من الحقيقة المتحقق منها.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.