How not to solve Jane Street's ASIC puzzle. Kinda.

Act I: “wait, they left the hierarchy in” (18:27 – 18:55)

PROMPT 1 (the brief)

18:27: Cloned the repo. Checked what was installed.

18:31: Started the SKY130 PDK download in the background (volare).

18:32: Wrote gds_inspect.py: open the GDS, dump top cell / layers / hierarchy / labels as JSON.

The first real finding, about four minutes in. The GDS still contains named standard cells — sky130_fd_sc_hd__nand2_2, dfrtp_2, clkbuf_16 — with their pin labels (A, B, Y, D, Q, CLK, RESET_B) intact inside them. Only the internal net names were stripped. And the external ports survive as text on the metal layers: clk, rst_n, A, B, en, S.

The cell histogram read straight out of the GDS matched 01_netlist.v instance for instance. That decided the whole approach: this is not a geometry problem, it’s a connectivity problem.

PROMPT 2: “USE UV FFS”

(I had started building a venv with python3 -m venv. Fair.)

18:34: extract.py — KLayout LayoutToNetlist, SKY130 layer definitions, MOSFET extraction from diff/poly/nwell geometry.

18:40: Extraction working: 1412 MOSFETs, 547 nodes, 55 ms. Per-cell device counts match the SkyWater library netlists exactly for all 18 cell types.

18:42: Supply rails identified structurally — the node carrying the most PMOS source/drains is the positive rail: 610 terminals vs 16 for the next candidate. It turned out to be the one labelled VPWR.

I read the official sky130.lvs deck to learn how they model the substrate (an empty layer tied to a global net). That’s the only code I read that someone else wrote for this problem, and it’s PDK material.

Act II: the simulator does not work, three times (18:42 – 18:53)

First run of the switch-level simulator: 486 of 547 nodes unknown. Nothing worked at all.

Two of the three bugs were cheap. Conservative X propagation meant an asynchronous reset could never clear a power-on unknown, because a transistor with an unknown gate injected “unknown” rather than “this value, maybe” — fixed with three-valued reachability. Simultaneous updates, evaluating a whole wavefront against frozen values and committing together, made every cross-coupled latch oscillate forever with both halves flipping on every step — fixed by committing each component immediately.

The third one is the good one. The flip-flops didn’t work, and I couldn’t see why in a 1412-transistor netlist. So I wrote a tool to carve a single cell instance out into a standalone circuit (cell_ir.py) and ran one dfrtp_2 on its own. It captured a 1 correctly and a 0 as unknown. That asymmetry was the clue.

The cause: while a clock edge ripples through a cell’s internal inverters, the forward path briefly fights the keeper it is meant to override — and the keeper is deliberately the weaker device, 0.42 µm against 0.64 µm. Calling every contention “unknown” makes the latch store the unknown and never recover. Resolving by lowest-resistance path, using the widths from the extraction, fixes it.

This is the moment the project became about physics rather than connectivity. You cannot simulate these cells without transistor sizes.

Act III: proving it’s right, then the humbling (18:53 – 19:16)

18:53: Icarus Verilog testbench against 00_source.v as the oracle.

18:54: 15 000 random sequences across 3 seeds, ~490k cycles: zero divergences.

19:00: Coverage crate: four definitions, AFL-style bitmap, plus a calibration pass that auto-suppresses the clock tree (nodes that change on ≥98% of samples) without anyone naming it.

19:05: Custom fuzzer. Finds S in 878 executions. RTL confirms the same cycle.

19:07: First benchmark. Random search found it in 170 executions. Coverage-guided needed 878.

The obvious experiment — 32-cycle sequences — says coverage guidance is worse than useless. I nearly wrote that down as the result.

The fix was to ask how hard rather than whether: sweep the sequence-length cap. At 32 cycles the design has so many chances to stumble into a satisfying state that blind search wins. Squeeze it to 8 and every cycle has to be right:

One configuration, read as the verdict. First time in the project a check I trusted gave a confident wrong answer.

Act IV: making it fast, which mattered more than being clever (19:10 – 19:56)

The speed came from automatic cell characterisation: simulate each library cell on its own, at transistor level, over every reachable configuration of its own nodes and every combination of its inputs, and out comes a transition table. A flip-flop and a NAND go through the same loop; the flip-flop just has more states. The resulting model runs at 1.75M cycles/s — ~30× the transistor model, and faster than Icarus running the original Verilog. For contrast, ngspice on the same extracted netlist manages 3.6 cycles/s: it agrees with everything else, but the 8-cycle benchmark point would have taken it 126 days.

Act V: the challenge, and an hour of nothing (19:49 – 20:49)

Extraction generalises with no changes: 9875 placements, 1618 standard cells, 0.6 s. Characterisation: 64 cell types, 2 s.

The strongest single validation in the project: both models reproduce every one of the 5616 output bits recorded in the puzzle’s own example_inputs.vcd. A model built only from geometry and a layer table, reproducing the reference waveform of a design nobody has explained.

Then a 16-configuration fuzzing campaign: 17.9 million executions, 699 million simulated cycles, one hour, nothing.

Notable from the failure: state-hash coverage fills 100% of a 65536-entry bitmap at every sequence length, with corpora up to 18 500 entries. On a 707-cell design almost every execution reaches a state never seen before, so everything looks novel — which is the same as nothing looking novel.

Act VI: babush’s questions, and four measured negatives (20:00 – 21:10)

PROMPT 3 — “are you running the fuzzer right now / how do I run it / what does ‘on the real challenge’ mean”

PROMPT 4 — “are we piping the register states into cmp-log style feedback”

That one reframed the problem. The cone analysis derives, mechanically, that the warm-up’s target is decided by 16 register bits with exactly 15 of 65536 assignments satisfying it — no one typed the word “comparator”. On the challenge, sampling the same predicate:

of 20000 samples: 7457 already assert, 10104 are one flip away, 2439 further

37% of arbitrary register states already satisfy success. The challenge is not hard because its condition is narrow, but because the design never visits those states. That is a reachability problem, and it is the sentence the rest of the project turns on.

PROMPT 5 — “Are you using libafl or a custom fuzzer”

PROMPT 6 — “how do I run the libafl one myself on the actual challenge”

Both, and the LibAFL build paid for itself twice without ever winning a benchmark: my loop being slower than it exposed a bug of mine (28k → 94k executions/s once fixed), and prompt 6 exposed another — my LibAFL build was skipping the calibration pass, so it had been watching the clock tree while my loop wasn’t, making the comparison unfair in my own favour. The rest of the stretch is four refinements I built, measured, and left switched off:

Input-to-state took four iterations, each fixing a real flaw, and the verdict never changed. Also: a five-seed check said it was a 3× win; twenty seeds said noise. Second time in the project a check I trusted gave a confident wrong answer.

Act VII: the pivot (21:10 – 21:40)

PROMPT 7 — “Takeaway?”

PROMPT 8 — “I need some actionable takeaway c***” ← load-bearing

I’d been writing reflective summaries. This one made me produce a list of things to do, and the first item was: stop fuzzing, export to a model checker. Which I should have concluded myself an hour earlier, the moment the 37% number landed.

PROMPT 9 — “ok”

21:23: SMT export built. Every piece already existed: characterisation says which cells are pure logic (→ Boolean functions read off their own truth tables) and which remember (→ state bits, next value obtained by driving the cell through a clock edge). The clock isn’t modelled — one transition is one cycle — so the clock tree is identified and dropped. Challenge becomes 92 state bits, 598 combinational cells per cycle.

21:23: Warm-up: solver recovers the known trigger in 13 ms, and the trace replays through the simulator.

21:29: Challenge: unsat through 96, sat at 128.

Then the check that mattered. Pinning the export’s inputs to random sequences and comparing all nine outputs against the simulator passed — because this design’s outputs sit at zero for hundreds of cycles, so the check was two models agreeing that nothing happens.

Replaying the puzzle’s own VCD through both caught it instantly: 28 disagreements, first at cycle 122, which is the first cycle the outputs do anything. The bug: a cycle has two settled states — registers sample the logic settled against the old state, outputs are read from the logic settled against the new one. I’d collapsed them into one, shifting every output by a cycle.

A validation that cannot fail is not a validation. Third time in the project a check I trusted gave a confident wrong answer.

21:40: Corrected: unsat ≤96, sat at 128, success at cycle 127. Replays on both models under every power-up convention.

21:45: Asked four times at different depths: four different traces, four different assertion cycles, same output byte — 0x28. I reported that as the answer.

Act VIII: “have you tried running it for longer” (21:45 – 22:00)

PROMPT 10 — “Dude. Have you tried like, running it for longer after success.” ← load-bearing, and the one that actually solved it

0x28 is '('. My first solve unrolled 128 cycles and asserted at 127, so there was exactly one cycle left to observe. The design emits the answer over the following fifteen:

(* TWO STARS *)

OCaml comment syntax, which for Jane Street is a signature rather than a coincidence.

And then one more bug, which only this could have found. At first only the SMT export could read the message — both simulators reported the bus as unknown through the whole window, which is exactly why I’d dismissed those cycles as noise.

21:50: Built replay --find-x-origin: find the first cell that emits an unknown although every one of its inputs is definite. It named one cell: dfstp_2, the async-set flop, one falling clock edge after capturing a value.

21:52: Carved that cell out standalone — the same tool from Act II, three hours later — and reproduced it in eight cycles.

21:55: Cause: charge sharing decided by majority instead of capacitance. A flip-flop’s storage node is large (it drives an inverter); the internal nodes of a transistor stack are tiny. A falling edge briefly ties them together, the model calls it a conflict, the flop stores the unknown, and being a latch it never recovers. Weighting by gate area — from the same extraction as everything else — fixes it.

21:58: Both simulators now read (* TWO STARS *) directly. No solver needed.

That bug survived 15 000 differential sequences against the warm-up RTL (which has no set-flops) and the challenge’s own waveform (which never drives one into that state). Validation only covers the operating modes your stimulus visits. Fourth time in the project a check I trusted gave a confident wrong answer.