‏مهندسی معکوس یه چیپ برای حل چالش Jane Street

Jane Street هر چند وقت یه بار چالش می‌ذاره، و این یکی نویسنده رو یه ماه تمام گرفتار کرد. صورت چالش ساده‌ست: یه فایل GDS بگیر، که توش هندسهٔ یه ASIC توصیف شده (ASIC یعنی چیپی که برای یه کار خاص طراحی شده)، و از روش بفهم اون چیپ چی کار می‌کنه و رمزی که توش قایم شده چیه. چالش دو بخش داره: یه warmup که طرح مدار رو هم بهت می‌دن، و پازل اصلی که فقط برات آرزوی موفقیت می‌کنن.

اولش بدون هیچ تحقیقی افتاد تو خود فایل‌ها. با کتابخونهٔ پایتونی gdstk فایل GDS رو خوند و دید warmup ۲۷ المان داره. اسم المان‌ها با پیشوند sky130_fd_sc_hd__ شروع می‌شد؛ بعدتر فهمید sky130 یه کتابخونهٔ استاندارد المان‌های چیپه و مستنداتش می‌گه هر المان چی کار می‌کنه. همین مستندات و برچسب‌هایی که کتابخونه به SVG صادر می‌کرد، کلید کار شد: با اون‌ها می‌شد فهمید هر تکه هندسه ورودی و خروجی کدوم گیته.

مرحلهٔ بعدی ساختن گراف مدار بود. منطقش اینه که هر دو تکه که روی لایه‌های مجاور هم‌پوشانی دارن، عملاً به هم وصلن، و هر چند تکه سیم که به هم می‌چسبن یه سیم واحد حساب می‌شن. همین مرحله روی پازل اصلی با حدود ۱۰ هزار المان نزدیک یه دقیقه طول می‌کشید، در حالی که روی warmup دو ثانیه بود. نویسنده بعد گراف رو به Verilog برگردوند تا بشه سیمولیشن گرفت. وسط همین کار یه سیم پیدا کرد که هیچ چیزی اون رو درایو نمی‌کرد، به Jane Street گزارش داد و فرداش تأیید گرفت که واقعاً باگ خودشونه.

بخش خنده‌دار پست اعتراف خود نویسنده به بیراهه رفتنه: برای این چالش یه سیمولاتور مدار روی sqlite3 نوشت، بعد یه زبان توصیف سخت‌افزار و پارسرش، بعد یه هارنس تست، بعد یه نمایشگر موج، و بعد یه نمایشگر GDS با raylib، و آخر همه‌شون رو دور ریخت و برگشت سر ابزارهای آماده. خودش می‌گه همیشه کارها رو از سخت‌ترین راه انجام می‌ده. حتی چند روز گیر کرده بود چون یادش رفته بود پین reset رو ست کنه، درست مثل اینکه ماشین رو روشن نکنی و تعجب کنی چرا حرکت نمی‌کنه.

سخت‌ترین قسمت، پیدا کردن ورودی ۱۲۰ بیتی درست بود؛ امتحان کردن همهٔ حالت‌ها از عمر بشر بیشتر طول می‌کشید. ایدهٔ نویسنده این بود که سیمولیشن رو برعکس اجرا کنه: می‌دونه خروجی تو کلاک ۱۲۰ باید چی باشه و می‌دونه مدار از صفر شروع می‌شه، پس هر قدم به عقب، خواسته‌ش رو به تابعی از قدم قبلی بازنویسی می‌کنه. اول این کار رو با یه اسپردشیت انجام داد (به شوخی می‌گه اسپردشیت‌ها زیر پوستشون constraint solverهای قدرتمندی هستن) و بعد سراغ z3 رفت، که هزاران قید رو در چشم‌به‌هم‌زدنی حل می‌کرد.

نکات کلیدی:

• ورودی مدار ۱۲۰ بیت بود و جواب درست پیام (* TWO STARS *) رو روی خروجی می‌ساخت
• پازل اصلی حدود ۱۰ هزار المان از ۸۱ نوع داشت، در مقابل حدود ۱۰۰۰ المان و ۲۰ نوع در warmup
• استخراج مدار با هم‌پوشانی هندسهٔ لایه‌های مجاور و یکی‌کردن سیم‌های چسبیده انجام شد
• ورودی‌های دیگه پیام‌های دیگه می‌دادن: همه صفر EMPTY SKY، همه یک BIG BANG، جواب غلط TRY AGAIN
• نویسنده وسط کار یه سیم پیدا کرد که هیچ چیزی درایوش نمی‌کرد و Jane Street تأیید کرد باگ خودشونه