← Back to home

Reverse-Engineering an ASIC

From a Binary GDS File to (* TWO STARS *)

A complete walkthrough of the Jane Street ASIC puzzle using KLayout, z3, and Icarus Verilog.

Introduction

Jane Street published an ASIC reverse-engineering puzzle (blog post).

Task: Figure out what input bit sequence on I makes the success output pin go high and find as many easter eggs as you can.

The Approach

Write in advance

Before I started the puzzle, I opened the puzzle.gds file with KLayout, which could render zoomed versions of each part in detail and check each layer separately. At this stage, I found that the standard cells used are from sky130_fd_sc_hd. I had seen this library in the test folder of the OpenRoad project (which contains a LEF file), so I directly used this library later in the analysis. I also viewed the simulation results in example_inputs.vcd using GTKWave, but I don’t think it really helps much… just for enjoying fancy waves.

I don’t know much about physical design from my background, but the warmup example gives hints. As a newbie, my direct solution is very intuitive: I would like to identify all the cells first, then find their connections, and from the technology library we could know each cell’s Boolean representation. At this stage, we should be able to write a netlist, which could be simulated, synthesized, etc.

Then we need to make sure every step mentioned above is “doable”.

The final strategy in the solution has four phases:

Phase 1: Extracting a netlist from the geometry

Strategy

Three operations reverse the place-and-route process:

1. Identify the metal stack — determine which GDS (layer, datatype) pairs correspond to li1, met1, …, met5, and which VIA cells connect adjacent layers.
2. Build connected components per layer — for each metal layer, flatten all polygons (top-level routing + every cell’s internal metal, transformed by its placement) and merge touching/overlapping ones via Region.merge(). Each resulting “blob” is one electrical net on that layer.
3. Label blobs with cell pins via point-in-polygon — for each placed cell’s each pin, transform the pin’s LEF rectangle into world coordinates and find which merged blob contains the pin’s center point (Polygon.inside(Point)).

Cross-layer connections are resolved by walking every VIA cell: each VIA’s bottom-layer metal shape and top-layer metal shape identify two blobs that are actually the same net. A union-find data structure merges these into final net IDs.

Visualizing the extraction step by step

The following figures (from the actual GDS geometry data in json format, rendered using matplotlib, data can be dumpped from KLayout directly, those fancy gifs are generated with the help of GLM 5.2) show what each operation sees. Throughout, the color scheme is:

At this zoom level, the design looks like a solid block, you can see overall structure (the power grid stripes, the main core area, the INTERNAL-cell row below) but cannot distinguish individual cells, pins, or wires. The next figures peel back layers to reveal how the routing is constructed.

met1 is the lowest real metal. It carries the power rails (the wide horizontal stripes at the top and bottom of each cell row) and the shortest routing connections. When we merge all touching met1 shapes, the power rails form one giant connected blob, which is why power-net matching must be excluded from signal extraction.

This is the scale at which the extraction algorithm operates. The LEF gives us the exact (x, y) position of each pin. After transforming by the cell’s placement, we search for the merged blob whose polygon contains that pin’s center — linking the pin to its electrical net.

Phase 2: Verifying the extracted netlist

Generating the cell library from Liberty

Now we have connected all standard cells and formed a netlist. To do the simulation, the last thing we need to do is to “mark” all standard cells with their function. This is where the technology library gets involved. Every cell has a clearly defined Boolean function; we just need to extract it.

gen_cell_lib.py reads the function: field from sky130hd_tt.lib for every cell used in the netlist and emits one Verilog assign per cell:

From

cell (sky130_fd_sc_hd__o22a_2) {
    function : "(A1&B1) | (A2&B1) | (A1&B2) | (A2&B2)";
}

to

module sky130_fd_sc_hd__o22a_2 (input A1, input A2, input B1, input B2, output X);
  assign X = (A1&B1) | (A2&B1) | (A1&B2) | (A2&B2);
endmodule

Building the replay testbench

vcd_to_tb.py parses example_inputs.vcd and emits a Verilog testbench that drives clk, rst_n, enable, I to match the VCD exactly, then samples O[7:0] and success at every timestamp and compares against the recorded values.

Result: bit-exact match

=== RESULT: 624/624 checks passed, 0 mismatches ===
*** ALL CHECKS PASSED ***

624 output samples across 3.1 µs of simulated time, all matching the reference VCD.

Output decodes as ASCII

The recorded O[7:0] values spell a message (consecutive duplicates collapsed):

\0 T R Y   A G A I N \0 T R Y   A G A I N \0

The wrong-input message is literally TRY AGAIN — confirming the extracted netlist is functionally identical to the original design.

Phase 3: Solving for the winning input

Why brute force fails

The design has 92 flip-flops (2⁹² states). Random sampling of 5,000 patterns × 150 cycles produced zero successes. The winning state requires a specific ~120-bit serial input.

Bounded model checking with z3

solve.py unrolls the netlist for 150 cycles as a satisfiability problem:

1. Create one z3.Bool per net per cycle (739 × 151 ≈ 112k variables, where 739 is the number of wires).
2. Constrain every combinational cell output to its Liberty function at each cycle (including conb_1 constants: HI = 1, LO = 0).
3. Constrain every DFF transition: Q[t+1] = D[t] when rst_n = 1, else reset value.
4. Fix rst_n = 0 for cycles 0–2, rst_n = 1 from cycle 3, enable = 1 from cycle 4.
5. Leave I[t] as free variables (the search target).
6. Assert success = 1 at some cycle in [5, 150].

z3 returns sat in 7 seconds.

Result

The 122-bit winning input (cycles 4–125):

000000010101000010000000000001010101000000000000101000000100000100000010000010100001000000010000001000001001000101000000000

Verified in iverilog: success goes high at cycle 126, and the output changes from TRY AGAIN to:

(* TWO STARS *)

Easter eggs

Four hidden output messages

The output generator produces different messages depending on the input:

Cosmic progression: empty sky → big bang → try again → two stars.

(* ... *) is OCaml/SML block-comment syntax, Jane Street’s house language.

Morse code in cell geometry

36 empty placeholder cells (INTERNAL_3, INTERNAL_7) below the main core at y = -53 µm encode a Morse code message. The cell widths and gap sizes follow the standard 1:3:7 International Morse Code timing ratio:

Decoded:

.--.  .  .-.   .-  .-.  .  -.  .-  --   .-  -..   .-  ...  -  .-.  .-
 P    E   R     A   R    E   N   A   M     A   D      A   S   T   R   A

(* TWO STARS *)