Jane Street раскрыла итоги ASIC-головоломки: чип проверял Star Battle

В августе Jane Street опубликовала головоломку: участникам выдали только итоговую физическую топологию небольшого чипа (файл GDS) без списка соединений (нетлиста) и имён внутренних сигналов. Нужно было восстановить, что чип делает. Теперь компания раскрыла ответ и разобрала способы решения.

Пришло около 400 работ из более чем 30 стран, больше всего из США, Индии, Великобритании и Австралии. Среди участников были школьники, исследователи, практикующие инженеры и пенсионеры. Большинство использовало KLayout, Yosys и Z3 вместе с собственными инструментами (многие написал ИИ) на Python, Rust, C++, OCaml, Haskell и даже Odin.

Чип оказался аппаратным проверяющим для головоломки Star Battle (она же «Two Not Touch») на поле 11x11: нужно поставить ровно две звезды в каждой строке, каждом столбце и каждой цветной области, причём звёзды не должны касаться друг друга, даже по диагонали. Чип принимает 121 такт входных данных, по одному на клетку, и параллельно проверяет: 2-битные счётчики для каждой строки и каждого столбца (в каждом должно быть ровно 2 звезды); 121-битное ПЗУ, сопоставляющее клетки областям, и 2-битный счётчик на каждую область; линию задержки, отслеживающую соседние клетки; счётчик общего числа звёзд для вывода пасхальных надписей. Результаты проверок объединяются логическим И в сигнал успеха. Строки вывода лежат в ПЗУ и скрыты небольшим LFSR (регистром сдвига с обратной связью), зависящим от игрового поля. При успехе логика вывода расшифровывает строку с решением и выдаёт её. Чип спроектирован на открытой библиотеке стандартных ячеек SKY130 с помощью инструмента LibreLane.

Первый шаг, извлечь из топологии нетлист на уровне вентилей. Чтобы облегчить старт, авторы оставили в GDS имена ячеек (например, sky130_fd_sc_hd__nand2_2), и проверка LVS в Magic или KLayout давала сырой нетлист. Владислав Шаповалов написал собственный конвейер извлечения на C++, отладив его на тренировочной схеме.

Далее нетлист нужно было моделировать. Одни генерировали Verilog и брали модели ячеек SKY130, другие, как Стивен Эберт, писали собственные вычислители. Выданная осциллограмма позволяла сверять результат, но совпадение с ней не гарантировало верность модели: у Алехандро Сото Франко модель на Python воспроизводила образец, хотя неверно обрабатывала все ячейки, выдающие константную единицу (их выходы оставались нулями). Это фактически отключало проверку соседства, и можно было находить «верные» поля с касающимися звёздами. Ошибку он поймал, сравнив модель с симуляцией в Icarus Verilog на дополнительных входах.

Самый ожидаемый подход, идти от выхода «успех» назад по схеме. Подсказкой служила топология: каждый «остров» соответствовал одному модулю исходного RTL. Санджай Равишанкар обвёл рамками области, разбил схему на модули, проверил границы по связности и смоделировал каждый модуль. Аарон Ши применил идею из курса сигналов и систем: подавал на нетлист «импульсы» в разных точках и сравнивал каждый триггер с базовым состоянием из нулей; так он увидел, что триггеры соответствуют строкам, столбцам и областям и каждый должен набрать ровно 2, и построил решение. Ещё один путь, SAT-решатели, которым не нужно понимать схему; Локеш Аравапалли сначала получил вход от SAT-решателя, а затем разобрал по нему устройство схемы. Габриэль Табоада реверс-инжинирил выходную часть, чтобы понять кодирование решения и нужное начальное значение.

Среди визуализаций авторы отметили средство просмотра нетлиста и топологии бок о бок от Джошуа Стэплтона, наглядный разбор сборки чипа из PMOS- и NMOS-транзисторов от Хосе Варгаса, онлайн-версию головоломки от Амрута Гулавани и интерактивную анимацию Кьяртана ван Дриля, возможно, любимую у авторов. Были и забавные работы: Александр Смоллвуд синтезировал нетлист на FPGA, Нихил Канийери скомпилировал его в командные блоки Minecraft, Дэвид Гарнер перевёл весь чип в аналоговую симуляцию SPICE, Марцин Вуйцик построил доказательство с нулевым разглашением Groth16 о владении решением.

Пасхальные яйца: два участника нашли все шесть задуманных, шестеро нашли шесть из семи, если считать ошибку с висящим проводом. Среди них: расшифровка двух неудачных попыток в example_inputs.vcd как 7-битного ASCII даёт «THE NIGHT SKY AWAITS»; дата в заголовке VCD «Sat Dec 31 23:59:60 2016» (настоящая високосная секунда); азбука Морзе на неиспользуемом слое, «PER ARENAM AD ASTRA» («сквозь пески к звёздам»); сообщения об ошибках («EMPTY SKY» для всех нулей, «BIG BANG» для всех единиц, подсказка «TWO NOT TOUCH» при соседних звёздах, иначе «TRY AGAIN»); около 1 400 изолированных квадратов на слое met2 образуют логотип Jane Street 57×57 пикселей; формы одиннадцати областей складываются в «JSC»; а неподключённый провод в тракте «TWO NOT TOUCH» изначально был ошибкой топологии, пойманной при LVS, но оставленной намеренно.

В выводах авторы пишут, что ИИ станет частью подобных задач и сильно меняет создание инструментов анализа, просмотра нетлистов и отладки. Одни участники использовали его для небольших скриптов, другие отдавали агентам всю головоломку. Когда задачу придумывали, авторы заметили, что новейшие модели при одном запросе за 30 минут или меньше выдавали итоговое решение, что, по их словам, лишает работу большей части удовольствия и пользы. Лучшими они назвали разборы тех, кто продолжал разбираться после получения ответа, и отладочные истории тех, кто сверял независимые реализации и подавал заведомо неверные входы.

Ключевые факты

• Головоломка Jane Street: по одной топологии GDS чипа без нетлиста нужно было понять, что он делает; чип оказался аппаратным проверяющим Star Battle 11x11 («Two Not Touch») на 121 такт входа.
• Получено около 400 работ из более чем 30 стран; большинство использовало KLayout, Yosys и Z3 плюс собственные инструменты, многие из которых написал ИИ.
• Подходы к решению: ручной разбор схемы от выхода назад, динамическое исследование импульсами, SAT-решатели, взлом выходного генератора с LFSR; одна модель с ошибкой в константных ячейках отключила проверку соседства.
• Пасхальные яйца: два участника нашли все шесть задуманных, шестеро, шесть из семи с учётом ошибки с висящим проводом; среди них логотип из около 1 400 квадратов и надпись «JSC» из форм областей.
• По словам авторов, при создании задачи новейшие модели решали её по одному запросу за 30 минут или меньше.

Почему это важно

Это редкий подробный отчёт о реверс-инжиниринге аппаратного обеспечения с большим числом участников и разными подходами: ручной анализ, динамическое исследование, SAT-решатели и инструменты, написанные ИИ. Авторы прямо говорят, что ИИ становится частью таких задач и меняет создание инструментов анализа и отладки, а новейшие модели на этапе подготовки решали задачу одним запросом за 30 минут или меньше.

Кому это важно

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

Как это применить

Из разбора можно взять рабочую цепочку: извлечь нетлист (Magic или KLayout с LVS, либо собственный разборщик), смоделировать его (Verilog с моделями SKY130 или свой вычислитель), сверить с образцом осциллограммы, а затем искать структуру: идти от выхода назад, подавать импульсы или использовать SAT-решатель. Совет авторов по отладке: сравнивать независимые реализации и подавать входы, которые должны давать отказ, а не только повторять примеры. Цены и условий участия в тексте нет.

Можно ли доверять

Это собственный разбор организатора, Jane Street, о его же головоломке, поэтому описание устройства чипа и пасхальных яиц исходит от авторов задачи. Оценки роли ИИ, их наблюдения, а не измерения. В видимом тексте не названы победители, призы и рейтинг работ; не указано, сколько решений были верными и сколько участников использовали ИИ. Текст оригинала в доступной версии обрывается в разделе выводов.

Риски и подводные камни

Совпадение с выданной осциллограммой не доказывает корректность модели: пример с неверными константными ячейками показывает, что ошибка может отключить целую проверку. Решение через SAT даёт ответ, но не объясняет схему. Авторы также отмечают, что решение задачи ИИ одним запросом лишает работу большей части удовольствия и пользы от неё.

«Затем сравнил каждый триггер с базовым состоянием из одних нулей. Триггеры, которые изменились, это отклик на этот один бит.»

— Аарон Ши, участник головоломки (из его разбора, приведено в посте Jane Street)