ثمانية براهين شكلية خضراء أصبحت خمسة قابلة للاعتماد حين دققتُ تأكيدات SystemVerilog
شاهدتُ لوحة تحقق شكلي تركيبية تقدم تقريرًا يفيد بـ 8/8 PROVEN، ثم رأيتُ تدقيقها الداخلي يعتمد فقط 5/8 بوصفها TRUSTWORTHY. هذا التحول المعاكس هو المنطلق الأساسي لـ Proof Firewall، عرضنا التوضيحي القابل للتشغيل لحوكمة تأكيدات SystemVerilog (SVA) المولّدة بالذكاء الاصطناعي، وقد غيّر المعيار الذي أريد أن يستوفيه أي برهان أخضر قبل أن يصل إلى مراجعة الاعتماد النهائي للتصنيع (tape-out sign-off).
لقد بنيتُ اللوحة بخصائص مُعدّة ضمن بيئة اختبارية تحاكي «خصائص ألّفتها نماذج لغة كبيرة» على وحدة تحكيم تركيبية، وخط أنابيب ثنائي المراحل، ونقطة عبور نطاقات الساعة (CDC)، لأن الحالة غير المريحة تستحق أن تكون مرئية. فقد يبدو التأكيد محترمًا تمامًا في سجل الخصائص، ويمكن لمحرك التحقق الشكلي أن يُرجع نتيجة خضراء، ومع ذلك قد لا يكون التضمين المنطقي قد أدى أي عمل على الإطلاق، أو قد يظل ناجحًا حتى بعد كسر سلوك التصميم المعني. كنتُ أتعامل مع كلمة PROVEN بوصفها نقطة وصول نهائية. لكن بناء هذا العرض التوضيحي أجبرني على التعامل معها كبداية لمراجعة الأدلة.
إن العرض التوضيحي لـ Proof Firewall لا يستبدل محرك التحقق الشكلي، ولا يستوعب كود RTL حقيقيًا، ولا يستدعي نموذج لغة كبيرًا مباشرًا في مساره الافتراضي. إنه أصغر حجمًا وأكثر قابلية للفحص عن عمد: إذ يقيّم مدقق نموذج للحالات الصريحة مكتوب بلغة Python بالكامل تمثيلًا وسيطًا (IR) لنظام انتقال تركيبي، ثم تفحص بوابة الحوكمة إمكانية الوصول إلى المقدمة (antecedent reachability)، وإهلاك الطفرات (mutation kills)، ومخروط التأثير (COI). والناتج إما مبرر لتقديم شهادة عرض توضيحي موقّعة أو سبب لتعليق النتيجة للمراجعة البشرية.
بدأتُ بالنوع الخاطئ من اللون الأخضر
أتذكر أن الإصدار الأول من اللوحة كان يبعث على الاطمئنان تحديدًا لأنه كان شديد النقاء. ثماني خصائص، وثماني شارات خضراء، وعرض للتدفق المجرد جعل العمل يبدو مكتملًا. كان حدسي الأولي هو جعل العرض التوضيحي يفسر تلك النتيجة النقية بشكل أفضل. وظننت أن المهمة الهندسية كانت مجرد عرض: إبراز البراهين، وعرض التأكيدات، وجعل لوحة التحكم أسهل في الوثوق بها. كانت النتيجة الخضراء حقيقية، لكنها كانت تجيب عن سؤال أصغر بكثير من السؤال الذي يتعين على المراجع طرحه.
ثم أخضعتُ الخصائص الثماني نفسها للفحوصات التي تتطلبها محادثة الاعتماد الفعلي. هل أصبحت المقدمة (antecedent) صحيحة في أي وقت؟ هل كان التأكيد سيعترض لو غُيِّر جزء ذو صلة من التصميم؟ هل يفرض قيودًا على مخروط تأثير (COI) ذي مغزى؟ تلك الأسئلة أقل إرضاءً للغرور من الشارة الخضراء لأنها تسأل عما استحقّه البرهان بالفعل، وليس مجرد ما أرجعه الحلاّل.
كان عليّ التخلي عن التأطير الأول للبناء. فالشاشة التي أظهرت 8/8 PROVEN كانت عرضًا دقيقًا لخط الأساس في التدفق المجرد، لكنها كانت غير مكتملة كقصة اعتماد نهائي. وبعد تدقيق جدار الحماية، أصبح لدى اللوحة التركيبية الثابتة نفسها خمس نتائج TRUSTWORTHY، ونتيجة واحدة VACUOUS، ونتيجتان WEAK. ولم يُعَد تصنيف النتائج الثلاث المتبقية كنجاح، بل جرى تعليقها مع الأدلة التي توضح السبب. تصنيف البرهان وقرار الاعتماد هما مخرجان مختلفان تمامًا.
لقد اخترتُ كلمة «الحوكمة» بعناية هنا. فالفحوصات الحتمية في العرض التوضيحي تجعل قرار الاعتماد قابلاً للمراجعة. قد يقترح مؤلف SVA اختياري تأكيدًا معينًا، لكن مدقق النموذج وبوابة السياسات هما من يحددان الحكم النهائي. الوكلاء يقدمون المشورة، والشيفرة هي التي تقرر. كنتُ أحاول جعل البوابة مقروءة وواضحة بما يكفي بحيث تكون النتيجة السلبية مفيدة بدلاً من أن تكون مجرد أمر محرج. فالنتيجة المحجوبة تحتاج إلى سبب يمكن لمهندس التحقق فحصه، وإعادة إنتاجه، والاعتراض عليه.
الخاصية ARB3 جعلت المشكلة مستحيلة التجاهل
وجدتُ أوضح إخفاق في ARB3، وهي خاصية وحدة التحكيم التركيبية assert (g0 && g1) |-> (turn == 0). في التدفق المجرد، تظهر بلون أخضر. ولكن عندما فتحتُ شكلها الموجي وأدلة إمكانية الوصول، تبيّن أن المقدمة g0 && g1 كانت مستحيلة الوصول في وحدة التحكيم التركيبية تلك. وبالتالي، لم يُثبَت التضمين إلا بالمعنى الضيق المتمثل في أنه لم يُضطر أبدًا إلى الاستجابة للحالة التي يصفها. المقدمة لا تنطلق أبدًا.
من السهل قول هذا التمييز ولكن من الصعب استحضاره عندما تكون لوحة التحقق مليئة باللون الأخضر. قرأتُ التضمين في البداية بوصفه ادعاءً حول سلوك التحكيم. غير أن نتيجة إمكانية الوصول غيّرت ما كنت أنظر إليه؛ إذ كان ادعاءً لم يتحقق شرط تحفيزه إطلاقًا. وتسمية ذلك VACUOUS أكثر فائدة بكثير من الإبقاء على تصنيف أخضر، لأنها توجّه المراجع نحو الافتراض أو التحفيز الذي جعل البرهان أجوف.
ظللتُ أعود إلى هذه اللوحة أثناء العمل على تصنيفات السياسات. VACUOUS قد تبدو نتيجة قاسية حتى نفكر في البديل. فإذا احتفظ سجل الاعتماد النهائي ببرهان دون تسجيل أن مقدمته لا تنطلق أبدًا، تكون المراجعة قد تلقت استنتاجًا مجردًا من الشرط الذي يمنحه معناه. والسجل الأفضل هو الذي يجعل هذا القيد صريحًا ويترك للمراجع البشري أمرًا ملموسًا للتدقيق فيه. سجل إمكانية الوصول هذا مكانه الصحيح بجانب الحكم النهائي.
كان عليّ أيضًا مقاومة التعامل مع الجوف (vacuity) كتحذير شكلي بحت. فإذا كان الهدف من الخاصية تقييد شرط تحكيم، فإن سلوك التحفيز غير القابل للوصول يُعد دليلاً محوريًا حول ما إذا كانت الخاصية قد اختبرت السلوك المقصود بالفعل. ولا ينبغي للوحة التحكم أن تطلب من المراجع استنتاج ذلك من نتيجة خضراء؛ بل يجب أن تحتفظ بنتيجة إمكانية الوصول، وتستبعد النتيجة من مسار الشهادة، وتجعل إجراء المراجعة التالي واضحًا لا لبس فيه.
لقد زاد سياق الصناعة من خطورة الموقف في نظري. فدراسة عام 2024 الصادرة عن Wilson Research Group / Siemens EDA والمذكورة في مواصفات العرض التوضيحي تشير إلى معدل نجاح للسيليكون من المحاولة الأولى يبلغ 14% فقط. هذا ليس قياسًا خاصًا بـ Veriprajna، ولا تدّعي هذه اللوحة التركيبية تفسير هذا الرقم. لكنه يجعلني بالتأكيد أقل استعدادًا للتعامل مع حالة لوحة تحكم مبهجة كدليل بحد ذاتها.
خاصية خط الأنابيب نجت من العطل الذي توقعتُ أن تكتشفه
صادفتُ الإخفاق الثاني أثناء اختبار PIPE3، وهي خاصية خط أنابيب تركيبي ثنائي المراحل: assert v2 |-> (s2 == s2). كنتُ أريد مثالًا موجزًا لتأكيد يبدو منطقيًا بما يكفي ليمر عبر مراجعة سطحية. لكن النتيجة (consequent) هي تحصيل حاصل؛ إذ تنص على أن s2 تساوي نفسها. النتيجة لا تقيّد أي شيء.
الخطوة المهمة في العرض التوضيحي لا تقتصر على رصد تحصيل الحاصل في النص النثري. فبوابة الحوكمة تحقن طفرات تصميمية أحادية النقطة ذات صلة وتتساءل عما إذا كانت الخاصية ستبطلها (تقتلها). وفي حالة خط الأنابيب الضعيف المعروضة، PIPE3 تُسجّل نتيجة إبطال طفرات 0/6 (0/6 mutation kill result). فالخاصية تظل ناجحة مع النسخ المعطوبة ذات الصلة. ولهذا السبب تُسند السياسة تصنيف WEAK بدلاً من السماح لنتيجة PROVEN المجردة بالبقاء كدليل اعتماد. تختبر نتيجة الطفرات حساسية مفيدة وحقيقية.
تعلمتُ شيئًا غير مريح من محاولة جعل هذا المثال يبدو أقل وضوحًا. يمكن للإنسان أن يقرأ s2 == s2 ويرفضها سريعًا. لكن العديد من نقاط الضعف لن تعلن عن نفسها بهذا الوضوح. ولهذا السبب لم أرد أن يعتمد العرض التوضيحي على رصد المشغّل لنص مشبوه. فالمخرج المفيد حقًا هو الإجراء المنتظم: إمكانية الوصول، واختبار إهلاك الطفرات ذو الصلة، ومخروط التأثير (COI)، وقرار السياسة الذي يوثق أسبابه.
بتُّ أرى فحص الطفرات بوصفه طريقة منضبطة لرفض التفسيرات شديدة الملاءمة للبرهان. فالهدف ليس اصطناع إخفاق درامي، بل التساؤل عما إذا كانت الخاصية ستلاحظ تغييرًا محليًا ذا صلة في السلوك الذي يُفترض بها تقييده. وحين لا تفعل ذلك، تخبر النتيجة المراجع بأمر قابل للتنفيذ: هذا التأكيد يحتاج إلى تعزيز أو إلى مسار مراجعة مختلف قبل أن يتمكن من دعم سجل الاعتماد النهائي.
وهذا أيضًا هو السبب في أن معيار التقييم (benchmark) للعرض التوضيحي يحتاج إلى وصف دقيق. فتشغيله المحلي لـ python -m backend.bench يحقق نتيجة 18/18 مقابل مجموعة تأكيدات تركيبية مصنفة وثابتة، ويحدد 6 براهين كان خط الأساس غير الخاضع للحوكمة في العرض التوضيحي سيمررها بالموافقة التلقائية دون تدقيق. هذه الأرقام هي مجرد فحص لقابلية إعادة الإنتاج على البيئات التركيبية المصنفة لهذا العرض التوضيحي؛ وليست معدل إنتاج فعليًا، ولا ادعاءً عامًا حول التأكيدات التي يؤلفها الذكاء الاصطناعي، ولا مقارنة بأدوات التحقق الشكلي التجارية.
توقفتُ عن محاولة جعل البوابة تبدو متساهلة
كان أمامي خيار تصميمي بعد نتائج التدقيق الأولى: إما تلطيف الأحكام المحجوبة لتبدو اللوحة أكثر تفاؤلًا، أو ترك اللوحة ترفض اعتماد ما لا يمكنها الدفاع عنه. اخترتُ الخيار الثاني لأن مراجعة الاعتماد النهائي الحقيقية تحتاج إلى القدرة على التمييز بين البرهان الكامل والبرهان المحدود (bounded)، وبين المقدمة غير القابلة للوصول والخاصية ذات المغزى، وبين الفحص الضعيف وذلك الذي يستجيب للسلوك المعطوب ذي الصلة. حجب الاعتماد هو نتيجة مراجعة، وليس طريقًا مسدودًا.
ينعكس هذا الاختيار بوضوح في مفردات السياسة؛ إذ إن حكم TRUSTWORTHY هو ما ينال شهادة العرض التوضيحي الموقّعة. بينما BOUNDED-PROVEN، وVACUOUS، وWEAK، وDEAD، وVIOLATED تحتفظ بأسباب مختلفة لحجب تلك الشهادة أو تصعيد النتيجة. ففي بيئة عبور نطاقات الساعة (CDC) على سبيل المثال، فإن الخاصية الأقوى assert (req && !ack) |-> ##1 req تأتي بحكم VIOLATED وتنتج شكلاً موجيًا تركيبيًا ملموسًا لمثال مضاد. وهي توضح فئة من إخفاقات المعاملات المفقودة أو أخطاء CDC، ولا تعبر عن رقاقة عميل فعلية.
لا أرى في هذا دعوة لاستبدال المحرك الحالي لفريق التحقق؛ فالتوجه الإنتاجي مستقل تمامًا عن نوع المحرك: وضع بوابة حول سير عمل التحقق الشكلي الحالي، ثم جعل معايير القبول الخاصة بها قابلة للفحص. أما محولات المحركات الفعلية واستيعاب كود RTL الحقيقي فهما مؤجلان في هذا العرض التوضيحي. الحدود المعروضة ضيقة عن قصد. وتلك الحدود مهمة لأنها تجعل الادعاء متناسبًا مع ما يعمل بالفعل.
أريد الآن الإيصال بجانب الحكم
أواصل التفكير في المخرج التوثيقي الذي يحتاجه اجتماع الاعتماد النهائي حين يكون مؤلف التأكيدات مدعومًا بالذكاء الاصطناعي. إنه ليس درجة ثقة يضعها المؤلف؛ بل سجل يوضح الفحوصات التي جرى تشغيلها، وما كانت نتيجة إمكانية الوصول، وما الطفرات التي أُبطلت، وما الذي احتواه مخروط التأثير (COI)، ولماذا سمحت السياسة بالشهادة أو حجبتها. تحتاج المراجعة إلى أدلة يمكنها إعادة فتحها والتحقق منها.
وهذا بالضبط ما يصدّره العرض التوضيحي في ملف signoff_certificate.json: أحكام لكل خاصية، وإمكانية الوصول، ونتائج الطفرات، ومخروط التأثير (COI)، وسجلات الأمثلة المضادة عند انطباقها، وحقل SHA-256. لقد بنيتُ الشهادة كسجل تجريبي توضيحي لأن المراجع يجب أن يكون قادرًا على إعادة بناء القرار دون قبول شارة خضراء على سبيل الثقة العمياء. يجب على الشهادة أن تحفظ المسار المؤدي إلى حكمها.
وإذا كنتَ تفضل رؤية ذلك بدلاً من قراءة وصفي له، فإليك النظام بأكمله يعمل من البداية إلى النهاية.
لقد جعلتُ العرض التوضيحي قابلاً للتشغيل حتى يمكن فحص التحول المعاكس من 8/8 إلى 5/8 بدلاً من تكراره كشعار تسويقي. والنتيجة التي أخرج بها منه متواضعة لكنها راسخة: البرهان الجدير بالاعتماد يحمل دليلاً على ما قيّده، وما نجا منه، ولماذا يمكن لشخص ما الاعتماد عليه. يظل اللون الأخضر مفيدًا؛ لكنه يحتاج ببساطة إلى سجل يسمح للمراجع التالي بتقرير ما إذا كان يستحق المضي قدمًا.
