T27.AI

Блог

Задняя половина openXC7 из спека: FASM в кадры и в битстрим

2026-10-03 · 8 мин чтения

[один дизайн на одной плате, эквивалентность, а не лучший битстрим; время на одном занятом ноутбуке, отношения грубые; скорость fpga-assembler — из его README, не наша] openXC7 превращает FASM в битстрим Xilinx 7-series двумя инструментами prjxray: fasm2frames на Python и xc7frames2bit на C++. Мы пересобрали эту половину так, что каждая позиция бита, адрес кадра и слово пакета берутся из трёх t27-спеков. Против двух инструментов она совпадает байт в байт на 22 из 22 файлов FASM и 16 из 16 файлов кадров и быстрее примерно в 6–14 раз на небольших настоящих дизайнах, примерно в 85 раз на дизайне в 121 587 строк и до примерно 200 раз на синтетических тестах. Сравнение нашло тихий заворот битов в fasm2frames (f4pga/prjxray#2574), отсутствующую проверку микросхемы в xc7frames2bit (#2573) и наш собственный баг на kintex7. На плате AX7203 (XC7A200T) .bit, записанный так для дизайна в 121 587 строк, совпал с openXC7 байт в байт, загрузился в SRAM и вернул 403 200 из 403 200 помеченных квитанций.

openXC7 собирает битстрим Xilinx 7-series в две половины. Первая — yosys и nextpnr: на входе Verilog, на выходе FASM. FASM — это текстовый список фич вроде CLBLM_R_X3Y0.SLICEM_X0.ALUT.INIT[63:0] = 64'h.... Вторая половина превращает этот список в битстрим. fasm2frames из prjxray (Python) находит биты каждой фичи и пишет конфигурационные кадры, а xc7frames2bit (C++) упаковывает кадры в конфигурационные пакеты. Мы переписали вторую половину так, что каждая позиция бита, адрес кадра и слово пакета берутся из t27-спека, и сравнили её байт в байт с двумя инструментами, которые она заменяет.

Что лежит в спеках

• packets.t27: поток конфигурационных пакетов. Заголовки, регистры, команды, CRC и последовательность записи, которую использует xc7frames2bit.
• far.t27: обход адресов кадров для xc7a35t, xc7a100t и xc7a200t; микросхема выбирается по IDCODE.
• frames.t27: ECC кадра и то, куда бит из базы попадает в кадре. Это смещение тайла в словах, сдвиг псевдонима у тайла *_SING, тайл, который начинается ниже своего кадра, и что происходит с битом, который выпадает за его пределы.

Драйвер, bitwalk, написан на Rust. t27c gen-rust генерирует его функции-правила из этих спеков. Грамматика FASM, поиск фич, файловый ввод-вывод и текстовый вывод написаны руками; битовая арифметика — нет. Каждый раздел спека ссылается на файл и строку prjxray, которые он воспроизводит (prjxray c9f02d857, prjxray-db 517d66a).

Измерено

Мутационный гейт ещё раз окупился, пока писался этот пост. Поддержка kintex7 изменила то, как драйвер считает биты за пределами тайла, и один внесённый дефект выжил: окно тайла на одно слово длиннее. Тесты спека его поймали, а прогон по корпусу — нет, потому что новый счётчик поглотил ровно тот бит, который сдвигал дефект. Теперь счётчик разделён на два, так что у тайла, который начинается внутри своего кадра, собственные биты никогда не окажутся снаружи, и дефект снова ловится.

Скорость

Синтетические файлы не длиннее настоящего дизайна, около 1 100 строк против 1 785, но fasm2frames тратит на них в 12–45 раз больше времени. Мы не профилировали, почему, и о причине ничего не утверждаем. Ещё мы перезасекли fasm2frames на трёх файлах при той же нагрузке, что и наши прогоны: 3,4 с, 32,5 с и 104,4 с — это делает отношения больше, а не меньше. На графике оставлены меньшие.

Что ещё делает эту работу

Найдено по дороге

Дифференциальное сравнение полезно только тогда, когда стороны расходятся. Три раза они разошлись, и каждый раз дефект был у инструмента, с которым мы сравнивали.

• fasm2frames не отвергает фичу сайта, которого нет у тайла *_SING. На нижнем SING-тайле биты заворачиваются в слова 99–100 кадра, которые принадлежат другому тайлу. На верхнем SING-тайле они отбрасываются. Код выхода в обоих случаях 0, и воспроизводится это одной строкой FASM. Сообщено в f4pga/prjxray#2574. На kintex7 то же самое: в одном синтетическом файле 337 завёрнутых и 356 отброшенных битов. bitwalk по умолчанию пишет те же байты, поэтому 22/22 выше и держится; --strict отвергает файл и называет строку.
• xc7frames2bit принимает кадры для чужой микросхемы: кадры xc7a100t с микросхемой xc7a200t дают код выхода 0 и 192 лишних кадра. bitwalk их отвергает. Сообщено в f4pga/prjxray#2573, исправления в openXC7/prjxray#27 и #28.
• В случае 05 из lromor/fpga-assembler#49, 83-битном значении RXCDR_CFG, собственные кадры fpga-assembler отличаются от эталона: 18 битов не хватает, 5 лишних. bitwalk совпадает с эталоном. Наше прочтение исходников: парсер упаковывает длинный двоичный литерал в 64-битные слова со старшего конца, так что для 83 битов первое слово содержит только младшие 19 битов. Эмуляция такой упаковки даёт ровно 18 недостающих и 5 лишних битов.

Один дефект был наш. В сетке тайлов kintex7 есть четыре тайла, которые начинаются на 2 слова ниже своего кадра, а наш драйвер читал смещение как беззнаковое и останавливался. Теперь спек говорит, как размещаются биты такого тайла (seg_shift), и к этому есть тест.

На плате

Совпадение файлов — это утверждение о файлах. Чтобы проверить цепочку на железе, мы собрали один настоящий дизайн для ALINX AX7203 (XC7A200T): trinet node 0, 121 587 строк FASM, 20 230 кадров. На этом FASM bitwalk снова совпал с openXC7 байт в байт и по кадрам, и по .bit, и занял около 0,8 с там, где fasm2frames занял около 68 с, на хосте, который всё это время был занят. Затем openFPGALoader загрузил .bit от bitwalk в SRAM по JTAG, без записи во флеш, и FPGA сообщила DONE.

tri x7-board · t27 back half on the AX7203

Поскольку два файла .bit идентичны, это не показывает ничего, чего не показал бы файл openXC7. Утверждение — эквивалентность на одном дизайне на одной плате, а не лучший битстрим. Передняя половина, yosys и nextpnr-xilinx, принадлежит openXC7 и не менялась.

Чего это не показывает

• На плате прогнан один дизайн. Все остальные проверки выше сравнивают файлы.
• Кроме дизайна для платы, в корпусе нет FASM для xc7a200t, и нет эталона Vivado для xc7a100t и xc7a200t. Там «байт в байт» значит «как у инструментов prjxray», а не «как у Vivado».
• Правило для тайла, который начинается ниже своего кадра, покрыто только тестами спека. Ни один бит из базы не попадает в эти тайлы kintex7, так что корпус его не проверяет.
• Грамматика FASM и поиск фич — написанный руками Rust, проверенный корпусом, а не выведенный из спека.

Поработаем вместе

Хотите так же проверить собственный дизайн?

Я аудирую RTL и строю независимые побитово точные модели, затем провожу результат через синтез и, когда это полезно, проверяю на плате Artix-7. Первый модуль проверки — бесплатно.

Обсудить задачуУслуга верификации