silicon · reverse engineering

A Star Battle, etched in silicon

2026-09-05~16 min

Jane Street's 2026 puzzle provides puzzle.gds. GDSII is the file format normally used to send a physical chip layout to fabrication; it stores shapes on named process layers rather than source code. The task is to recover the circuit and find a serial input that raises success. This post describes the extraction, analysis, and verification procedure. The recovered circuit checks an 11×11 Star Battle board.

Method

I treated the layout as the output of a compilation pipeline and reversed one stage at a time. Each stage produced a simpler representation and had a separate check: 

mask polygons
    -> standard-cell footprints       geometry XOR, rotations, mirrors
    -> pins and connected nets        metal/via connectivity extraction
    -> structural Verilog             728 functional instances
    -> registers and datapaths        graph passes to a fixed point
    -> transition system              yosys -> AIG
    -> accepted serial input          ABC bounded model checking
    -> puzzle rules and regions       simulation + GF(2) support probing

The warm-up in the challenge repository includes source Verilog, a synthesized netlist, DEF, and GDS for a known circuit. DEF describes placed cells and routed nets before they are converted into final mask geometry. I used these files to test cell matching and net extraction against known results: the extracted model recovered all 230 placed instances and all 84 signal-net partitions. The challenge says that the puzzle uses a very similar flow, so I still checked each assumption against the puzzle layout and traces.

The analysis scripts and selected intermediate artifacts are in the companion repository.

Identify the standard cells

The layout contains fixed-height rows of standard cells. A standard cell is a reusable physical implementation of a small function such as a NAND gate or flip-flop; synthesis tools place copies of them side by side. The following row contains a NAND, a compound AND-OR, an XOR, and a well-tap cell. The colors show poly, diffusion, local interconnect, and metal layers.

nand2_2a22o_2xor2_2tapvpwrvgnd_1
one standard-cell row from puzzle.gds · poly (red), diffusion (green), licon/li1/met1 stacked · dashed = cell outlines

The GDS retains its cell hierarchy, so KLayout can group the polygons for each placed instance. I did not use the cell names for identification. For each definition, I merged the device layers, translated them to a common origin, and compared them with cells from sky130, an open 130 nm process design kit and standard-cell library. The comparison uses the geometric XOR area: any area present in only one of the two layouts remains in the result. I tested four rotations and their mirrored forms because placement rows can be flipped. An XOR area of zero is an exact geometric match.

sky130 xor2, as drawn and mirrored · the matcher tries all 8 orientations and takes the zero-XOR fit

This pass identified 69 specific standard-cell definitions, including drive-strength variants, with no ambiguous matches. Collapsing those variants left 67 base families: 60 combinational, three sequential, and four physical or tie-cell families. I then discarded the hierarchy and repeated the identification from geometry alone. The metal-1 rails gave 102 placement rows, and the 460 nm placement grid gave candidate cell boundaries. An exact-match tiler recovered all 722 placed logic cells.

Recover the cell functions and nets

A cell footprint identifies a library cell but does not by itself describe its behavior. For the first functional model, I read each matched cell's Boolean output function from its Liberty file. Liberty is a standard text format that records a cell's pins, logic functions, and timing data. I used z3 to compare those expressions with common operators. If the two expressions cannot differ, the solver returns unsat and proves the equivalence. 

xor2    X = (A&!B) | (!A&B)     ==  A xor B          proven (unsat)
xnor2   Y = (!A&!B) | (A&B)     ==  not (A xor B)    proven
nand2   Y = (!A) | (!B)          ==  not (A and B)    proven
nor2    Y = (!A&!B)             ==  not (A or B)     proven
a21o    X = (A1&A2) | (B1)       ==  (A1 and A2) or B1  proven
mux2    X = (A0&!S) | (A1&S)    ==  S ? A1 : A0       proven

To check the result independently, I recovered the functions a second way, without Liberty. A transistor channel is poly ∩ diffusion; diffusion minus poly gives source and drain; n-well separates PMOS from NMOS; contacts and local interconnect connect the terminals. For each small cell, I enumerated every input pattern and evaluated the conducting switch network. This produced complete truth tables for all 60 combinational cell families, and all 60 matched Liberty. The same pass found three sequential storage-loop families and separated four physical or tie-cell families. This transistor-level method still needs a technology layer map, but it does not need the standard-cell function library.

KLayout's LayoutToNetlist then traced metal and vias to determine which pins share a net. A netlist is simply a list of component instances and the wires connecting their pins. The emitted gate-level model contains 722 logic instances: 630 combinational gates and 92 flip-flops. Six constant cells bring the functional-instance count to 728. Its ports are clk, rst_n, enable, serial input I, O[7:0], and success. Taps, decaps, and diodes were left out because they do not affect the digital model.

A connectivity audit found one undriven net. KLayout had represented a physical pin as a labeled floating terminal and a separate unlabeled terminal touching the driven conductor. I added a general repair rule: if one instance has an unlabeled terminal on a driven net and a labeled input on an undriven net, merge the terminals and discard the floating one. All later analysis used the repaired model.

The repository includes a VCD, a timestamped trace of digital signal values, with sample inputs and recorded outputs. Replaying those inputs through the extracted netlist reproduced all 22 output checks. On an invalid input, the output spells TRY AGAIN one byte at a time. This replay was the end-to-end check for extraction.

Recover the state-machine structure

The extracted Verilog is a flat collection of library instances connected by numbered nets. The following lines are from that model, including the flip-flop that drives success: 

module puzzle (clk, rst_n, enable, I, O, success);
  input clk; input rst_n; input enable; input I;
  output [7:0] O; output success;
  sky130_fd_sc_hd__and2  i0  ( .A(n35),  .B(n6),   .X(n1)  );
  sky130_fd_sc_hd__o21a  i1  ( .A1(n10), .A2(n1),  .B1(n4), .X(n44) );
  sky130_fd_sc_hd__inv   i3  ( .A(n2),   .Y(n87) );
  sky130_fd_sc_hd__dfxtp i7  ( .CLK(n710), .D(n764), .Q(n274) );
  sky130_fd_sc_hd__dfstp i10 ( .CLK(n568), .D(n614), .Q(n604), .SET_B(rst_n) );
  ...
  sky130_fd_sc_hd__dfrtp i137 ( .CLK(n710), .D(n804),
                                 .Q(success), .RESET_B(rst_n) );

Each flip-flop stores one state bit between clock edges. Names such as register, counter, and comparator are absent from the flat file, so I recovered larger structures from the connectivity graph before using a solver. The graph contains 92 flip-flops and 630 combinational gates.

recover.py runs local passes over the netlist graph and iterates them to a fixed point, which took eight rounds. A pass records a candidate grouping and its supporting edges; it does not rewrite the graph. The passes were:

The resulting summary was: 

=== concept recovery: 92 flops, 152 candidate concepts ===

control classes (reset / clock partition):
   84 flops   reset=0     -> zero-init state
    4 flops   reset=none  -> free-running counter
    4 flops   reset=1     -> seed / one-init register

autonomous registers:
   width 4    self-clocking counter, gated by i203

input-mixing registers:
   width 85   coupled block; 58 bits directly sample serial I

operand buses (word-level reductions):
   56 state bits -> D[i137]           (the win comparator)
   16 state bits -> each O[7] ... O[0] (16-entry byte ROM)

This gives a working model of the machine. An 85-flop coupled block receives I while enable is active. A four-bit autonomous register acts as an address counter. The next-state cone of the success flip-flop depends on 56 other state bits. Each output bit depends on 16 state bits; taken together, the outputs implement a 16-entry byte ROM.

These structural groups give names to the state used in the next step. The 92 flip-flop outputs form the current state; their D-pin logic defines the next state; and the serial input supplies one new value at each clock edge. With those pieces identified, the circuit can be written as a transition system and queried over a bounded sequence of clock steps.

Build and query the transition system

The extracted Verilog says which cells are connected, but Yosys also needs a behavioral definition for each sky130 cell. I generated small Verilog models from the Liberty functions. These are two of the definitions used for the formal model: 

module sky130_fd_sc_hd__and2 (A, B, X);
  input A, B; output X;
  assign X = A & B;
endmodule

module sky130_fd_sc_hd__dfrtp (CLK, D, RESET_B, Q);
  input CLK, D, RESET_B; output reg Q;
  initial Q = 1'b0;
  always @(posedge CLK or negedge RESET_B)
    if (!RESET_B) Q <= 1'b0; else Q <= D;
endmodule

Linking these definitions with the extracted instances turns the flat netlist into an executable sequential circuit. Let S_t be the 92 flip-flop outputs immediately after clock step t, and let I_t be the serial input at that step. The combinational gates feeding every D pin define the next-state function T. The success port is the Q output of one flip-flop, so the output function G selects that bit from the current state: 

S_0       = initial post-reset state
S_(t + 1) = T(S_t, I_t)
success_t = G(S_t)

This pair of functions and an initial state are the transition system. It discards physical details such as cell placement and wire shape, while keeping everything that can affect the state on the next clock edge.

I first wrote this relation explicitly with z3. The following is the central loop from the actual model. Each dexpr[f] is the Boolean expression found by walking backward from flip-flop f's D pin until reaching current-state bits or I: 

S = m.init_state()
Ibits = [z3.Bool(f"I_{t}") for t in range(N)]

for t in range(N):
    nxt = {f: z3.Bool(f"S{t+1}_{f}") for f in m.flops}
    sub = [(m.qv[f], S[f]) for f in m.flops]
    sub += [(m.iv, Ibits[t])]
    for f in m.flops:
        s.add(nxt[f] == z3.substitute(m.dexpr[f], *sub))
    S = nxt

This code shows the unrolling directly, but the general SMT model became slow as the bound increased. For the main search I used Yosys and ABC. The supplied VCD establishes the input protocol: reset the circuit, then load one serial bit on each of 121 enabled clock cycles. The formal wrapper models the interval after reset, holds enable high, leaves the serial bit unconstrained, and exposes success as the property output: 

module top (input clk, input i, output success);
  wire [7:0] O;
  puzzle dut (
    .clk(clk), .rst_n(1'b1), .enable(1'b1), .I(i),
    .O(O), .success(success)
  );
endmodule

The clk port is present because the Verilog cell models are edge-triggered. After sequential lowering, one AIG frame represents one register update; the counterexample data of interest is i. The cell models contain the initial values used after reset. Yosys then flattened the wrapper and the 728-cell design, normalized the flip-flops, and converted the combinational part to an AIG, an AND/inverter graph: 

read_verilog -sv build/cells_yosys.v
read_verilog -sv build/puzzle_fixed.v
read_verilog -sv build/formal_aig.v
hierarchy -top top
prep -top top -flatten
async2sync
dffunmap
simplemap
aigmap
write_aiger -map build/puzzle.aim build/puzzle.aig

An AIG still contains state elements, but every combinational expression between them is represented using only AND nodes and inverted edges. ABC can therefore ask, for each bound k, whether there are input bits satisfying the following formula: 

Init(S_0)
and T(S_0, I_0, S_1)
and T(S_1, I_1, S_2)
...
and T(S_(k-1), I_(k-1), S_k)
and success(S_k)

I ran that query with the following command. write_cex writes the counterexample trace, which in this case is the input sequence we want: 

yosys-abc -c "read build/puzzle.aig; print_stats; \
  bmc3 -F 400 -T 150; write_cex -a build/win2.cex"

Yosys reduced the property cone to 79 state elements and 806 AND nodes; state and output logic unrelated to success was removed. ABC proved that bounds 0 through 121 cannot reach the output and found success=1 at frame 122. At that frame the SAT instance had 3,145 variables and 12,723 clauses.

I replayed the witness through the original sky130 simulation models and observed the same success edge. This checks the result against the library cell models, independently of the simplified AIG used for the search.

I then used z3 to block that witness and search for alternatives in the bounded model. The variables for all 121 load cycles were fixed. Two later input samples occur after the success state has been evaluated, so they do not affect the board and remained unconstrained. The 121-bit payload is therefore unique.

Identify the checked rules

The output messages explain what the 121 input bits represent. An all-zero input produces EMPTY SKY, an all-one input produces BIG BANG, and an input with adjacent selected cells produces TWO NOT TOUCH. The successful input raises success and produces:

(* TWO STARS *)

These diagnostics identify a two-star Star Battle: an 11×11 grid with two stars in every row, column, and irregular region, and no two stars touching horizontally, vertically, or diagonally. Serial input order maps directly to the grid, one row after another. The successful payload contains 22 stars.

Recover the regions

The row, column, and non-adjacency rules are now known, but the 11 irregular regions are still missing. They are not exposed as simple groups of comparator inputs: the serial input is mixed into a coupled state register before it reaches the success logic.

The useful signal came from the internal state instead. I simulated 121 inputs containing a single star, one at each board position, and recorded which state bits in the success cone changed. Several bits act as GF(2) parity accumulators. GF(2) is single-bit arithmetic in which addition is XOR, so such a bit flips once for every selected cell in its support. Eleven of the measured supports were disjoint and together covered the board: 

region parity supports (cells):  4  5  6  7  8  8  9  11  14  21  28
                                 ---------------------------------------
                                 sum = 121  ->  a clean partition of the grid

The supports partition all 121 positions, and the successful payload has two stars in each support. An independent Star Battle solver, given only these regions, returns the same grid and proves it unique. As a separate check, I generated boards with the row and column counts held at two. For each board, I compared the recovered region counts with the chip's diagnostic output: a TWO ... message means that the count checks passed, while a different message identifies a count failure. The two classifications agreed.

The serial order and recovered supports give the following puzzle map:

the recovered 11-region puzzle map · serial input order runs row by row

Solving that recovered instance independently produces the same board as the formal witness:

the unique solution · verified on the sky130 models: success high, output (* TWO STARS *)

Additional data in the files

The following details are not needed for the solve, but they appear to be intentional parts of the challenge.

A decorative GDS layer contains 36 rectangles in two widths with a 1:3 ratio. Interpreting the widths as Morse code gives:

PER ARENAM AD ASTRA

This changes per aspera ad astra, “through hardships to the stars,” to “through sand to the stars.” The VCD version string is “Leave no stone unturned.”

Reading each sample-input row as a 7-bit character gives “The night sky awaits.” The warm-up circuit checks A + B == 496; 496 is a perfect number. The VCD timestamp is Dec 31 23:59:60 2016, the leap second added at the end of that year.

Technology used

The main verification points were 230/230 warm-up instances, 84/84 warm-up signal-net partitions, 69/69 cell definitions, 722/722 flattened logic instances, 60/60 geometry-derived truth tables, and 22/22 VCD output checks. The final input was re-simulated on the extracted sky130 model, and the recovered Star Battle instance was solved independently to confirm that it has one solution.

Thank you to Jane Street for publishing an interesting challenge and for including enough intermediate material in the warm-up to make the reverse-engineering process testable.