Reverse-Engineering an ASIC From Its Layout
Overview
Jane Street's 2026 puzzle handed out the physical layout (a GDS file) of a real,
fabricated chip built on SkyWater's open sky130 process — no schematic, no netlist,
just polygons. The chip takes a 121-bit serial input, and on the correct input it
raises a success flag and prints a secret message; on any other input
it prints "TRY AGAIN". The task was to recover what the chip actually does purely
from its layout, and then work out the one input that makes it succeed.
Design
The first step was turning geometry into a netlist. The layout was hierarchical — named standard-cell instances from the sky130_fd_sc_hd library, with only the net names stripped out. Pin labels on their own layer had survived at exact coordinates, so I built a KLayout-based extractor that flood-fills the metal and via layers into electrical nets, then reads off every pin's identity from its preserved label. That produced a structural Verilog netlist — 713 gates, 92 flip-flops — which I validated by replaying Jane Street's own example waveform through it and matching their "TRY AGAIN" output bit-for-bit before trusting anything downstream.
With a real netlist in hand, the next question was what actually drives
success. Tracing backward from its flip-flop led to a 56-bit equality
comparator — meaning some transformed version of the input had to match a hidden
constant. Critically, the chip has nowhere near 121 flip-flops of storage for a
121-bit input, so it isn't just shifting bits into a register and comparing; a shared
datapath transforms each bit as it arrives, cycle by cycle. That ruled out reading
the answer off directly and made this a real search problem: I extracted exact truth
tables for every gate type, unrolled the entire checker across its 121-cycle input
schedule, and handed the resulting circuit to the Z3 SAT solver. It found the
satisfying input in about 3.4 seconds, and a second solve with a blocking clause
confirmed the answer is unique. Feeding that input to the real gate-level simulation
confirmed it end to end: success latches high and the chip streams out
(* TWO STARS *) — OCaml comment syntax, a nice touch from the puzzle's authors.
Challenges & What I'd Do Differently
The part that could quietly sink the whole approach was trusting the extracted netlist without proof, so I leaned hard on validating at every stage — the extractor against a warmup puzzle with a known-good netlist first, then the full extraction against the provided example waveform, before ever writing a line of solver code. That discipline paid off directly: a subtle netlist bug would have produced a confidently wrong answer with no warning.
Once the SAT solve worked, I spent some extra time (purely out of curiosity) trying other ways the answer could have been found. Treating the transform as a linear system over GF(2) seemed promising given how XOR-heavy the datapath looked, but a direct superposition test proved it's genuinely nonlinear. A binary decision diagram hit real exponential blow-up before finishing. A Gröbner-basis approach couldn't complete even a small slice of the problem in reasonable time. Most interesting was implementing PODEM, the classic ATPG line-justification algorithm: my first version reported the goal unsatisfiable after suspiciously few backtracks, which turned out to be a genuine bug — it was justifying two logically irrelevant "don't care" inputs on a gate before the one input that actually mattered, so it committed nearly the entire 121-bit input to values that didn't matter and then failed for a reason that wasn't real. Fixing the ordering (justify whatever's actually required before anything left free, the standard PODEM "unique sensitization" idea) got rid of that false negative — but it then thrashed for real, repeatedly re-deriving the same sub-goal through the chip's reconvergent fanout with no memory of having failed there before. SAT's Boolean-satisfiability search with unit propagation and clause learning is exactly built to avoid that kind of repeated work, which is a large part of why it finished in seconds where the more "manual" approaches didn't. If I did this again, I'd reach for SAT immediately rather than treating it as one option among several — but I don't regret the detour; it's the clearest demonstration I've seen of why these older exact methods still lose to a modern SAT solver on real, structured hardware.
Results
Solved: the unique 121-bit input, verified in a real gate-level simulation of the
extracted netlist, makes the chip raise success and print
(* TWO STARS *). Submitted before Jane Street's September 4, 2026
deadline; this write-up went up once submissions closed.