Nineteen days from “what does reverse-engineering an ASIC even mean?” to a mask-level layout decompiled into gates, simulated, SAT-solved, and proved complete — and the discovery that the silicon is a puzzle validator with a Latin motto written on it in Morse code.
One binary file, no names, no netlist, no source.
Jane Street’s 2026 puzzle ships a single artefact: puzzle.gds, a GDSII stream —
the format a foundry receives. It is not source code and not a schematic. It is
photomask geometry: polygons on numbered layers, where layer 66 is polysilicon and
layer 68 is the first metal, plus thousands of placements of named library cells. Everything
above that level — module boundaries, signal names, the design’s intent — was compiled away.
The stated goal is to drive a success output high. The real goal, buried in the
README, is that “you’ll need to simulate it to get your final answer” — the chip emits
a string on O[7:0], and that string is the submission. success is a
checkpoint, not the finish.
A warmup/ directory carries the same design at every compilation stage — RTL,
netlist, placed netlist, GDS. That is the Rosetta Stone: any tool built to run the pipeline
backwards can be checked against ground truth before it is ever pointed at the real thing.
The blog permits AI for tooling and for the warm-up, and forbids feeding it the puzzle
files or having it write the submission. So the rule for the whole campaign was:
build instruments, never read the evidence. Every command that touched
puzzle.gds was run by hand; the answer arrived as tool output, not as
a model’s claim.
Eight working sessions. The first three build understanding, the next three build instruments, the last two use them.
Opening question — “does reverse-engineering mean recovering the original Verilog?” — is
answered no: the deliverable is behavioural equivalence, not textual recovery. Then
warmup/00_source.v line by line, followed by nine questions that go all the
way down: what is fanout, what is a net, what is a flip-flop, why does combinational
logic need a clock at all.
sky130_fd_sc_hd__dfrtp_2 naming scheme, and why 6 pins can carry 16 bits of state.A two-column annotated reference is published so question and answer sit side by side instead of scrolling apart. Then the RTL→GDS pipeline — Yosys, ABC, place-and-route, stream-out — and which stages are reversible. GDS is explained as “SVG, but the layers are physical materials”, which is where the analogy earns its keep: an SVG layer is cosmetic, a GDS layer is a fabrication step.
The layout viewer is opened, layer numbers (64/5, 66/20)
decoded, and its macro IDE turns out to have a genuine defect: the Run button stays
bound to the wrong file no matter what is selected. Two workarounds are tried before the
right move — abandon the GUI, run klayout -b -r script.py, then abandon that
too for the klayout PyPI module and a normal venv with a debugger.
KLayout’s LayoutToNetlist is pointed at the warm-up GDS: conducting layers
declared, via layers bridged, each standard cell recovered as a subcircuit with pin names
read from the text labels inside it. The output is compared to the reference netlist not
by name — the extracted names are meaningless — but by net signature: each net
reduced to the multiset of celltype.pin it touches.
Three modules in one day. A cell library carrying Boolean expression trees; a netlist parser that infers port directions from usage and exposes fan-in cones; a cycle-based simulator. Then the conceptual jump — a SAT solver has no notion of time, so time is turned into space. The circuit is copied once per cycle and frame k’s flop outputs are wired to frame k+1’s inputs, which turns a cyclic circuit into an acyclic formula. Explained with a visual artifact before any code was written.
The survey runs on puzzle.gds: 9,875 placements, 80 cell types, and two
names that belong to no library — INTERNAL_3 and INTERNAL_7.
Fifteen cell types have no definition. A review pass strips 80 lines of speculative
flags from the toolchain, with the standing instruction not to cut anything the puzzle
might need.
--check-lib refuses to proceed while any
placed cell type lacks a definition, because a wrong cell function corrupts every result silently.The hardest day. Hand-written cell definitions are thrown out and re-derived from the PDK’s own Liberty data. An undriven wire is chased for hours. Eight flip-flops turn out to be the wrong type to reset to zero. Escaped Verilog identifiers silently collapse all eight output bits into one port — twice, once in the reader and once in the writer. Then, with the blockers cleared: 122 frames, one unique input, fifteen bytes out.
(* TWO STARS *) — and, hidden on a layer below the
die outline, a strip of Morse code.Deadline day, spent on completeness rather than the answer. Jane Street’s own reference waveform is parsed and replayed through the extracted netlist. The set of messages the chip can emit is enumerated by SAT until UNSAT. The 121-bit input is recognised as an 11×11 grid, the region map is recovered behaviourally, and the puzzle is re-solved from scratch to confirm it. A forked-file sweep looks for further eggs and finds none.
Each stage discards something provably inert. The whole point is that every arrow is checkable.
I, enable high throughout, verdict at frame 122.
The success cone is 484 of 728 cells, and it sits entirely
inside the O[7:0] cone — nothing feeds the verdict without also feeding
the output. Thirteen flip-flops belong to the output generator alone, which is precisely the
region the puzzle README says can be ignored during reverse-engineering.
The reason to trust the answer is not that a solver returned SAT. It is that five independent methods were made to agree.
| Check | Method | Result |
|---|---|---|
| Extraction is faithful | Net-signature isomorphism against the warm-up’s reference netlist — name-independent | 230/230 cells 84/84 nets |
| Cell semantics are real | Library parsed from the PDK’s Liberty JSON, not hand-written; exhaustive 65,536-pair self-test reproduces the warm-up RTL exactly | 0 mismatches |
| The netlist matches the original chip | Jane Street’s own example_inputs.vcd replayed through the extracted netlist,
comparing O and success every cycle |
312/312 cycles |
| The solver and simulator agree | Every z3 model replayed through the independent Python simulator; disagreement aborts rather than reporting | PASS |
| The input is unique | Blocking-clause enumeration over generalised cubes, run to exhaustion | 1 solution UNSAT after |
| The length is minimal | 121 cycles UNSAT, 122 SAT — pinning the protocol at exactly 121 clocked bits plus a settle frame | 122 frames |
| Nothing else can be emitted | Message vectors blocked whole and re-solved until UNSAT, after first proving by SAT that no output is possible outside frames 122–136 | 5 messages 27 byte values |
| The recovered puzzle is the right one | Star Battle rebuilt from the extracted region map and solved from scratch in z3, independently of the netlist | 1 solution, identical |
Replaying the reference VCD initially showed 20 mismatches on O, zero on
success. That pattern — one signal wrong, the other right — is the signature
of a sampling offset rather than a logic error. Shifting the comparison by one cycle gave
0/312. The VCD logs O at the clock edge; the simulator returns the value computed
during the cycle. Same trajectory, different label.
121 = 11 × 11. The input was never a bit stream. It was a board.
Read the winning input row-major into an 11×11 grid and the structure is immediate: exactly two stars in every row, exactly two in every column, and no two stars touching — not even diagonally. The chip is a Star Battle validator, and the messages it emits are the rules of the game.
The architecture then explains itself. 121 squares but only 92 flip-flops means the grid cannot be stored; it must be scored incrementally as bits arrive:
| Count | Role | Evidence |
|---|---|---|
| 12 | Shift register — the adjacency window | Only stages q0, q9, q10, q11 tap out to logic: squares i−1, i−10, i−11, i−12. That is left, up-right, up, up-left — which is why it is 12 bits and not 11. |
| 22 | 11 column counters, 2 bits each | Saturating: 0, 1, 2, 3 — and a fourth star still reads 3. |
| 22 | 11 region counters, 2 bits each | Recovered by the single-star sweep; an exact-cover search found only two ways to tile 121 squares, the columns and these. |
| 8 | Position counter (4 row + 4 column) | Addresses the readout. |
| 8 | Output character generator | One private flop per output bit — the characters are computed, not stored in a ROM. |
| 4 | Readout position counter | 16 positions, matching the 15-byte burst. |
| 1 | Row counter | Clears at each row boundary — which is why it never showed up in end-of-run scans. |
| 3 | Total star count, done flag, output enable | — |
| 11 | Unidentified | Left unresolved at the deadline. |
Five, and SAT-proved to be all of them. The answer is also a joke in the house language: an OCaml comment whose delimiters contain exactly two asterisks — a comment that counts its own stars.
It was visible in the very first command run against the file, and walked past for two weeks.
The survey printed bbox (0,-52.72; 200,300). A standard-cell array starts at
y = 0 by construction — rows stack upward from the origin. Negative y means
something was deliberately placed outside the design. That 52.72 µm strip is the whole
find, and no rendering was needed to spot it.
What is down there: 36 marks on layer 200/0, in one row, in two widths. Quantised
against a 1.38 µm unit, the widths are {1, 3} and the gaps are {1, 3, 7} — with nothing left
over. That is the ITU Morse timing specification, not a coincidence.
PER ARENAM AD ASTRA
“Through the sand, to the stars.” — per aspera ad astra with aspera (hardships) swapped for arenam (sand). Silicon comes from sand.
Which makes (* TWO STARS *) literal as well as self-referential: the die’s motto is
about reaching the stars, and the payload it hands back is two of them. The strip sits
deliberately outside the official die outline — the prBoundary is
(0,0;200,300) and does not contain it. It is also absent from the supplied
layout.png render, so the only way to it was the file itself.
Kept because the interesting ones share a property: the regression suite stayed green through most of them. A test that passes on the warm-up says nothing about a construct the warm-up does not contain.
Cell library written from the naming scheme, not the datasheet.
Fifteen missing cell types were filled in by inferring functions from names like
o2bb2a.
A wrong Boolean function corrupts every simulation and every SAT result with
nothing to warn you. Fixed by discarding the hand-written library entirely and parsing 70
cells from the PDK’s Liberty JSON — including deriving reset/set polarity from the
ff() group, and raising rather than guessing on an active-high clear.
Every flip-flop pinned to 0 at reset. The design has 84
dfrtp, 4 dfstp and 4 dfxtp — a dfstp
leaves reset at 1, and a dfxtp has no async control at all.
Worse than a plain bug: the solver and the simulator shared the assumption, so
--verify would have agreed with itself while both were wrong. Initial state is
now derived per-cell from Liberty.
Bus indices eaten from escaped identifiers. The port regex stripped
[...] assuming a bus width, so \O[0] … \O[7] all
collapsed to one port named O.
Correct for input [7:0] data, wrong for an escaped identifier
where the brackets are the name. Present twice — once in the reader, and again in
the writer, which emitted the illegal output O[0]; so the fixed reader hit the
same bug on the next pass.
Hierarchy counted one level deep. The inventory walked only the top
cell, so the 21 INTERNAL_3 and 15 INTERNAL_7 containers hid their
contents.
The library gate could have passed while an undefined cell type sat inside a container. Found by the user asking whether those cells were in the output at all.
Shift-chain detection recognised only mux2 hold paths.
On the puzzle, 51 of 92 flip-flops build their hold path from ordinary gates —
nand2b, o21a, a21o.
The warm-up used mux2 exclusively, so this could never have
shown up there. The first fix then over-detected — a counter bit also reads its own
Q back — and needed a truth-table query to distinguish pass-through from
arithmetic. Only possible because the library carries real functions.
--verify drove rst_n randomly, re-asserting
reset on roughly half of all cycles.
The design barely left its reset state, so the equivalence check proved
almost nothing while reporting PASS. Related: a proposed --free-init mode was
outright unsound — it let the solver invent a starting state no reset can produce.
A missing pin connection silently skipped 8 of 63 cells.
Fault injection showed one deleted connection cascading through the design
with no diagnostic — and clean.py --verify comparing two identically-broken
simulations and printing PASS. A warning now fires inside step(), so every
caller inherits it.
“ALL GREEN” printed over three real failures. set -e does
not fire inside a pipeline.
Three regression steps had produced no output at all. Same session also broke
survey.py by re-opening a docstring in a replacement — caught only because a
syntax check ran.
“Fixed” a floating net that was never fixed. An undriven wire,
n1447, was chased across a whole session. Three other bugs were found
and fixed along the way, the count went from 15 problems to 1, and that got reported in a
way that read as resolution.
Called out directly — “Are you sure it’s all correct now?” — and retracted. It was then settled properly and empirically: 3,000 random cycles with the net forced to 0 and to 1 produce identical outputs, so it cannot affect anything. Its forward cone contains zero sequential cells.
A false negative that hid the one place it did matter. The check “is this net in any output’s cone?” compared a net name against a set of cell names — it could never match.
The net reaches O[1] and O[4]. That is exactly why a
fifth message came out two different ways in two runs. The enumeration now leaves the net
free per-frame and reports the indeterminacy rather than hiding it.
“J S C” — a company acronym read out of three grid regions.
One region is unmistakably a blocky S. The second was pattern-matched, the third forced — a shape with a full bottom bar and a stray square called a J — and then the reading order was chosen to produce the acronym. Fitting the data to the conclusion. Retracted under questioning: one letter spells nothing, and an S is the most likely shape to appear by chance.
Six identically-named scopes in the reference VCD, pushed four times.
Viewers merge same-named scopes, so the file renders exactly like the conventional form — there is no channel there to hide anything in. Settled by generating two rewritten VCDs and loading all three side by side. It was a generator quirk.
Hunting the “two stars” as drawn geometry.
A vertex histogram showed every shape on every layer was a 4-gon, killing star-shaped art. Metals and placement were rendered — power straps and functional clumps. All 893 text objects turned out to be standard-cell pin labels. The actual find needed none of it, only the bounding box.
KLayout’s macro IDE ran the wrong file, permanently.
Tree selection, saving, reopening, F5 — none of it moved the run binding. Never diagnosed. Escaped via a one-line loader stub, then abandoned for batch mode, then for the PyPI module. The right call, two workarounds late.
“Don’t give away any answers — I need to work it out myself.” ·
“Don’t perform any installations yourself.” ·
“Why not patch directly, why write a Py script to do this?” ·
“You can read the file, why are you doing these tricks?” ·
“Do you really need a new script instead of adding it to survey.py?” ·
“Why are you holding rst_n=1?”
The last one had no good answer — it was a convenience carried over from the warm-up and
never re-examined. Investigating it exposed the unsound --free-init mode.
Thirteen files, 4,033 lines of Python. Everything runs from the command line.
| Tool | Lines | Does |
|---|---|---|
| survey.py | 404 | Layer table, recursive cell inventory, per-cell geometry dump, library gate (--check-lib), inert-cell detection by height and power pins |
| extract.py | 206 | GDS → Verilog netlist via LayoutToNetlist, via flattening, filler stripping |
| celllib.py | 195 | Cell semantics parsed from the PDK’s Liberty JSON — no hand-written functions |
| crosscheck.py | 387 | Liberty function parser, shared with the cell library |
| netlist.py | 487 | Parser and graph: direction inference, driver/sink invariants, backward and forward cones |
| clean.py | 391 | Graph rewrites — directions, clock-tree collapse, structural net naming — with equivalence verification |
| sim.py | 627 | Cycle-based simulator: topological evaluation, per-cell reset semantics, register recovery, CSV output |
| solve.py | 558 | z3 bounded model checking: unrolling, cube generalisation, all-solutions enumeration, VCD emission |
| sim_special.py | 249 | Proves the output-message set complete by enumerating to UNSAT |
| vcd.py | 125 | VCD → CSV, for replaying the reference trace against the extraction |
| sweep.py | 158 | Batch stimulus runs with randomised tails |
| extract_cells.py | 167 | PDK cell data extraction |
| compare_netlists.py | 79 | Name-independent structural isomorphism check |
enable and rst_n high throughout,
success at frame 122:Eleven of 92 flip-flops were never assigned a role. The census covers the shift register, both counter banks, the position and readout counters, the character generator and the flags — the remainder was not chased before the deadline.
One net has no driver. Its geometry is two cell input pins joined by a single
top-level metal wire with vias only at the ends; no third cell’s geometry touches it, every
conducting layer in that region is registered, and nothing lies within 400 nm. It is either a
genuine floating net in the design or an extraction gap that could not be measured. Either way
it was proved inert for success, and its only reach — two bits of one non-winning
message — is reported as indeterminate rather than papered over.
Two of the three “letterform” regions were a false reading, withdrawn. Whether the remaining S is intentional is unknown and probably unknowable.
The final completeness query — the message alphabet with enable and
rst_n both left free, roughly 142,000 variables over 200 frames — was still running
when submissions closed. The held-enable version had already returned UNSAT.