Jane Street逆向工程挑战：我的硬核解题路
Solving the Jane Street Reverse Engineering Challenge
Jane Street推出的逆向工程挑战彻底把我拖进了一个月的兔子洞。面对一个ASIC芯片的GDS文件，我试图从零开始理解其功能。起初，我固执地选择最艰难的路径：用Python和sqlite3手写电路模拟器，甚至自创硬件描述语言，结果在无数旁支末节中浪费了数周时间。最终，我放弃自研工具，转而利用gdstk库和sky130标准文档，通过几何重叠分析成功提取电路逻辑。从识别移位寄存器、加法器到比较器，我手动绘制连接图并用Verilog验证，终于解开了谜题。这是一次关于坚持、试错与最终回归常识的硬核工程之旅。
我总是选择最艰难的路来做事。
HN 评论区
74- mdritch
我超爱 z3。去年 Jane Street 的那个谜题我就第一次用了它，那题是个伪装成神经网络的哈希算法。我在工作中大量使用 MCMC，也做过一些关于用 z3 进行 MCMC 模型形式化验证的小规模探索，但还没什么实质成果。这次经历激励我重拾这个方向。
- ctippett
> 我最后用了一个叫 'z3' 的工具。它简直像魔法？每次它找到解，我都兴奋不已。
太有共鸣了。我上第一堂运筹学课时也有同样的感觉。把看似复杂到无法理解的问题框定为一堆简单的约束条件，然后得到解，这简直就像魔法一样。
- anonymousDan
挺有意思的是，他们居然有一套自研的开源 OCaml 工具链用于芯片设计。我原本以为业界共识是大家都还被那些糟糕透顶的厂商工具链绑死。这对生产级的芯片设计来说，是个现实的替代方案吗？
- piker
> 嗯，我其实不知道接下来该做什么
让我帮你：好好琢磨一下怎么花掉 Jane Street 每年付给你让你打卡上班的几百万美元吧。听说私人飞机挺贵的，比如。:)
- xvilka
为了真正帮助处理这类任务（鉴于图片质量不错），有一个开源软件叫 Degate[1][2]。