Faver: Повышение генерации RTL на основе LLM с помощью функционально абстрактного проверяемого промежуточного слоя

Основная информация

• ID статьи: 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 является наименее автоматизированным и наиболее трудоёмким этапом проектирования микросхем. Хотя LLM демонстрируют потенциал в генерации 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% на нескольких тестовых наборах и LLM
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: LLM генерирует Verilog testbench
• baseline-L: LLM как судья
• baseline-P: LLM генерирует Python testbench (без 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. Благодаря инновационному дизайну функционально абстрактного промежуточного слоя, она эффективно решает проблему семантической пропасти между верификацией программного и аппаратного обеспечения. Результаты экспериментов убедительны, метод имеет хорошую практическую ценность и академическое влияние.