Привет! Меня зовут Андрей, я занимаюсь в YADRO верификацией аппаратного обеспечения. В разработке цифровых устройств (GPU, CPU, AI-ускорители) большое внимание уделяют трактам обработки данных (datapath). Архитекторы создают эталонные модели блоков на языках высокого уровня (C/C++), чтобы быстрее проводить архитектурные исследования и отладку алгоритмов — например, операции с плавающей точкой, полиномы, матричные умножения. Однако конечная реализация выполняется на RTL (Verilog/SystemVerilog).

После реализации в виде RTL-кода всегда хочется проверить соответствие итогового дизайна оригинальной модели. В этот момент в мире ASIC-разработки часто начинают думать сразу о UVM, корнер-кейсах и прочих долгих прелюдиях перед оформлением багов.

В качестве альтернативы здесь выступает формальная верификация. Если вы работаете в небольшом стартапе, то, скорее всего, вам нужен маршрут формальной верификации, описанный моим коллегой в статье «Формальная верификация „для бедных“: выбираем open-source решение». Но если вам повезло работать в крупной полупроводниковой компании с доступом к коммерческим инструментам формальной верификации, то можно подумать о проверке логической эквивалентности между C и RTL-кодом.

Один из популярных инструментов для такой проверки — это Jasper C2RTL App в составе платформы Cadence JasperGold. По механике он очень похож на известные многим инструменты LEC и SEC, но в качестве эталонной реализации здесь выступает код на C.

В этой статье мы рассмотрим, как работает C2RTL, из каких этапов состоит процесс верификации с ним, как формируются проверки (ассерты) и с какими ограничениями сталкиваются инженеры.

Общий маршрут верификации C2RTL

Процесс верификации в C2RTL итеративный и включает следующие ключевые шаги:

1. Компиляция эталонной модели в C/С++. Для компиляции используется встроенный С-компилятор, условный GCC из апстрима не подойдет.

2. Компиляция реализации (RTL). Используется стандартный RTL-компилятор, встроенный в JasperGold.

3. Мапирование сигналов: мы рассказываем инструменту, какие входы/выходы модели соответствуют входам и выходам реализации.

4. Генерация верификационного окружения. На основе маппинга C2RTL генерирует формальные свойства (ассерты), проверяющие, что выходы RTL эквивалентны выходам C++ модели при заданных условиях и задержках.

5. Доказательство непротиворечивости ассертов. C2RTL использует специализированные word-level движки, оптимизированные для работы с арифметикой и трактами данных, в отличие от классических bit-level движков.

6. Отладка ассертов с контрпримерами. В C2RTL отладка не отличается от любого другого приложения в составе JasperGold, поэтому особо останавливаться тут не будем.

Компиляция эталонной модели

Так как в качестве эталонной модели используется С/С++, то сравнение с RTL-кодом становится непростым. Поэтому JasperGold выполняет конвертацию С/С++ описания в крайне низкоуровневый RTL. Сгенерированный таким образом код из-за ограничений инструмента мне посмотреть не удалось, но можно открыть и посмотреть схему этого кода, что бывает полезно при отладке. Она немного похожа на HSL (High Level Synthesis), где как раз выполняется конвертация С/С++ кода в RTL-описание. Для примера можем взять код сумматора на С:

int main () {
   unsigned int result_0_o;
   unsigned int operant_0_i;
   unsigned int operand_1_i;
   #ifdef JASPER_C
       JASPER_INPUT(operant_0_i);
       JASPER_INPUT(operand_1_i);
   #endif
   result_0_o = operant_0_i + operand_1_i;
   #ifdef JASPER_C
       JASPER_OUTPUT(result_0_o);
   #endif
}

В этом коде мы берем два операнда, складываем и выдаем результат. Соответственно, вместо функции сложения может быть код произвольной сложности. По результату можно открыть схему и посмотреть, во что сконвертировался код: в данном случае мы получаем ожидаемый сумматор.

Для компиляции, как обычно, есть два пути: нажимать кнопочки через GUI (такое мы не одобряем) и скриптование через старый добрый TCL. Команда для компиляции достаточно проста и имеет минимум «ручек», где во флаги можно передать макросы и пути для поиска инклюдов:

check_c2rtl -compile -spec $filelist -flags $cpp_flags

Оптимизация эталонной модели

Для упрощения сгенерированной модели и ускорения проверок JasperGold поддерживает оптимизацию через обрезание логики: весь не участвующий в проверках код удаляется, и логики становится меньше. На больших дизайнах обрезание может занять десятки минут, но зато потом при проверках результата иногда удается экономить часы. Для включения оптимизации нужна всего одна команда:

check_c2rtl -spec -set_dynamic_pruning -total_time_limit 600 -per_branch_time_limit 100

Как формируются ассерты

C2RTL генерирует два типа ассертов: одни проверяют эквивалентность C и RTL кода, другие — корректность самой синтезированной C модели (самопроверка трансляции кода).

Ассерты эквивалентности

Перед генерацией ассертов на проверку эквивалентности необходимо выполнить мапирование сигналов между моделью и реализацией. Мапирование входов устроено весьма просто:

check_c2rtl -map -spec {{<signal_from_model>}} -imp {{<signal_from_rtl>}}

После такой команды инструмент формальной верификации будет рассчитывать эквивалентность с учетом одинаковых воздействий на входы модели и реализации. Для связи выходов и непосредственно генерации ассертов необходима чуть более длинная команда:

check_c2rtl -map \
    -spec {{<signal_from_model>}} \
    -imp {{<signal_from_rtl>}} \
    -imp_delay <pipeline_delay_in_clocks> \
    -map_condition {<output_valid>} \
    -clock {posedge clk} \
    -disable {~rst_n}

Команда стала длиннее, так как требуется дополнительно указывать задержку и триггер. Задержка необходима, поскольку эталонная модель на C зачастую является комбинационной, а конвейер RTL имеет некоторую задержку.

Для каждой пары сопоставленных выходных сигналов формируется свойство SystemVerilog Assertion (SVA). Общий вид свойства:

@ (clocking_event)
    disable iff (disable_cond_expr)
    (
        (##spec_delay_value 1'b1).triggered and map_condition.triggered)
        |->
        spec_signal == $past(imp_signal, spec_delay_value)
    )

В коде ассерта spec_signal — это сигнал из модели, impl_signal — это сигнал из RTL, spec_delay_value — это задержка конвейера. То есть мы, по сути, ждем триггер и проверяем, что результат RTL совпадает с выдачей модели N тактов назад.

Интерфейсы модели

Внимательный читатель уже пару абзацев как должен задаваться вопросом: откуда интерфейсы у модели на C? Заботливый Cadence заготовил для нас специальные макросы, которые необходимо добавить в код:

#ifdef JASPER_C
  #include <jasperc.h>
#endif

int main() {
    unsigned short int ina[32];
    unsigned short int inb[32];
    unsigned short int out[32];
    bool op;

    #ifdef JASPER_C
        JASPER_INPUT_ARRAY (ina);
        JASPER_INPUT_ARRAY (inb);
        JASPER_INPUT(op);
    #endif

    for(int i = 0; i < 32; ++i) {
        if(op)
            out[i] = ina[i] + inb[i];
        else
            out[i] = ina[i] - inb[i];
    }

    #ifdef JASPER_C
        JASPER_OUTPUT_ARRAY (out);
    #endif
}

В простом примере выше интерфейсы определяются с помощью макросов JASPER_INPUT_ARRAY/JASPER_INPUT и JASPER_OUTPUT_ARRAY. В документации доступно чуть больше вариаций для корректной обработки разных ситуаций — например, использования структур и т. д. Таким образом, если аккуратно обложить код макросами, то можно использовать одни и те же исходники как для верификации, так и для локальной отладки модели.

Если вам интересна верификация, возможно, вас заинтересуют и наши вакансии:

• Cтарший инженер по верификации (Wireless & Systems)

• Инженер по верификации (Wireless & Systems)

• Инженер по UVM-верификации

Ассерты корректности синтеза кода на C/C++ в RTL

C2RTL имеет встроенную возможность генерации ассертов для кода на C/C++. Для достоверности результатов это наиболее важно. Если ассерты дают контрпример (CEX), то результаты сравнения эквивалентности считаются невалидными: скорее всего, исходное высокоуровневое описание было сконвертировано в RTL некорректно.

Инструмент автоматически генерирует следующие проверки:

• InsufficientLoopBound / InsufficientFunctionRecursion. Проверка, что количество итераций цикла или глубина рекурсии не превысили лимит развертки (по умолчанию 256). Если лимит мал, синтез может быть неполным.

• VLASizeLimit. Если в коде используется динамическое выделение памяти (malloc, new) или массивы переменной длины (VLA), инструмент синтезирует память фиксированного размера (по умолчанию 256 байт). Ассерт проверяет, что программа не обращается за пределы этого выделенного буфера.

• ReachableUFC (Unimplemented Function Calls). Если в коде на C++ объявлена, но не определена функция или она взята из списка неподдерживаемых стандартных библиотек, инструмент «блэкбоксит» ее: подставляет черный ящик и дальше самостоятельно драйвит выходное значение. Ассерт проверяет, достижим ли вызов этой функции.

• UnresolvedFunctionPointer. Проверка, что указатель на функцию или вызов виртуальной функции всегда указывает на корректно существующую функцию.

• UndefinedShift. Проверка безопасности операций сдвига (<<, >>). В C++ поведение сдвига на отрицательное число или на число, превышающее разрядность, не определено. C2RTL перехватывает такие случаи, чтобы избежать расхождений с семантикой SystemVerilog.

Ограничения и требования к коду

Использование C2RTL накладывает определенные ограничения на стиль C++ кода, чтобы гарантировать корректный синтез формальной модели.

Обязательная инструментация макросами

Исходный C++ код требует минимальных модификаций с использованием макросов в блоках #ifdef JASPER_C:

• JASPER_INPUT / JASPER_OUTPUT — определение портов модели.

• JASPER_SHOW — сохранение внутренней переменной в формальной модели для отладки. По умолчанию переменные, не влияющие на вывод, могут быть вырезаны оптимизацией.

• JASPER_BUFFER — создание промежуточного буфера.

Однако следует внимательно следить за предупреждениями в логе. Особенности работы формальных инструментов таковы, что если какая-то конструкция языка окажется несинтезируемой, то JasperGold может просто откинуть часть логики модели и заменить ее на черный ящик. А инженеру потом придется искать, откуда появились странные результаты в контрпримерах.

Обработка циклов и рекурсии

Инструмент C2RTL не поддерживает синтез циклов «как есть». Он должен развернуть их (unroll).

По умолчанию лимит развертки — 256. Если компилятор не может определить статическую границу цикла, он разворачивает его 256 раз. Если цикл требует большего числа итераций для корректной работы, это приведет к ложному срабатыванию InsufficientLoopBound и невозможности верификации.

Наконец, важно упомянуть, что вложенные циклы могут приводить к экспоненциальному росту модели.

Динамическая память

Динамическое выделение памяти поддерживается, но синтезируется как статический массив фиксированного размера — 256 байт по умолчанию. Сюрпризов для формального верификатора тут нет. Во всех применениях для сокращения сложности и ускорения доказательства необходимо сокращать объемы используемой памяти. Динамическое выделение превращается в статическое выделение «под капотом» и до некоторого времени будет работать незаметно.

Поддерживаемые библиотеки

«Из коробки» C2RTL поддерживает лишь небольшое количество библиотек. Опишу, как обстоит ситуация с рядом основных.

• SoftFloat. Полная поддержка версии 3e для операций с плавающей точкой (IEEE).

• STL. Поддержка ограничена. Контейнеры вроде vector поддерживаются, но map, set, list либо «не рекомендуются», либо заглушены.

• Boost. Поддерживаются отдельные функции (версия 1.57).

• I/O. Не поддерживаются. Любой код, использующий printf, fopen или iostream, не будет синтезирован для формальной верификации. Вызовы этих функций будут черными ящиками или приведут к остановке синтеза.

Дополнительные библиотеки подключать можно, но с учетом ограничений инструмента. Полный перечень поддерживаемых функций можно уточнить в мануале, а мануал получить у вендора. Из списка выше меня особенно интересовала библиотека SoftFloat, но оказалось, что встроенная версия не поддерживает RISC-V-модификации. У меня без проблем откомпилировалась версия из апстрима — а позже она успешно послужила эталоном для проверок RTL.

Заключение

Jasper C2RTL — это мощный инструмент для формальной верификации RTL-реализаций различных конвейеров. В качестве «золотой» модели C2RTL использует C++. Ключевые особенности механизма:

• Автоматизация: маршрут от компиляции C++ до генерации SVA-свойств максимально автоматизирован.

• Гибридная формальная проверка: использование word-level движков для борьбы со сложностью арифметических схем.

• Контроль корректности: генерация «санитарных» проверок, гарантирующих, что сама C++-модель синтезирована правильно.

В некоторых сценариях Jasper C2RTL позволяет довольно быстро настроить формальное окружение для тестируемого модуля и уже через несколько часов начать разбирать первые ошибки. Общие свойства формальной верификации — 100% покрытие и короткие трассы — помогают очень быстро отлаживать проблемы. А при недостатке формальных верификаторов — и вовсе выполнить верификацию силами RTL-инженера.

В качестве минусов отмечу стоимость решения. Придется занести два мешка денег в Cadence: сначала за JasperGold, а потом за отдельную лицензию C2RTL. Но, как я заявил в заголовке, мы рассматриваем формальную верификацию «для богатых».

Аналогичный инструмент — Datapath Verification — есть и у Synopsys, но я им не пользовался. Если у вас есть опыт работы с ним, будет интересно почитать о вашем опыте и сравнить с C2RTL.