一颗芯片，藏着一个 11×11 的谜题——有人为它花了一个月

目录

• 一份 GDS 文件，和一个叫「逆向」的词
• 先学会读图，再学会造工具
• 一个 bug 报告，成了他最得意的技术成就
• 用电子表格写硬件描述语言
• z3：把「我想要什么」翻译成数学
• 答案是一个 OCaml 注释
• 我在服务器上跑了一个缩小版
• 为什么「最难的路」反而是最快的路

一份 GDS 文件，和一个叫「逆向」的词

9 月 4 日，一个叫 Chris（网名 anitil）的悉尼工程师，在个人博客上发了一篇长文：《论解决 Jane Street 逆向工程挑战》。标题下面还有一行小字——「或者说：为什么我总把事情搞复杂」。

Jane Street 是家很出名的量化交易公司。它每隔一阵子就丢出一个挑战，让全世界的人来解，解出来的人能进它的候选名单。这次的题目有点不一样：它给了一份 GDS 文件。

GDS 是芯片制造领域的文件格式，全称 Graphic Data System II，1970 年代由 Calma 公司发明，到今天还是芯片设计工具链里的通用语。简单说，一份 GDS 文件就是一颗芯片的「施工图纸」——每一层是什么材料、走线怎么铺、元件放在哪，全在里面。Jane Street 给参与者的是一个真实的、未公开的 ASIC（专用集成电路）设计文件，要求是：把它逆向出来，搞清楚这块芯片是干什么的，然后找到藏在里面的东西。

Chris 一开始连 GDS 是什么都不知道。他自己在文章里写：「我到现在也不知道 GDS 是啥的缩写」——后来评论区有人告诉他，他才补上。他有一张电气工程的学位，但从来没干过电气工程的活。

他接下了这个挑战，然后花了一个月。

先学会读图，再学会造工具

挑战分两部分：一个热身题（warmup），信息给得多一些；一个真谜题，几乎什么都不给。热身题的文件里有 27 个元件，Chris 用 Python 的 gdstk 库把它们读了出来，顺便发现了一个叫 vcd 的文件——他也不知道这缩写是啥，但往里一翻，看到一串像 ASCII 字符的东西。他写了段 C 程序跑了一下，输出是：

T R Y   A G A I N

原来电路里藏着信息。它会对你的输入说「再试一次」。

接下来他干了一件很符合他自嘲风格的事：自己写了一个电路模拟器。 理由很简单——「因为我想」。他先用 sqlite3 当驱动写了一个，然后发现用 Python 设计电路太痛苦了，于是又写了一个描述硬件的语言，然后又写了一个测试脚本的 harness，然后又想写波形查看器……写到一半他放弃了，改用现成的 surfer。他给自己这段经历起的标题是「Getting Distracted and wasting my time. And my life.」——分心、浪费时间、浪费生命。但这段弯路不是白走的，他借此把 GDS 格式的底层结构摸了个透。

真正的转机来自 Jane Street 博客推荐的 GDS 查看器。

他把整个布局放大看了很久，对照已知信息把输入输出端口标了出来。他注意到文件里的元件名字都带 sky130_fd_sc_hd__ 前缀——这是 Google 开源的 SkyWater 130nm 工艺库的标准单元命名。他顺着这个线索找到了文档，终于搞明白这些元件每个是干什么的：and 是与门，o21bai 是某种复杂的或非门组合。

最妙的一步在这里：他用 SVG 提取了元件的标注信息，然后用库函数检查两个元件在二维空间里是否重叠。GDS 本质上是三维几何的描述，元件之间的连接关系就藏在「相邻图层上的重叠」里。这个假设一开始他不确定对不对，但跑出来的结果好得出奇——甚至找出了一些肉眼根本看不出来的连接。「视觉检查永远发现不了它们。」

一个 bug 报告，成了他最得意的技术成就

把几何转成电路图之后，热身题的结构清晰了：两个移位寄存器、一个加法器、一个比较器。

比较器的名字直接叫 comparitor496——它要求输入的总和等于 496。Chris 把各个部分拼进一个模拟器，跑通了，输出了正确的波形。

他管那个时刻叫「I knew I had a chance」——我知道我有戏了。

真正的谜题规模大了一个数量级：81 种元件类型（热身题只有 20 种）、接近一万个元件（热身题只有一千个）。他的提取脚本从 2 秒变成了将近一分钟。他把电路提取出来、接上模拟器，第一次跑——不对。他花了整整两三天排查，最后发现原因蠢得惊人：忘了设置 reset 引脚。整个电路一直处于禁用状态。「就像忘了发动汽车，然后纳闷为什么车不走。」

修好之后，「TRY AGAIN」如期而至。他甚至发现了更多彩蛋：

输入	输出
错误答案	TRY AGAIN
全 0	EMPTY SKY
全 1	BIG BANG
正确答案	待定

但真正让他骄傲的不是这些。他在模拟器里发现了一条悬空的导线——它只连着两个输入引脚，却没有被驱动。旁边的引脚更奇怪：既不是输入也不是输出。他抱着「我大概是看错了」的心情给 Jane Street 发了封邮件报告这个 bug。

第二天，回复来了：你是对的。 那确实是一个 bug，只是不影响最终结果。

「我真心觉得这个 bug 报告可能是我最酷的技术成就之一。」他写道。

用电子表格写硬件描述语言

接下来是整场挑战最难的阶段：输入有 120 位，穷举是不可能的。Chris 试过把输出导线一路往回追，但复杂度超出了他的能力。

他想到一个逆向的思路：既然我知道第 120 步的输出应该是什么，电路又是从全零起步的，那我能不能倒着推？ 这本质上是个递推关系——每一步的输出可以写成上一步状态的函数。理论上可解，但需要约束求解器。

然后他做了一件让评论区全体起立的事情：

他用 Google Sheets 写 Verilog。

「我为接下来要展示的东西道歉。」他在文章里写道。那是一张电子表格，里面密密麻麻的公式，生成了一段 Verilog 代码，再喂给他的模拟器跑。

「没想到吧，电子表格底下其实是个相当精密的约束求解器。」这段「歪门邪道」证明了倒推的思路可行，但撑不了全局——它太依赖人眼盯着输出手动翻 bit。

是时候上重武器了：约束求解器。

z3：把「我想要什么」翻译成数学

z3 是微软研究院开发的一个定理证明器，准确说是 SMT（可满足性模理论）求解器。Chris 早就听说过它，但一直被「约束」「求解器」这种大词吓住。「我只需要一个能解约束的东西——哦，我懂了。」（原文：I just need a thing to solve the constraints in my - ooooh I get it!）

用 z3 的感觉，他自己形容是「有点魔法」：「每次它找到一个解，我都会涌起一阵狂喜。你告诉它『这条线永远不能为低』『这条线在第 120 步必须为高』，它要么找出怎么做到，要么告诉你做不到。」

他最后给 z3 喂了几千条约束，求解几乎是一眨眼的工夫。但也付出了代价：电路到 z3 的翻译大部分是他手写的。「我已经病得不太信任自己能写转换脚本了。」

最终，他把所有约束合成一个巨大的脚本，修掉最后几个 bug，在晚上 10 点跑出了：

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

「我的手开始发抖，因为到这一步，它能有解，只可能是因为我拿到了答案。」

他把结果喂回模拟器——答案出现了：

(* TWO STARS *)

答案是一个 OCaml 注释

这个答案有两层意思。

表层：TWO STARS 是谜题的答案——两颗星。评论区有人指出，这块芯片其实是一个 11×11 Star Battle 检查器：一个 11×11 的格子，每行、每列、每个区域都要恰好放两颗星，而且星与星不能相邻（包括斜对角）。输入的那 120 位就是棋盘状态，芯片的工作就是判断这个棋盘是不是一个合法的 Star Battle 解。彩蛋也对上了：错误的棋盘 → TRY AGAIN，全空棋盘 → EMPTY SKY，全满棋盘 → BIG BANG。还有人发现芯片布局里藏着摩斯电码。

里层：(* ... *) 是 OCaml 的注释语法。Jane Street 是全球最大的 OCaml 使用者——它用这门语言写交易系统，连自己的芯片设计工具链（Hardcaml）都是用 OCaml 写的。所以答案本身就是一个 OCaml 注释：一颗藏了两颗星的芯片，用雇主最爱的语言的语法，说「答案在这」。

Chris 把答案发给 Jane Street，第二天早上收到了确认邮件。他把表格里的「待定」改成了 (* TWO STARS *)。

他在 HN 上说：他特意问了 Jane Street 能不能发文章，对方让他等到工作日结束再发，怕剧透。他 5:30 发的。

我在服务器上跑了一个缩小版

读完全文，我决定自己验证一遍这条链路的每一环——不是用真芯片（我这儿可没有），而是用 z3 在服务器上复现「Star Battle 检查器」的核心逻辑。

第一环：11×11 的 Star Battle 到底有多少解？

我写了 30 行 z3 脚本，规则照抄：每行恰好 2 星、每列恰好 2 星、星与星（含对角）不相邻。跑：

=== 实验 1：11x11 Star Battle（无区域约束）解的数量 ===
前 3 个解用时 0.14s（只枚举前 3 个，实际解远多于此）
解 1:
  ·······★·★·
  ·★···★·····
  ········★·★
  ···★·★·····
  ·······★·★·
  ·★·★·······
  ········★·★
  ····★·★····
  ★·★········
  ····★·★····
  ★·★········

0.14 秒。三行约束（行、列、不相邻）就把 11×11 的棋盘塞进了一个解空间，z3 像开挂一样往外吐解。这让我理解了 Chris 说的「狂喜」——你描述规则，机器负责剩下的，而「剩下的」是 2^121 种可能的棋盘。

第二环：热身题的 496 到底特别在哪？

comparitor496——为什么是 496？我算了算：

1+2+...+31 = 496 == 496? True
496 的二进制: 0b111110000
496 的真因子: [1, 2, 4, 8, 16, 31, 62, 124, 248]
真因子之和: 496 == 496? True

496 是第 31 个三角数（1 加到 31），同时是完全数——它的真因子之和恰好等于它自己。这大概是 Jane Street 的工程师选它的原因：一个本身就「完美」的数字，用来当校验和，还挺符合这家公司的气质。

第三环：答案为什么是 (* TWO STARS *) 而不是 TWO STARS？

这不需要跑代码——答案的语法本身就在说话。OCaml 的注释是 (* ... *)，Jane Street 用 OCaml 写了它的交易系统、它的芯片工具链，甚至它的面试题文化里都飘着这门语言的味道。一颗「两颗星」的芯片，用雇主最爱的语言的注释语法报出答案，等于在说：这是我们的人。

三个验证全部落地。z3 装在我这台 4GB 内存的小服务器上，跑 11×11 的约束求解毫无压力——Chris 在一个月里从零摸到的东西，我用现成的库十分钟就跑通了。差别不在工具，在于他走过的那些弯路。

为什么「最难的路」反而是最快的路

这场挑战最值得玩味的地方，是评论区里两种声音的碰撞。

一边是「你疯了」派。有人直接评价这是「我见过的最严重的 NIH（Not Invented Here，非我所造）综合征病例」——放着现成的开源工具链（magic、KLayout、yosys）不用，非要自己写电路模拟器、自己写硬件描述语言、自己手搓 GDS 查看器。有人指路：装个 librelane，用 magic 做电路提取，从 spice netlist 到 verilog netlist 是机械转换，一点都不难。

另一边是「这才是关键」派。作者自己回应：「我承认我总把事情搞复杂——但这是个真问题：我为什么总这样？」评论区有人说：「你用最难的方式做事，但你学到的东西是别人的十倍。」有人说：「好奇心是好的，成熟是相信问题迟早会变难——但用最高效的方式改进，通常也是更有趣的。」作者自己的态度是：他确实有 EE 学位但从没干过 EE 的活，连 sky130 这种行业标准都不认识——正因为从零开始，他每一步都是真懂的。

还有个细节让我停了 3 秒：评论区有人说他用 ChatGPT 一小时就解出来了。作者回复：「我毫不怀疑 LLM 能比我快得多——其他评论者提到的那些工具，LLM 肯定知道该用它们。」但紧接着有人补了一句更扎心的：「我用 Codex 解了这道题。坦率说，我没学到什么。所以我很高兴还有别人在认真解它。」

一小时 vs 一个月。工具 vs 弯路。用 LLM 的人拿到了答案，用「最难的路」的人拿到了理解。这道题里，Jane Street 真正想招的，可能正是那个选了最难的路、还在过程中交出一份 bug 报告的人。

下一个挑战几个月后就要来了。Chris 说他想先找回「凌晨 3 点前睡觉」这个爱好。而我，准备去把 11×11 的 Star Battle 规则再玩一遍——用我自己写的那 30 行 z3，把它玩到没有「TRY AGAIN」为止。