Или: почему я никогда не выбираю лёгких путей

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

Чтобы было понятнее, о чём именно пойдёт речь — вот публикация «Can you reverse engineer an ASIC?» в блоге Jane Street, с которой всё это и началось.

А если кому вдруг захочется почитать (ужасный) код, который я использовал в этом состязании, можете заглянуть в мой репозиторий на GitHub.

Вызов принят

Где‑то на задворках моей памяти пылится диплом инженера, поэтому многие из тех слов, что были в описании конкурса, оказались мне знакомы. Задача заключалась в том, чтобы взять ASIC и разобраться с тем, как именно он функционирует. Если тут есть такие, кому не знакома аббревиатура «ASIC», поясню, что расшифровывается она как (Application‑Specific Integrated Circuit, интегральная схема специального назначения). Это — всего лишь мудрёное наименование того, что обычно называют «Computer Chip» (компьютерный чип, микросхема). Компании вроде Jane Street, по‑видимому, проектируют такие чипы ради того прироста в производительности, который они дают в сравнении со стандартным оборудованием от обычных производителей.

Как бы там ни было, задача состоит в том, чтобы взять GDS‑файл с описанием чипа и методами реверс‑инжиниринга выяснить, как именно он функционирует. Затем, возможно, там обнаружится какой‑то пароль или что‑то подобное. А о том, что значит «GDS», я и раньше не знал, да и сейчас понятия не имею.

Соревнование состояло из двух частей. Первая — разминка, когда участникам дают довольно много сведений (вроде реального проекта чипа). А вторая — настоящая головоломка. Тут участников снабжают крепким рукопожатием, пожеланиями удачи и перспективами провести без сна следующие три недели.

Что находится в файлах?

По какой‑то неведомой причине я, занимаясь подобными вещами, обычно не ищу лёгких путей. Поэтому, вместо того чтобы заняться предварительными исследованиями, я сразу же начал копаться в файлах. В них мне попались кое‑какие знакомые слова, вроде «clk» (clock, тактовый сигнал), «rst» (reset, сигнал сброса), «VGND» (Ground Voltage, земля) и «VPWR» (Power Voltage, напряжение питания).

Ещё там была целая куча… чего‑то, снабжённого префиксом sky130_fd_sc_hd__, за которым шло нечто, напоминающее названия логических элементов, вроде «or» (ИЛИ) или «not» (НЕ), а также прочее подобное. Это ли те самые сведения, которые мне нужно извлечь из файла?

Мне попалась весьма приятная Python‑библиотека gdstk, которая, похоже, способна всё это читать. Она сообщила мне, что в разминочной головоломке имеется 27 элементов. Неплохо для начала!

% python3 -c 'print(len(__import__("gdstk").read_gds("warmup/04_final.gds").cells))'
27

В основной задаче ещё был файл VCD. Это текстовый файл, в котором, как мне кажется, содержатся входные или выходные данные симуляции или что‑то вроде этого. А о том, что означает аббревиатура VCD, я не знал и сейчас не знаю. В этом файле моё внимание привлекли какие‑то подозрительно выглядящие записи, содержащие ASCII‑символы. Я повозился с этим файлом, написав небольшую программку на C, после чего мне удалось вытащить из него фразу «TRY AGAIN» (попробуйте снова). Так, значит, в устройстве каким‑то образом «зашито» сообщение!

$ gcc what-is-this-thing.c && ./a.out
T R Y   A G A I N  T R Y   A G A I N

Ну, это уже что‑то.

Отвлекаюсь, впустую трачу время. А заодно и жизнь

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

Вы смело можете этот раздел пропустить. Жаль, я этого не сделал.

Несколько дней спустя

Так, я сделал симулятор схем на базе sqlite3. Приятная штука получилась. Но на Python довольно‑таки сложно проектировать электронные устройства! Если бы существовал язык для описания «железа».

Несколько дней спустя

Написан парсер для моего нового языка и теперь я могу проектировать схемы. Но их надо тестировать! Был бы способ заскриптовывать входные данные и проверять то, что получается на выходе.

Несколько дней спустя

Сделана тестовая обвязка для моего симулятора. Но так тяжело выводить на экран то, что происходит. Эх, если бы… Короче, видите, к чему всё идёт?

Несколько дней спустя

Я бросил писать просмотрщик временных диаграмм сигналов и решил просто воспользоваться Surfer Waveform Viewer. Но эти GDS‑файлы… Сложно с ними работать. Что же делать?

Несколько дней спустя

Прибегнув к библиотеке raylib, я написал простой просмотрщик GDS‑файлов, но никак не смог добиться того, чтобы блоки располагались так, как мне нужно. В итоге я понял, что слишком далеко отклонился от основной темы и что пришло время забросить самоделки.

Вот и окончился этот тяжкий раздел. Рады, что его пропустили?

Соберись, Крис. Соберись!

В блоге Jane Street упоминается довольно удобный просмотрщик GDS‑файлов. Открыв в нём файл, я просидел какое‑то время, вперив немигающий взгляд в экран и ожидая озарения. Мне удалось примерно наметить входы схемы, а позже, анализируя трассировку дорожек в файлах, получилось подтвердить, что это действительно входы. Так как это было разминочное задание, у меня была возможность сравнить то, что я знал об устройстве, с тем, что видел на экране.

Что представляют собой эти файлы?

Похоже, что в этих файлах имеется некое подобие «слоёв», состоящих из материалов разных типов, ну или что‑то подобное. Мне кажется, что это нечто вроде инструкций для 3D‑принтера, описывающих, куда надо подвести печатающую головку и на какой глубине наносить материал. Может, эти файлы и правда близки к инструкциям для некоей машины? Но в них, похоже, вместо элементов, произвольно расположенных по вертикали, используются стандартные слои фиксированного размера, что упрощает задачу.

Мне хотелось доказать, что я способен хотя бы обрабатывать эти файлы, поэтому я попытался извлечь из них логотип Jane Street, находящийся в правом верхнем углу. Задача эта оказалась несравнимо сложнее, чем я себе придумал. Мне наконец удалось извлечь абсолютно всё, за исключением этого самого логотипа. Ну да ладно. Нам ли жаловаться? Идём дальше.

Ещё я как‑то выяснил, что библиотека, которой я пользуюсь, способна извлекать элементы в виде SVG‑файлов, куда попадает и множество текстовых меток, описывающих отдельные части компонентов. Возможно, это станет ключом к решению задачи, так как я, вероятно, смогу использовать эти сведения, чтобы понять, где на схеме расположены входы и выходы.

Пришло время почитать про все эти элементы

Я понял, что, двигаясь на ощупь, дальше не пройду. Поэтому я решил, что настало время зарыться в документацию. Судя по всему, официальный источник знаний обо всём, что мне требовалось, находился на странице sky130-unofficial, несмотря даже на слово «unofficial» в её названии.

В документации нашлись ответы на многие из моих вопросов. Ну почему я сразу не пошёл прямо сюда?

Оказалось, что таинственное «sky130» — это нечто вроде стандарта или описания некоего набора технологий для производства микрочипов. Подозреваю, что создавать чипы — дело нелёгкое, поэтому тут есть смысл в использовании стандартизированных элементов. Очень важно, что в документации было описание функционала элементов. В случае с чем‑то вроде элемента «and», который, вероятно, представляет собой логический вентиль И, всё выглядит довольно‑таки просто, а вот штуковина с названием «o21bai» — это… сразу и не поймёшь, да нам оно, в общем‑то, и не нужно.

Используя сведения из документации и текстовые метки из SVG‑файла, я теперь могу хотя бы приблизительно сопоставить геометрические объекты со входами и выходами элементов исследуемой схемы. Это, полагаю, первый шаг к тому, чтобы превратить описание в нечто реальное. Тут мне несказанно повезло, так как применяемая мной библиотека умеет проверять, перекрываются ли элементы в двумерном пространстве (не забывайте, что GDS‑файлы описывают трёхмерные структуры).

Я не был полностью уверен в предположении, что метки накладываются точно на описываемые ими элементы, но всё оказалось куда лучше, чем я ожидал! Похоже, метки были помещены точно над центрами элементов! Система обнаружила даже некоторые объекты, которые чисто визуально соединёнными не казались, то есть простой осмотр схемы не помог бы узнать, что они соединены друг с другом. А когда смотришь лишь на порты ввода/вывода всей схемы, картинка оказывается гораздо чище, чем раньше.

Полагаю, теперь можно построить граф соединений?

Теперь, похоже, у меня есть всё необходимое для того, чтобы извлечь описание устройства из GDS‑файла. Задача эта не из лёгких. Тут имеется тысяча соединений и почти 17 тысяч полигонов, и это даже без всего того, что меня не интересует.

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

Мой алгоритм — это просто ужас, но с работой он пока справляется. Я тут, кроме прочего, упростил схему, а именно — взял все «провода» и… не знаю, объединил ли, сплавил ли их в один проводник. Логика тут в том, что если дорожки соприкасаются, то в моём представлении это один проводник.

К моей удаче, я в прошлом году, пока был без работы, потратил несколько недель на решение задач с LeetCode, поэтому алгоритмам на графах меня не запугать и не замедлить.

Много дней спустя

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

У меня начало получаться преобразовывать граф соединений в описание аппаратуры на языке, называемом Verilog. Это, вдобавок, позволило мне запускать простые симуляции, вроде проверки того, что «перевод этого пина в высокое состояние переключает другой пин в низкое». Я в итоге смог вытащить из файлов сведения о расположении всех компонентов. Выглядело это всё как комок спагетти, поэтому я занялся ручным рисованием соединений.

Я не пользовался специальными инструментами (ну, за исключением excalidraw, любимой программы для рисования). В основном я действовал так: просто вглядывался в схему до тех пор, пока не начинал видеть в ней какой‑то смысл. Я, как обычно, не искал лёгких путей.

На этой картинке не хватает лишь одного: остатков рассудка.

В итоге я понял, что представляют собой основные компоненты разминочной задачи. Это были два сдвиговых регистра (сдвигают данные), сумматор (отвечает за сложение чисел) и компаратор (сравнивает то, что ему предложат). Тогда я занялся симуляцией выходов устройства. Я знал, что входные сигналы должны дать в сумме 496, так как компаратору было дано имя comparitor496. Поэтому, чтобы достичь цели, нужно было лишь подать на вход правильную последовательность битов. Это — простая математика, а настоящая сложность заключалась в том, чтобы заставить все компоненты работать в одной упряжке в рамках единой симуляции.

Эх, был бы какой‑то способ это сделать, не рискуя при этом окончательно свихнуться.

Прошло несколько часов и всё получилось! Схема наконец заработала!

Тогда я понял, что у меня есть шанс решить основную головоломку. Но время было не на моей стороне, да и мой иммунитет к тому моменту начал сдавать.

Переход к основной задаче

В основной головоломке имелось гораздо больше типов элементов, чем в разминочной (что‑то около 81 против 20), да и по количеству их тоже было больше (почти 10 000 против 1000). Легко эту задачу не решить. Мне удалось быстро переделать под новые условия «разминочные» скрипты, правда для этого пришлось отключить всю валидацию. Ход, конечно, не самый лучший, но как временное решение — сойдёт. Хуже было то, что процесс извлечения сведений о схеме устройства теперь занимал почти целую минуту, хотя раньше на это уходила всего пара секунд.

Начало работы

Мне удалось одержать небольшую победу над задачей, переработав шаг, на котором я получал сведения о соединениях, сделав его в 100 раз быстрее (ускорив с 3,4 секунд до 0,03 секунд). То, что получилось, до байта повторяло то, что было, поэтому я был уверен, что эта доработка не сопровождалась появлением новых ошибок. Правда, это улучшение выглядело не очень‑то заметным на фоне громадного времени, необходимого на выполнение основного шага. Поиск всех соединённых компонентов по‑прежнему занимал почти минуту. К счастью, я, после кошмара, через который прошёл, решая разминочную задачу, был вполне уверен в результатах работы этого шага, поэтому мне не нужно было выполнять его слишком часто.

Извлечение схемы основной задачи

Времени это заняло немало, но в итоге мне удалось добавить в проект реализацию примерно четырёх десятков новых компонентов, необходимых для решения реальной задачи. Я просто вручную копировал их с сайта документации. Сейчас мне ясно, что я мог скопипастить их откуда угодно, но (если кто не помнит), лёгкие пути — это не для меня.

После этого, внеся в проект некоторые улучшения, повышающие удобство работы, вроде имён или псевдонимов для дорожек, я смог построить и запустить симуляцию для основной задачи. Работать она отказалась, но, несмотря на это, ощущалось, что я в одном шаге от решения.

Баг в задаче?

Меня расстраивало лишь то, что пришлось отключить валидацию. А без этого сложно двигаться вперёд, так как в схему могут попасть ошибки, которые можно заметить лишь через несколько часов или дней. Поэтому я попытался снова включить проверки. Например, на одном из этапов проверялось, чтобы абсолютно все линии были к чему‑нибудь подключены.

На одном из участков схемы я обнаружил проводник без источника сигнала. Это значило, что его состояние совершенно неизвестно моей симуляции. Очень странно. Ведь даже если сигнал в каком‑то проводнике нас и не интересует, его обычно подключают к чему‑то, выдающему некий известный сигнал, а не оставляют «висящим в воздухе». Я предположил, что это — результат ошибки в моём алгоритме выявления пинов, но при внимательном осмотре схемы оказалось, что моя программа правильно нашла проводник, который подключён лишь к двум входным пинам и ни к чему больше.

А что ещё страннее — в схеме имелось подключение к соседнему пину, который даже не являлся входным или выходным! Может, это баг и этот пин должен быть подключён к одному из входов? Я разбирался в этом всём весьма поверхностно, но, преодолев смущение, сообщил об ошибке в Jane Street.

Надпись на схеме у красного кружка: «Не должно быть соединено?» Надпись у линии: «Не подключён?»

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

Взгляд с высоты птичьего полёта

Я потратил немало времени, размещая на схеме крупные узлы и проводники, соединяющие их. После этого всё начало как‑то складываться. Мне удалось выяснить, что узел, выдающий сигнал успеха, подключён к 6 проводникам. Задача теперь слегка упростилась, сведясь к «как перевести эти 6 линий в высокий уровень?» К счастью, две из них переходили в состояние логической единицы после определённого количества тактовых сигналов, то есть оставалось разобраться лишь с четырьмя.

Я обнаружил и другие закономерности. Самый левый узел, похоже, работает как генератор сигналов, которые затем передаются в другие части схемы. Выходит, «пароль» скрыт в структуре этих элементов?

Объединив три таких узла, я выяснил, что до момента перевода выхода в высокий уровень проходит 121 или 120 переключений тактового сигнала. Это соответствовало временной диаграмме из задания. Возможно, правильный пароль нужно передать схеме за определённое количество тактов, а если этого не сделать, будет выведено некое сообщение?

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

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

Оказалось, что я — идиот

Общую схему, собранную из отдельных компонентов, всё не удавалось запустить, несмотря на то, что я два или три дня тщательно эти компоненты тестировал. А оказалось, что я просто забыл установить в высокое состояние пин «reset». В результате всё устройство попросту не включалось. Это — как забыть завести машину, а потом удивляться, почему она не двигается.

Я это исправил и тут же, как ожидалось, увидел сообщение «TRY AGAIN». Вот он — успех!

А ещё интереснее было то, что, когда я убрал входные данные, подаваемые на схему, оказалось, что в ней запрятаны и другие сообщения:

Хандра

Я добрался до самой сложной части испытания. Оказалось, что входы схемы рассчитаны на 120 бит, и у меня совершенно не было идей касательно того, куда двигаться дальше. Я уже подумывал о том, чтобы просто перебрать все входы, но это, к сожалению, заняло бы больше времени, чем имеется в распоряжении всего человечества.

Провод за проводом

Я пробовал отследить сигналы в направлении от выходов ко входам схемы, но отказался от этой затеи из‑за слишком сложной конфигурации входов. Мне нужен был какой‑то другой, новый подход. В какой‑то момент я, в рабочих заметках, задался вопросом о том, что произойдёт, если я запущу симуляцию задом наперёд. Меня захватила эта идея.

Дело тут в том, что мне известно то, каким должен быть сигнал на выходе, и то, какими должны быть в этот момент входы.

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

Это похоже на рекуррентное соотношение, но я при этом знаю о том, каким должен быть выход на шаге 120, и о том, что в начале работы все линии выхода установлены в ноль. Поэтому, чисто теоретически, эту задачу можно решить математическими методами.

Надеюсь, следующая схема окажется понятнее рассуждений.

Signal I Understand (Сигнал, который мне понятен).

Some Complicate Set of Things (Некий сложный набор компонентов)

Input (Вход).

Clock (Тактовый сигнал).

Output (Выход).

Signal I care about (Интересующий меня сигнал).

Я сосредоточился на сдвиговом регистре, так как он больше всего напоминает то, с чем мне удалось разобраться, решая разминочную задачу (отличный педагогический ход, поэтому говорю «Спасибо!» Бену и Анишу!). Но тут обнаружились сложные ограничения, похоже, зависящие от предыдущих значений в сдвиговом регистре. Чтобы решить эту задачу, вероятно, потребовался бы решатель задач удовлетворения ограничений. Такие штуки известны своей запредельной сложностью, но я, к счастью, был знаком с одним очень хорошим инструментом из этой серии.

Об использовании электронных таблиц для написания Verilog‑кода

Сразу прошу прощения за то безобразие, которое собираюсь показать.

Да, это электронная таблица. Я использовал её для написания Verilog‑кода, который потом передал в симуляцию. Удивительно, но если разобраться с внутренним устройством электронных таблиц, оказывается, что сами они являются весьма продвинутыми решателями задач удовлетворения ограничений. Я выгрузил выходные данные в файл Verilog, и… сработало! Как минимум для двух проводников. Было понятно, что, в целом, этот метод недостаточно эффективен, так как он требует, чтобы я сам проверял результаты и переключал биты до тех пор, пока все проверки не начинали показывать успешный результат. Но я доказал, что подход «обратного» решения задач, подобных моей, жизнеспособен.

А теперь пришло время вызывать тяжёлую артиллерию и учиться пользоваться решателем задач удовлетворения ограничений.

Всё это… не так сложно, как я ожидал?

Я вспомнил, как читал о решателях ограничений в блоге Хиллела Уэйна (у него вышла новая книга — советую купить! Я себе взял), но меня подобные материалы всегда пугали своей сложностью. Там используются заумные слова, вроде «ограничения» и «решатель», а мне просто нужен инструмент для решения задачи… И тут до меня наконец‑то дошло!

В итоге я воспользовался инструментом под названием z3. Это какое‑то волшебство? Каждый раз, когда он находит решение, меня прямо‑таки переполняет счастье. Говоришь ему: «На этой линии никогда не должно быть нуля» или «На этой линии должна быть единица на шаге 120», и он либо находит способ сделать то, что от него просят, либо сообщает о том, что это невозможно. В итоге я смог передать ему тысячи ограничений, а он мгновенно находил решения.

Правда, отлаживать его — сущий кошмар. Всё, в основном, выглядело так: я усиленно размышлял и удалял ненужные строки до тех пор, пока система снова не начинала работать. Со временем я даже начал примерно понимать то, чего можно ожидать от решателя. В частности, если я не задавал исходные значения — он выбирал те, которые были удобными для него (и неудобными для меня).

Ещё меня замучило то, что я переносил данные из схемы в z3 вручную. Я сам не вполне понимаю, почему поступал именно так. Возможно, к тому моменту я уже настолько устал, что сам себе не доверял и не решался написать скрипт для преобразования данных.

Я разобрался с каждой из интересующих меня линий. Было примерно 24 таких, которые должны были одновременно находиться в высоком состоянии. Мне довольно легко удалось добиться этого для 22 из них, рассматривая каждую линию отдельно. Я сочетал использование решателя с собственными догадками, а потом проверял то, что получалось.

Оказалось, что я, как обычно, выбрал самый сложный путь

Выяснилось, что структура входных сигналов для многих элементов требует подачи всего двух импульсов в моменты, кратные 11, причём конкретный момент задаётся значением счётчика. Если бы я просто чуть дольше наблюдал за входами, то, возможно, понял бы это раньше. А я слишком сильно увлёкся более глубокими уровнями системы, упустив из вида то, что было прямо передо мной.

Ответ найден. Задача решена

Я объединил все ограничения в один гигантский скрипт и занялся борьбой с ошибками. Их оказалось не так уж и много. В 10 вечера я, вместо сообщения об ошибке, увидел следующее:

% python3 solver.py
Solution!
verilog saved to 'out.txt'

От волнения у меня затряслись руки, так как на данной стадии работы такой ответ скрипта мог означать только одно: решение найдено.

Я загрузил код в симуляцию, запустил её. Вот он — ответ: (* TWO STARS *).

Я написал в Jane Street. Следующим утром пришло подтверждение правильности решения. Теперь можно добавить ответ в таблицу:

Что дальше?

Я даже и не знаю, во что ещё ввязаться. Мне эта задача очень понравилась, но у меня есть и другие хобби, вроде «ложиться спать до трёх утра». В блоге Jane Street сказано, что в течение пары месяцев планируется провести новое испытание, так что следите за новостями!

Если у вас есть идеи каких‑нибудь интересных проектов — свяжитесь со мной через Hacker News или по электронной почте.

А если вы живёте в Сиднее и вам всё это было интересно — дайте знать. Может, поболтаем за чашкой кофе.

О, а приходите к нам работать? ? ?

Мы в wunderfund.io занимаемся высокочастотной алготорговлей с 2014 года. Высокочастотная торговля — это непрерывное соревнование лучших программистов и математиков всего мира. Присоединившись к нам, вы станете частью этой увлекательной схватки.

Мы предлагаем интересные и сложные задачи по анализу данных и low latency разработке для увлеченных исследователей и программистов. Гибкий график и никакой бюрократии, решения быстро принимаются и воплощаются в жизнь.

Сейчас мы ищем плюсовиков, питонистов, дата‑инженеров и мл‑рисерчеров.

Присоединяйтесь к нашей команде