注目★★★★★Hacker News
Jane Street ASIC解析、120ビットの答えをZ3で導出
30秒で把握
- 1Jane Street ASIC課題を約1か月で解析し正解「TWO STARS」を導出
- 2GDSの約1,000パスと約17,000ポリゴンをVerilog回路へ再構成
- 3120ビット入力を逆算しZ3の数千制約でシミュレーション検証
要約
著者は Jane Street のASICリバースエンジニアリング課題を約1か月かけて解き、正解「TWO STARS」を導出した。GDSファイルから約1,000個のパスと約17,000個のポリゴンを解析し、回路をVerilogとして再構成した。実課題は約10,000個の部品と81種類のコンポーネントで構成され、入力は120ビットだった。著者は回路を時間方向に逆算し、Z3に数千の制約を与えて必要な信号列を求め、シミュレーターで正解を確認した。途中でJane Streetに回路上の接続バグを報告し、実際の不具合だと確認された。
あなたへの影響
回路設計・検証に携わる日本のエンジニアは、GDS解析からVerilog化、制約充足による逆向き探索までの手順を検証材料として活用できる。
推奨：回路を制約ソルバーで解く手法は、複雑な状態遷移のデバッグや入力生成にもつながり得るため、Z3を小規模な検証回路で試す価値がある。