التحقق من التكافؤ الرسمي

الموسوعة الحرة

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

التحقق من التكافؤ ومستويات التجريد

بشكل عام، هناك مجموعة واسعة من التعريفات الممكنة للتكافؤ الوظيفي التي تغطي المقارنات بين مستويات مختلفة من التجريد وتفاوت دقة تفاصيل التوقيت.

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

تكافؤ الآلة المتزامنة

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

عادةً ما تخضع قائمة التوصيلات الأولية لعدد من التحويلات، مثل التحسين وإضافة هياكل التصميم للاختبار (DFT)، قبل استخدامها كأساس لتحديد مواقع العناصر المنطقية في التصميم المادي . كما تُجري برامج التصميم المادي الحديثة أحيانًا تعديلات جوهرية على قائمة التوصيلات (مثل استبدال العناصر المنطقية بعناصر مماثلة ذات قوة دفع و/أو مساحة أعلى أو أقل ). وخلال كل خطوة من خطوات هذه العملية المعقدة والمتعددة المراحل، يجب الحفاظ على الوظائف الأصلية والسلوك الموصوف في الكود الأصلي. وعند تصنيع الشريحة الرقمية النهائية ، تكون العديد من برامج التصميم الإلكتروني للدوائر المتكاملة (EDA)، وربما بعض التعديلات اليدوية، قد عدّلت قائمة التوصيلات.

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

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

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

ثمة طريقة بديلة لحل هذه المشكلة، وهي إثبات أن كود RTL وقائمة الشبكة المُصنّعة منه يتصرفان بنفس الطريقة تمامًا في جميع الحالات (ذات الصلة). تُسمى هذه العملية التحقق الرسمي من التكافؤ، وهي مشكلة تُدرس ضمن مجال أوسع هو التحقق الرسمي .

يمكن إجراء فحص تكافؤ رسمي بين أي تمثيلين لتصميم ما: RTL <> قائمة الشبكة، أو قائمة الشبكة <> قائمة الشبكة، أو RTL <> RTL، مع العلم أن الحالة الأخيرة نادرة مقارنةً بالحالتين الأوليين. عادةً، تُشير أداة فحص التكافؤ الرسمي بدقة عالية إلى موضع الاختلاف بين التمثيلين.

طُرق

هناك تقنيتان أساسيتان تستخدمان للاستدلال المنطقي في برامج التحقق من التكافؤ:

  • مخططات القرار الثنائية (BDDs): هي بنية بيانات متخصصة مصممة لدعم الاستدلال حول الدوال المنطقية. وقد اكتسبت مخططات القرار الثنائية شعبية كبيرة نظرًا لكفاءتها وتعدد استخداماتها.
  • إمكانية إرضاء الصيغة المنطقية الاقترانية: تُعيد خوارزميات حل مسائل SAT قيمةً لمتغيرات الصيغة المنطقية تُرضيها، إن وُجدت. يُمكن التعبير عن أي مسألة استدلال منطقي تقريبًا كمسألة SAT.

تطبيقات تجارية للتحقق من التكافؤ

أهم المنتجات في مجال التحقق من تكافؤ المنطق ( LEC ) في تصميم الدوائر الإلكترونية هي:

التعميمات

  • التحقق من تكافؤ الدوائر المعاد توقيتها: في بعض الأحيان يكون من المفيد نقل المنطق من جانب واحد من السجل إلى جانب آخر، وهذا يعقد مشكلة التحقق.
  • التحقق من التكافؤ التسلسلي: في بعض الأحيان، قد تختلف آلتان اختلافًا تامًا على المستوى التوافقي، لكنهما يجب أن تُعطيا نفس المخرجات عند إدخال نفس المدخلات. المثال الكلاسيكي هو آلتان متطابقتان للحالات، لكن لكل منهما ترميز مختلف للحالات. ولأن هذه الحالة لا يمكن اختزالها إلى مسألة توافقية، فإن الأمر يتطلب تقنيات أكثر عمومية.
  • تكافؤ البرامج، أي التحقق مما إذا كان برنامجان محددان جيدًا يأخذان N مدخلات وينتجان M مخرجات متكافئين: من الناحية النظرية، يمكن تحويل البرنامج إلى آلة حالة (وهذا ما يفعله المترجم، لأن الحاسوب وذاكرته يشكلان آلة حالة ضخمة). ومن ثم، نظريًا، يمكن لأشكال مختلفة من التحقق من الخصائص ضمان إنتاجهما نفس المخرجات. هذه المشكلة أصعب من التحقق من التكافؤ التسلسلي، لأن مخرجات البرنامجين قد تظهر في أوقات مختلفة؛ لكنها ممكنة، ويعمل الباحثون على حلها.

انظر أيضاً

مراجع

  • دليل أتمتة التصميم الإلكتروني للدوائر المتكاملة ، من تأليف لافاجنو ومارتن وشيفر، رقم ISBN 0-8493-3096-3دراسة استقصائية للمجال. تم استخلاص هذه المقالة، بإذن، من المجلد 2، الفصل 4، التحقق من التكافؤ ، بقلم فابيو سومينزي وأندرياس كولمان.
  • RE Bryant، خوارزميات قائمة على الرسوم البيانية لمعالجة الدوال المنطقية ، معاملات IEEE للحاسبات، C-35، ص  677-691، 1986. المرجع الأصلي حول BDDs.
  • التحقق من التكافؤ التسلسلي لنماذج RTL. نيخيل شارما، غاغان هاستير، وفينكات كريشناسوامي. إي إي تايمز .