TensorEQC: Structure-Aware Equivalence Checking with GF(2) Algebra, Exact Tensor Networks, and Reset Analysis : a Multi-Algorithmic Study of Datapath Verification and Reset-State Dependence

ملخص تقني: TensorEQC – التحقق من التكافؤ المدرك للبنية

بيان المشكلة
يعد التحقق من التكافؤ (Equivalence Checking - EC) حساسًا للغاية لتمثيل الدائرة. فالدارات ذات البنى المختلفة — مثل الشبكات الغنية بعمليات XOR، وسلاسل الحمل (carry chains)، ومضاعفات الحقول المنتهية، ومضاعفات الأعداد الصحيحة — تظهر خصائص بنيوية متميزة تفضل مناهج تحقق مختلفة. لا توجد طريقة واحدة (مثل الجبر البولياني، أو المخططات القرارية، أو الشبكات التنسورية) تهيمن عالميًا على جميع أنواع الدارات. علاوة على ذلك، يتطلب التحقق من الدارات التزامنية التمييز بين الاعتماد على الحالة الأولية القابل للملاحظة وبين حالة عدم اليقين التي تنتهي في حدود ملاحظة معينة، لا سيما فيما يتعلق بحالات إعادة الضبط (reset states).

المنهجية
يقدم البحث TensorEQC، وهو سير عمل بحثي قابل للتنفيذ مصمم كـ "محفظة متعددة الخوارزميات" (multi-algorithmic portfolio) بدلاً من كونه حلاً أحاديًا ضخمًا. وتتمثل فلسفته الجوهرية في أن المحرك يجب أن يفرغ التزام التحقق فقط إذا استطاع القيام بذلك وفقًا لمعانيه الدقيقة الخاصة؛ وإلا، يتم تمرير الالتزام إلى محرك آخر.

يتكون سير العمل من ثلاثة مكونات رئيسية:

1. المحفظة التوافقية (Combinational Portfolio): وهي عبارة عن خط أنابيب تسلسلي لمحركات التحقق، يعالج المخرجات حتى يتم إفراغ الالتزام أو الوصول إلى حد استهلاك الموارد. يتضمن خط الأنابيب ما يلي:
   • التجزئة البنيوية (Structural Hashing): لإثبات هوية مخططات الرسم البياني الموجه غير الدوري (DAGs) للتعبيرات تحت ركائز مدعومة (AND, OR, XOR، إلخ) مع التطبيع التبادلي.
   • المحاكاة (Simulation): تستخدم المحاكاة المجمعة (packed simulation) مع أنماط عشوائية، وأنماط صفرية كاملة، وأنماط وحيدة كاملة لإيجاد الشهود السلبية (negative witnesses/counterexamples).
   • الأشكال الجبرية الطبيعية (ANF): تمثل الدوال البوليانية كمتعددات حدود متعددة الخطية فوق الحقل GF(2). وهي تستخدم تمهيدية (lemma) محددة لتوليد شهود سلبية دقيقة من متعددات الحدود غير الصفرية.
   • الحذف التنسوري العلاقي (Relational Tensor Elimination): يمثل البوابات كمؤشرات تنسورية بوليانية. ويقوم بعملية حذف المتغيرات عبر الفصل (disjunction) فوق شبه حلقة (semiring) بوليانية (للحفاظ على وجود التعيينات المرضية) بدلاً من الجمع فوق GF(2) (الذي يحسب التكافؤ/parity).
   • ROBDD والحل النهائي الشامل: يستخدم مخططات القرار الثنائية المرتبة (Ordered Binary Decision Diagrams) مع سقف للعقد (node caps) وتعداد شامل للدعم الصغير كحلول نهائية.
2. تحليلات قطار التنسور (Tensor Train - TT): وحدة مرافقة تبني تمثيلات TT دقيقة من جداول الحقيقة لقياس الرتبة الجبرية واختبار الدوال الصفرية. وهي تميز بين الرتب فوق GF(2) والرتب فوق الأعداد الحقيقية، مشيرة إلى أن رتب GF(2) يمكن أن تكون أصغر بكثير.
3. تحليل إعادة الضبط (Reset Analysis): وحدة متزامنة تستخدم التركيب الذاتي للحالة الصريحة للتحقق من الاعتماد على الحالة الأولية. وهي تميز بين الحالات التي يكون فيها الاعتماد على إعادة الضبط ملاحظًا فورًا والحالات التي يختفي فيها بعد عدد معين من دورات "التطهير" (flushing cycles).

المساهمات الرئيسية

• تكامل المحركات الدقيقة: يوضح العمل التكامل العملي بين التجزئة البنيوية، والجبر GF(2)، والشبكات التنسورية العلاقية، وROBDDs، مع الحفاظ على عقود إثبات متميزة لكل منها.
• استراتيجية مدركة للبنية: يقدم أدلة تجريبية على أن كفاءة التحقق تعتمد بشدة على بنية الدائرة وترتيب المتغيرات. فعلى سبيل المثال، تنتج معاملات الجمع المتداخلة رتبًا تنسورية منخفضة (≤3)، بينما تؤدي المعاملات المنفصلة إلى رتب عالية (129)، مما يجعل الأخيرة أقل ملاءمة للمناهج القائمة على التنسور.
• تشخيصات حالة إعادة الضبط: يوفر طريقة للتمييز بوضوح بين الاعتماد الحقيقي على الحالة الأولية وبين عدم اليقين العابر في التصميمات المتزامنة.
• التحقق القابل لإعادة الإنتاج: يتضمن البحث ملحقًا جديدًا ومستقلاً بذاته يتحقق من بناء قطار تنسور GF(2) الدقيق، وقياسات الرتبة، واختبارات الدالة الصفرية لخمس دالات بمدخلات 16، مما يؤكد التمييز بين إلغاء التكافؤ (parity cancellation) والدوال الصفرية الفعلية.

النتائج التجريبية
تقرير الدراسة يعتمد على مجموعتين متميزتين من الأدلة:

1. حمل المحفظة التاريخي (v1.0.0): تتضمن هذه المجموعة 89 عملية تشغيل تشمل جامعات تسلسلية (ripple adders) بطول 2,048 بت، ومضاعفات ذات أساس حدودي بطول 128 بت، وشبكات تآلفية (affine networks).
   • النجاحات: نجح التدفق الكامل في التحقق من جامعات ripple بطول 2,048 بت (2.87 ثانية) ومضاعفات GF بطول 128 بت (0.80 ثانية)، متفوقًا على مناهج BDD-only في حالات محددة (مثل الجامعات بطول 2,048 بت حيث فشلت BDDs في الحل).
   • القيود: اصطدم النهج بحدود الموارد (سقف العقد، سقف العرض) في الجامعات بطول 1,024 بت والشبكات التآلفية بطول 1,024 مدخل. كما اقتصرت نتائج ضرب الأعداد الصحيحة على 10 بت بسبب نمو ANF وسقوف نطاق التنسور.
   • ملاحظة: أدى التدفق الكامل أحيانًا إلى تكبد أعباء إضافية (overhead) مقارنة باختيار المحرك الأمثل مباشرة، مما يسلط الض الضوء على المقايضة بين الأتمتة والكفاءة.
2. الملحق الجديد القابل لإعادة الإنتاج: أكدت تجربة مركزية على خمس دالات بـ 16 مدخلًا (بما في ذلك التكافؤ وضرب GF) أن بناء قطار التنسور الدقيق وتحليل الرتبة أمر ممكن للدوال الصغيرة. كما أثبتت أن المجموع القياسي لـ GF(2) الذي يساوي صفرًا لا يعني بالضرورة دالة صفرية (إلغاء التكافؤ)، وهو تمييز عالجه اختبار الصفر في TT بشكل صحيح.

الأهمية والادعاءات
يؤطر البحث مساهمته صراحةً كـ تقييم تقني محدد النطاق وليس كحل عالمي.

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

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