2025-11-12T17:13:10.726463

Faver: Boosting LLM-based RTL Generation with Function Abstracted Verifiable Middleware

Mu, Shi, Wang et al.
LLM-based RTL generation is an interesting research direction, as it holds the potential to liberate the least automated stage in the current chip design. However, due to the substantial semantic gap between high-level specifications and RTL, coupled with limited training data, existing models struggle with generation accuracy. Drawing on human experience, design with verification helps improving accuracy. However, as the RTL testbench data are even more scarce, it is not friendly for LLMs. Although LLMs excel at higher-level languages like Python/C, they have a huge semantic gap from RTL. When implementing the same functionality, Python/C code and hardware code differ significantly in the spatiotemporal granularity, requiring the LLM not only to consider high-level functional semantics but also to ensure the low-level details align with the circuit code. It is not an easy task. In this paper, we propose a function abstracted verifiable middleware (Faver) that streamlines RTL verification in LLM-based workflows. By mixing LLM-friendly code structures with a rule-based template, Faver decouples the details of circuit verification, allowing the LLM to focus on the functionality itself. In our experiments on the SFT model and open-source models, Faver improved the model's generation accuracy by up to 14%.
academic

Faver: تعزيز توليد RTL القائم على نماذج اللغة الكبيرة باستخدام برنامج وسيط قابل للتحقق من الوظائف المجردة

المعلومات الأساسية

  • معرّف الورقة: 2510.08664
  • العنوان: Faver: Boosting LLM-based RTL Generation with Function Abstracted Verifiable Middleware
  • المؤلفون: Jianan Mu, Mingyu Shi, Yining Wang, Tianmeng Yang, Bin Sun, Xing Hu, Jing Ye, Huawei Li
  • التصنيف: cs.SE cs.AI
  • تاريخ النشر: 9 أكتوبر 2025 (نسخة أولية من arXiv)
  • رابط الورقة: https://arxiv.org/abs/2510.08664

الملخص

تقدم هذه الورقة برنامجاً وسيطاً قابلاً للتحقق من الوظائف المجردة (Faver) لمعالجة مشكلة دقة توليد كود RTL القائم على نماذج اللغة الكبيرة (LLM). يجمع هذا الأسلوب بين بنية الكود الودية لـ LLM والقوالب المستندة إلى القواعد، مما يفصل تفاصيل التحقق من الدوائر، مما يسمح لـ LLM بالتركيز على الوظيفة نفسها. في التجارب على نماذج SFT والنماذج مفتوحة المصدر، يحسّن Faver دقة توليد النموذج بما يصل إلى 14%.

خلفية البحث والدافع

1. المشكلة الأساسية

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

2. أهمية المشكلة

  • تصميم RTL هو اختناق حرج في تدفق تصميم الدوائس المتكاملة
  • يمكن لأتمتة توليد RTL أن تحسّن بشكل كبير من كفاءة تصميم الرقائق
  • الطرق الحالية لا تستطيع الاستفادة الفعالة من خبرة الإنسان في "التصميم والتحقق"

3. قيود الطرق الموجودة

  • الحكم المباشر من LLM: يفتقر إلى أدوات استدلال قوية للتحقق من الوظائف بناءً على المواصفات
  • توليد RTL testbench: بيانات testbench أكثر ندرة من بيانات التصميم، وصعوبة التوليد مماثلة لتصميم RTL
  • التحقق البسيط من Python: الفروقات الضخمة بين الأجهزة والبرامج في الحبيبية الزمانية والمكانية تجعل التحقق المشترك صعباً

4. دافع البحث

الاستفادة من خبرة التصميم البشري في طريقة "التصميم والتحقق"، مع الحاجة إلى حل الصعوبات الأساسية لـ LLM في التحقق من الأجهزة، خاصة تحديات المتغيرات المتعلقة بالتوقيت وتوليد محفزات الاختبار.

المساهمات الأساسية

  1. اقتراح إطار عمل Faver: يسمح لـ LLM بكتابة كود دلالي عالي المستوى للتحقق من الدوائر، والاستفادة من إطار عمل التصميم والتحقق
  2. تصميم قوالب الوظائف-الفئات المجردة: تعيين دلالات الساعة والسجلات في تصميم الأجهزة إلى فئات Python/C التي تعتمد على الأحداث، مما يقلل الفجوة الزمانية والمكانية بين التحقق من الأجهزة والبرامج
  3. التحقق التجريبي: إثبات أن Faver يحسّن دقة توليد RTL القائم على LLM بما يصل إلى 14% على مجموعات اختبار ونماذج متعددة
  4. التحليل النظري: توفير نماذج رياضية لمعدل نجاح النظام ومعدل صحة التغذية الراجعة

شرح الطريقة

تعريف المهمة

الإدخال: وصف المواصفات باللغة الطبيعية لمتطلبات الوظائف الأجهزة الإخراج: كود RTL (Verilog) صحيح وظيفياً ويمر التحقق القيود: يجب أن يكون RTL المُولّد صحيحاً من حيث الصيغة والوظيفة

معمارية النموذج

يتضمن إطار عمل Faver أربع خطوات رئيسية:

1. توليد مواصفات التحقق (Verification Specification Generation)

  • الحفاظ على منافذ الإدخال/الإخراج: الاحتفاظ بنفس تعريفات منافذ الإدخال والإخراج
  • التجريد الوظيفي: تحويل الاتصالات الطوبولوجية لـ RTL إلى منطق معالجة الإدخال والإخراج للبرامج
  • تحليل الحدود: تحليل شروط الحدود لـ RTL وتعدادها في مواصفات التحقق

2. توليد نموذج مرجعي قائم على قالب الفئة

التصميم الأساسي:

class ref_model(Model):
    def __init__(self):
        global state_flag0, state_flag1  # تعيين السجلات كمتغيرات عامة
    
    @driver_hook()
    def reset(self):  # دالة إعادة تعيين مخصصة
        pass
    
    @driver_hook() 
    def step(self):   # واجهة وظيفية موحدة
        pass
    
    def func1(self):  # دوال وظيفية أخرى
        pass

التقنيات الرئيسية:

  • تعيين السجلات إلى المتغيرات العامة: تعيين سجلات الأجهزة كمتغيرات عامة على مستوى الفئة
  • الساعة كحدث: معاملة حافة الساعة الصاعدة كحدث "استدعاء step"
  • واجهة موحدة: الوصول الموحد إلى الوحدات المختلفة من خلال دالة step

3. توليد محفزات الاختبار الهرمي

آلية التعاون بين LLM والقواعد:

  • التخطيط عالي المستوى: يصمم LLM خطة اختبار لضمان التغطية الشاملة لفضاء الوظائف
  • توليد البيانات الزمنية: ينتج LLM بيانات إدخال زمنية ذات ارتباط وظيفي قوي
  • التحسين المستند إلى القواعد:
    • إدراج دالة إعادة التعيين المستندة إلى القواعد
    • فحص وتصحيح الحدود على تدفقات البيانات

4. المحاكاة المشتركة والتحسين التكراري

  • استخدام محاكاة Python-Verilog المشتركة للمطابقة الدقيقة
  • مقارنة الموجات على مستوى الأحرف، وتصنيف أنواع الأخطاء (أخطاء وظيفية، عدم تطابق التوقيت، مشاكل الشروط الحدية)
  • تعيين حد التكرار إلى 5 مرات لتجنب الحلقات اللانهائية

نقاط الابتكار التقني

  1. جسر الفجوة الدلالية: تحويل طوبولوجيا الدوائر إلى منطق البرامج من خلال التجريد الوظيفي
  2. استخراج المتغيرات الزمنية: تعيين مبتكر لمفاهيم التوقيت الأجهزة إلى نموذج البرامج الموجهة بالأحداث
  3. استراتيجية التحقق الهرمي: الجمع بين القدرات الدلالية العالية المستوى لـ LLM والدقة في نظام القواعد

إعداد التجارب

مجموعات البيانات

  • RTLLM: مجموعة معايير توليد كود RTL الأكاديمية
  • VerilogEval: مجموعة تقييم توليد كود Verilog الأخرى المستخدمة على نطاق واسع
  • بيانات SFT المجمعة ذاتياً: أكثر من 5000 زوج من أوصاف اللغة الطبيعية وكود RTL

مقاييس التقييم

  • Pass@1: معدل النجاح في التوليد الفردي
  • Pass@5: معدل النجاح حيث يمر واحد على الأقل من خمس عمليات توليد
  • sys_sel_pass@1: معدل نجاح نظام التصميم والتحقق في إخراج تصميم واحد
  • sys_inner_pass@5: معدل نجاح أي تصميم من بين خمس تكرارات داخلية

طرق المقارنة

النماذج الأساسية:

  • DeepSeek-R1-0528, Kimi K2, GPT-4O, QWQ-32B
  • Qwen2.5-Coder-32B-Instruct

نماذج SFT:

  • سلسلة CodeV, RTLCoder-Mistral-7B, CraftRTL-SC2-15B
  • Qwen2.5-7B-SFT (تدريب ذاتي)

خطوط أساس التحقق:

  • baseline-V: توليد Verilog testbench من قبل LLM
  • baseline-L: LLM كحكم
  • baseline-P: توليد Python testbench من قبل LLM (بدون Faver)

تفاصيل التنفيذ

  • استخدام Toffee (منصة محاكاة Python-Verilog المشتركة المستندة إلى Verilator)
  • تعيين حد الفشل المستمر إلى 5
  • استخدام طريقة LoRA لتدريب SFT لتقليل التكاليف الحسابية

نتائج التجارب

النتائج الرئيسية

تحسينات الأداء الكبيرة:

  • DeepSeek-R1-0528 على RTLLM: تحسن Pass@1 من 74% إلى sys_sel_pass@1 بنسبة 83%
  • Qwen2.5-7B-SFT: تحسن sys_inner_pass@5 بنسبة 14% مقارنة بالنموذج الأصلي
  • النماذج الأساسية تحقق تحسناً عاماً بحوالي 10% في معدل النجاح

الاتساق عبر النماذج: تظهر جميع النماذج المختبرة تحسناً متسقاً على مجموعتي البيانات، مما يثبت الفعالية العامة لـ Faver.

تجارب الاستئصال

تحليل مساهمة المكونات:

  • Faver- (بدون توليد محفزات الاختبار): تحسن متوسط بنسبة 2.75%
  • Faver الكامل: تحسن يصل إلى 12%
  • يثبت أن توليد النموذج المرجعي وتوليد محفزات الاختبار الهرمي كلاهما يساهم بشكل مهم في تحسين الأداء

تحليل أداء المدقق

مقاييس الدقة:

  • True Positive أعلى بشكل ملحوظ من False Positive
  • True Negative أعلى بشكل ملحوظ من False Negative
  • يتحقق من الشروط a > b و c > d في التحليل النظري

تأثير التحسين التكراري:

  • يظهر Faver-DeepSeek-R1-0528 تحسناً مستقراً في معدل الدقة أثناء العملية التكرارية
  • يظهر DeepSeek-R1-0528 الأصلي نمطاً عشوائياً من التقلبات في معدل الدقة

تحليل الحالات

مثال على تصميم نواة الالتفاف:

  1. التجريد الوظيفي: تحويل الاتصالات الطوبولوجية للمضاعفات والمجمعات إلى عملية التفاف
  2. معالجة الحدود: تحديد قيود عرض البيانات 8 بت ومشاكل مطابقة الأبعاد
  3. تعيين التوقيت: تحويل تدفق البتات المدفوع بالساعة إلى سلسلة استدعاءات دالة step

الأعمال ذات الصلة

الاتجاهات البحثية الرئيسية

  1. توليد RTL القائم على LLM: ChipGPT, ChipNeMo, BetterV وغيرها من النماذج المتخصصة
  2. طرق التصميم والتحقق: VerilogCoder, MAGE وغيرها التي تعتمد على تغذية راجعة التحقق
  3. التحقق من RTL: VerilogReader وغيرها التي تركز على توليد متجهات الاختبار

مزايا هذه الورقة

  • أول معالجة منهجية لمشكلة الفجوة الزمانية والمكانية في التحقق المشترك Python-RTL
  • توفير إطار عمل تحقق كامل من النهاية إلى النهاية، بدلاً من الاعتماد على منصات اختبار يدوية
  • تجنب قيود طرق التنبؤ البسيطة بالإخراج من خلال التجريد الوظيفي

الخلاصة والمناقشة

الاستنتاجات الرئيسية

  1. نجح Faver في جسر الممارسات الموجهة بالبرامج والخصائص المعتمدة على الحالة الزمنية في تصميم الأجهزة
  2. التغذية الراجعة للتحقق الدقيق على مستوى الوظائف أمر حاسم لتحسين إخراج LLM في بيئات تصميم الأجهزة
  3. استراتيجية التحقق الهرمي تجمع بشكل فعال بين القدرات الدلالية لـ LLM ودقة نظام القواعد

القيود

  1. حد التكرار: قد لا يكون تعيين حد تكرار ثابت بقيمة 5 مناسباً لجميع مستويات التعقيد في التصميم
  2. اعتماد نظام القواعد: لا تزال فحوصات الحدود ومنطق الإعادة تتطلب قواعس محددة مسبقاً
  3. قيود مجموعة البيانات: يركز التقييم بشكل أساسي على معايير أكاديمية نسبياً بسيطة

الاتجاهات المستقبلية

  1. التوسع إلى تصاميم أجهزة أكثر تعقيداً (مثل المعالجات و SoC)
  2. حدود تكرار تكيفية وتصنيف أخطاء أكثر ذكاءً
  3. التكامل مع سلاسل أدوات EDA الموجودة

التقييم المتعمق

المزايا

  1. الابتكار التقني: أول معالجة منهجية لمشكلة التوقيت في LLM للتحقق من الأجهزة، مع تحقيق تعيين دلالي فعال من خلال قوالب الفئات والنموذج الموجه بالأحداث
  2. كفاية التجارب: تقييم شامل على نماذج ومجموعات بيانات متعددة، بما في ذلك تجارب الاستئصال والتحليل النظري
  3. القيمة العملية: توفير تنفيذ مفتوح المصدر كامل مع قابلية إعادة إنتاج جيدة
  4. الدعم النظري: توفير نماذج رياضية لمعدل نجاح النظام، مما يعزز الأساس النظري للطريقة

أوجه القصور

  1. نطاق التقييم: التقييم يركز بشكل أساسي على معايير أكاديمية، مع نقص التحقق من تصاميم معقدة على مستوى الصناعة
  2. نظام القواعد: لا يزال يعتمد على قواعس محددة مسبقاً لفحص الحدود، مع درجة محدودة من الأتمتة
  3. قابلية التوسع: لم يتم التحقق الكافي من قابلية الطريقة للتوسع إلى تصاميم أجهزة معقدة جداً

التأثير

  1. المساهمة الأكاديمية: توفير نموذج تحقق جديد لمجال توليد تصميم الأجهزة القائم على LLM
  2. القيمة العملية: يمكن تطبيقها مباشرة على تدفقات تصميم RTL الموجودة، مع تأثير فوري
  3. قابلية الإعادة: مبنية على أدوات مفتوحة المصدر، مما يسهل على المجتمع البحثي إعادة الإنتاج والتوسع

السيناريوهات المناسبة

  • تصميم الدوائر الرقمية متوسطة التعقيد
  • تطوير الأجهزة الذي يتطلب التحقق السريع من النماذج الأولية
  • بيئات التعليم والبحث لتوليد كود RTL
  • كأداة تحقق مساعدة لأدوات EDA الموجودة

المراجع

تستشهد الورقة بأعمال مهمة في هذا المجال، بما في ذلك:

  • ChipGPT, ChipNeMo وغيرها من نماذج LLM المتخصصة في تصميم الأجهزة
  • VerilogCoder, MAGE وغيرها من طرق التصميم والتحقق
  • RTLLM, VerilogEval وغيرها من معايير التقييم القياسية
  • Toffee, Verilator وغيرها من أدوات المحاكاة المشتركة

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