ASIC Reverse-Engineering Puzzle 2026

• This repository contains my solution at solving ASIC Reverse-Engineering Puzzle 2026 hosted by Jane Street.
• I decided to call my submission "GDS-to-RTL", contrary to "RTL-to-GDS" :)
• The "ASIC Reverse-engineering" involves recovering a circuit from a layout file, working out what the circuit perorms, and then solving it.
• Check out ReGDS: A Reverse Engineering Framework from GDSII to Gate-level Netlist, and ASIC Reverse Engineering

---

Contents

Start here.

The pipeline, in the order it ran.

Extras and reference.

---

1. Timeline

---

2. What the puzzle turned out to be

• An "11x11 Star Battle (Two Not Touch) Validator". (pass in a solved puzzle and it tells you if it is right)
• Two stars per row, per column and per region, no two touching.
• Exactly one grid works.
• Drive in a solved 11x11 Two Not Touch Puzzle grid serially and the chip prints:

(* TWO STARS *)

• It was found that to drive "success" flag high, the following input sequence was needed :

  0000000101010000100000000000010101010000000000001010000001000001000000100000101000010000000100000010000010010001010000000

Note

• Star Battle is also referred to as Two Not Touch
• One can read about how the puzzle works here

Want to try the puzzle?

• Play here, read here
• Check out this sample interactive Two Not Touch Puzzle

Deliverables

• Below table lists all final deliverable files / outputs for the Puzzle :

---

3. What I did, in three lines

• Extracted a netlist from the raw geometry present in the puzzle GDS file.
• Proved the extractor pipeline exact against the warm-up's golden files, then validated it against the real chip's recorded outputs.
• Recovered the register structure, read the design's hidden data out of the silicon by probing it 121 times, solved the resulting puzzle two independent ways, and proved a behavioural model cycle-equivalent to the gates.

---

4. The files provided

• The puzzle provided the two sets of files :

Set I (Main Puzzle)

Set II (Warmup)

• The warmup puzzle is a small example design and was run through the same RTL to GDS flow, to obtain the GDS file (similar to main puzzle GDS).
• The example design consists of two shift registers, an adder, and a comparator, outputting success if A + B == 496.
• The whole flow was carried out using SkyWater's 130 nm PDK, see more.

• Two 8-bit shift registers fed from A and B, a 9-bit adder, and a comparator against 496. en gates the shifting and S falls straight out of the compare, so there is no state beyond the two registers.

---

Note : The Layout image provided reveals the following I/O,

---

Note :

• I ran the three puzzle files through exiftool for a preliminary check and found nothing interesting.

---

• The waveform (of the puzzle's VCD file) looks like :
• Notice the "success" flag remains low throughout.

---

4.1 The full file set a real RTL to GDS flow produces

• A puzzle GDS is the tail end of a much longer pipeline.
• Below is every file an open source flow, Yosys, OpenROAD, Magic, Netgen, the tools behind OpenLane, touches on the way from RTL to a tapeout ready GDS.
• Skipped: behavioural simulation and functional verification (UVM, assertions). Both check that the RTL is correct, neither produces a file that carries into physical design, so the table below picks up with a netlist already synthesised and already through DFT.

• Six formats do essentially all the work across those sixteen stages: .v (logic, at whichever stage), .lib (what a cell computes and how fast), .sdc (the clock period and I/O timing the design has to hit), .lef (a cell's physical footprint and routing rules), .def (where cells sit and how nets are routed), .gds (the shapes actually sent to the fab).
• .upf, .spef, .sdf, .cdl and every signoff report sit downstream of one of those six. They describe timing, power or manufacturing correctness. None of them describe logic.

4.2 What we were actually given

• .lib and .lef are the only two files shared across both puzzles, and both are given once for the whole PDK rather than per design: one voltage and temperature corner, no fast or slow corner, no multi corner set at all.
• The warm-up hands over four of the sixteen stages' outputs directly (source, netlist, netlist with power rails, post route DEF), so its GDS could be checked against something, not solved from nothing.
• The puzzle hands over exactly one, the GDS itself, stage 12 of 16, with cell and net names stripped out. That is the entire reason section 12's extraction algorithm was needed at all.

4.3 Did the missing files matter

• No.
• .sdc bounds clock period and I/O delay for timing signoff. It says nothing about what a cell or a net does, so dropping it costs nothing when the goal is function, not frequency.
• .upf only matters once a design crosses power domains or needs level shifters and isolation cells. 02_netlist_with_power_rails.v shows one VPWR and one VGND net feeding every cell, one domain, so there was never anything for a UPF to describe.
• The intermediate .def files, floorplan, placement, CTS, only show how the place and route tools converged on a layout. The final DEF or the GDS already contains where every cell ended up, which is the only fact the extraction in section 12 needs. The intermediate steps would have shown the tool's working, not new information.
• .spef, timing reports and .sdf describe delay. Every stage of this recovery, extraction, the equivalence proof, the SAT solve, runs on the netlist's logic, not its speed. Gate level simulation against the Liberty function tables (section 18) is exact regardless of delay.
• .cdl and the DRC/LVS reports confirm the layout matches its own netlist and obeys the fab's manufacturing rules. Questions about whether this one chip is manufacturable, not about what it computes.
• The one gap that was ever felt was a second .lib corner, and only as a sanity check: the function tables in section 18 fix what a cell does, and function does not change across corners, so even that gap cost nothing.
• The file that would have helped is the one the puzzle deliberately withholds: the RTL source. Every other file in the section 4.1 table is a restatement of the same logic in a different form, and none of those restatements is the logic itself.

---

5. The first breakthrough

• Switching to ASCII (I rarely use ASCII and prefer staying in Decimal/Hexadecimal/unsigned Integer) was the first breakthrough, I was on the blog site, and my eyes fell on :

---

• It was at this point while viewing the waveform when I decided to switch to viewing the VCD file in ASCII.
• Which revealed the following message "TRY AGAIN" (at 1255000 ps marker):

---

6. What the circuit turned out to be

• The chip is an 11 x 11 Star Battle validator, the puzzle also known as Two Not Touch.
• A 121-bit grid is shifted in serially on I, one cell per rising clock while enable is high, row-major.
• On the following edge it raises success if the grid places exactly two stars in every row, every column and every one of eleven irregular regions, 22 stars in total, with no two stars adjacent, diagonals included.
• It then streams an ASCII verdict out of O[7:0], one character per clock.
• The recovered RTL in 08_recovered_rtl.v is one flat module, because that is what the netlist is: synthesis flattened the hierarchy and the layout keeps no record of it.
• Written as a hierarchy, the same 728 cells are the blocks below, and each one occupies a contiguous region of the die.

• (†) : 4 bits because each row and each column holds 11 cells.
• The design uses 2-bit saturating counters to add up to check row/column/region counts

• The same nine blocks as a diagram. clk and rst_n reach every block and are drawn as a note rather than as nine wires. Below is where they actually sit on the die.

---

7. Quick start

• The pipeline is one Python file.

Install

• RUN.sh creates .venv and installs requirements.txt on first run, so on every platform the install is: get python, get iverilog, run the script.
• It takes about 3 seconds end to end and rebuilds warmup-solution/ and puzzle-solution/ from scratch every time.

Ubuntu / Debian

git clone https://github.com/NotCleo/GDS-to-RTL.git
cd GDS-to-RTL
sudo apt install iverilog python3-venv python3-tk tree -y
bash RUN.sh

• I do not own a Mac/Windows machine, so I made Opus 5 write this below two sections (please open an issue if it fails)

macOS

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"
brew install python icarus-verilog git tree python-tk
git clone https://github.com/NotCleo/GDS-to-RTL.git
cd GDS-to-RTL
bash RUN.sh

Windows

wsl --install -d Ubuntu

• Then open the Ubuntu shell and follow the Ubuntu block above.

Running it

bash RUN.sh                   the warm-up, which validates the toolchain, then the puzzle
bash RUN.sh --only warmup     just the warm-up
bash RUN.sh --only puzzle     just the puzzle
bash RUN.sh --no-iverilog     skip the two independent-simulator checks

To view the results

tree puzzle-solution warmup-solution

• Every file in those two directories is listed and explained in section 35.
• The captured output of a full run is in RUN.log, the pipeline's own stage-by-stage log is in GDS-to-RTL/run.log, and every stage is described with its numbers in GDS-to-RTL/summary.md.
• Neither viewer below is needed to reproduce anything.

Optional, only if you want to look at the waveforms by hand

mkdir -p ~/surfer_install && cd ~/surfer_install
wget "https://gitlab.com/api/v4/projects/42073614/jobs/artifacts/main/raw/surfer_linux.zip?job=linux_build" -O surfer_linux.zip
unzip surfer_linux.zip
chmod +x surfer
mkdir -p ~/.local/bin
mv surfer ~/.local/bin/
export PATH="$HOME/.local/bin:$PATH"
surfer puzzle-solution/14_success_inputs.vcd

• Open O[7:0] and set its format to ASCII.

What it is built from

If you have your own GDS

• The extractor is not specific to this puzzle, so it is also packaged on its own, in General-GDS-to-RTL/.

• Point it at any sky130 layout:

    python3 General-GDS-to-RTL/gds_to_netlist.py mychip.gds
    python3 General-GDS-to-RTL/gds_to_netlist.py mychip.gds -o out/
    python3 General-GDS-to-RTL/gds_to_netlist.py mychip.gds --def mychip.def --golden golden.v
    python3 General-GDS-to-RTL/gds_to_netlist.py mychip.gds --lef other.lef --lib other.lib
    python3 General-GDS-to-RTL/gds_to_netlist.py --show-layers
  

• The main pipeline is untouched and does not know it exists.

• Every cell's function comes out of the Liberty file, so a netlist of known functions is already a system of boolean equations, one per net.
• Substituting each equation into its consumer would expand a cone into an expression exponential in its depth, which is why fully expanding a counter produces megabytes, so a net keeps its own line when more than one thing reads it, when it is a port, when it holds state, or when folding it in would pass sixteen terms, and is folded in otherwise.
• The result is then run against the gates: exhaustively for a combinational design small enough to enumerate, over two thousand clocked cycles otherwise.
• Synthesis is not reversible!
• It flattens the hierarchy, deletes every name the layout did not keep as a label, and many different sources compile to the same gates, so nothing gets the original always blocks back.
• The RTL in puzzle-solution/08_recovered_rtl.v was written by hand from an understanding of the gates and then proved cycle-equivalent to them.
• Both are equivalent to the gates.
• Only the hand-written one says the circuit is an 11x11 Star Battle validator.
• What the structure report does is tell you where to look, and General-GDS-to-RTL/README.md says how to read it.
• For a PDK that is not sky130, --show-layers prints the layer table in the shape that --layers accepts, and you pass that PDK's own --lef and --lib.

---

8. Three ways to make success go high

• The chip is a validator. It checks a grid, it does not produce one.
• So once the RTL was recovered, the work left was to solve an 11 x 11 Star Battle and feed the answer in.
• There are three ways to do that, and all three are in this repository.

• SAT is what the pipeline runs, and it is the strongest of the three because it never looks at the region map. The question goes to the gates, so the answer is a property of the netlist and not of my reading of it. It also returns two facts the other two cannot: that 121 edges cannot work and 122 can, and that the key is unique. Section 25 is the whole of it.
• Paper is the route a person reaches for first. It works, and it is how the SAT answer got its first check, but it proves nothing about the circuit and it only solves the one puzzle.
• RTL is the only one of the three that stays in hardware. No Python and no solver library, just a second module wired to the recovered one. Section 32.

---

• Sections 9 to 31 are the pipeline in the order it ran.
• Every number in them is printed by GDS-to-RTL/gds_to_rtl.py on a fresh run, and the run that produced them is in RUN.log.

---

9. What is in a GDS file

• I started with puzzle/puzzle.gds, 1.4 MB.
• A GDS is a geometry file and nothing else.
• It stores polygons, each tagged with a layer number and a datatype, plus cell definitions that can be placed at a position with a rotation and an optional mirror.
• There is no wire, no gate, no pin and no connection anywhere in the format.
• Two pieces of metal are connected if and only if they physically overlap, and the file never records that they do.
• It has to be computed from coordinates.

• One thing survived, and it mattered enormously: the standard cells are still named.
• sky130_fd_sc_hd__nand3_2 says exactly what that cell does, because the PDK that defines it is public.
• What the flow stripped is everything above the cell: which instance is which, what the nets were called, and how the design was organised.
• Before writing any code I opened it in the Tiny Tapeout online GDS viewer, which needs no install and renders every layer at once.
• Staring at it explained nothing about the circuit. 9,875 placements with no labels look like 9,875 placements with no labels.
• It did show one thing, in the default view, without turning a single layer off: a pale rectangular block low on the die that does not look like routing.
• I switched to GDS3D to isolate it, because GDS3D can hide the power grid and separate the metal stack, and the block is on met2 with nothing under it.

Easter egg 1: the logo in metal 2

• Routing on a metal layer is long power straps and short jogs between vias.
• This was neither.
• 1,366 sub-micron polygons packed into a 17.10 x 17.10 um square, connected to nothing at all, over a piece of die with no cells beneath it.
• It is the Jane Street logo, drawn in real mask geometry, and the warm-up GDS carries it too at a different corner.
• Details and the rasterised version: Easter-Eggs/01_easter_egg.txt.
• That is everything looking at the layout produced.
• Everything after this is computed.

---

10. What to build first, and what to check it against

• The challenge asks for a netlist extractor, so one has to be written.
• The problem that comes with it: suppose I write it, point it at puzzle.gds, and it emits a netlist.
• How would I know that netlist is right?
• A netlist can parse cleanly, have every pin connected, have exactly one driver per net, and still describe a different circuit, because one missed overlap splits one net into two and nothing anywhere reports an error.
• The puzzle ships a warm-up, and the warm-up ships golden references, which is the only ground truth available anywhere in this exercise.

---

11. Inventory, before any connectivity work

• Stage W1 and P1. gdstk reads the GDS into a cell hierarchy; the code walks top.references, buckets each placement by its cell name, and dumps every label with its layer and coordinate.
• No geometry is interpreted here and nothing is connected.
• It is counting, so that I know what is in the file before deciding what to do with it.
• Output: 01_gds_inventory.txt in each solution directory.

• The warm-up is 79 logic cells: two shift registers, an adder, a comparator and three clock buffers, which is small enough to read by hand.
• That is the point of it.
• The 17 top-level labels on the puzzle are the ports, and they are the last real names left anywhere in the file:

'I'        on layer 70/5 at (  0.30,  79.22)
'clk'      on layer 70/5 at (  0.30, 238.34)
'rst_n'    on layer 70/5 at (  0.30, 185.30)
'enable'   on layer 70/5 at (  0.30, 132.26)
'O[0]'     on layer 70/5 at (199.70, 204.34)   ... through O[7]
'success'  on layer 70/5 at (199.70, 285.94)

• Inputs down the left edge, outputs down the right, exactly as the hint image in section 12 draws them.

---

12. Turning polygons into a netlist

• Stage W2 and P2. The tools are gdstk for the hierarchy, shapely for polygons and its STRtree R-tree index for spatial lookup, numpy for the coordinate arithmetic, and a union-find over integer node ids.
• The algorithm is four steps.

• Step 2 is the whole cost: it is an all-pairs proximity question over 35,531 polygons, and without a spatial index it is quadratic and unusable.
• Two polygons on the same layer are treated as one conductor if they come within 60 nm of each other.
• Section 21 shows the recovered partition does not depend on that number.
• Output: 02_extracted_netlist.v.

Note on shapely. 2.0 changed STRtree.query to take a predicate argument and to return integer indices rather than geometries. On shapely 1.8 that call signature does not exist, and the code silently builds a different netlist rather than failing. 2.0 is a hard floor, and requirements.txt pins it.

---

13. Three bugs, each of which produced the wrong circuit

• None of the three crashed.
• All three produced a netlist that parsed, had no dangling pins, had exactly one driver per net, and described a circuit that is not on the die.
• Each was caught by the warm-up comparison in section 14 and by nothing else.

• The pin one is not a rare edge case.
• Among the 66 cell types the puzzle uses, 172 of 285 signal pins are a single rectangle, so the naive reading works most of the time and fails exactly where it hurts.

• clkbuf_16 is the root of the entire clock tree, and its output pin is 20 separate rectangles.
• The diode one only surfaces with ground truth.
• The netlist without diode bridging had the right cell count, no dangling pins and no visible defect anywhere.
• It just described a different circuit.

---

14. Proving the extractor exact

• Stage W3 and W5. W3 compares my extraction against the shipped DEF and golden netlist directly; W5 compiles the golden netlist and my extracted netlist together with iverilog and simulates them side by side under vvp.
• Outputs: 04_golden_crosscheck.txt and 05_equivalence.txt.

• The third row is what settles it, and here is why it works.
• Two netlists are the same circuit exactly when they cut the same set of pins into the same groups, with the same ports attached to the same groups.
• That is a statement about set partitions, and names play no part in it.
• So the extraction can be proved exact while every instance in it is still called u17 and every net net_412.
• The DEF match is not part of that proof.
• It is there to put the names back afterwards, which is what 07_name_map.json holds.
• At this point the extractor is finished and validated, and the warm-up has one job left.

---

15. Solving the warm-up from its gates alone

• Stage W6. The extractor has been proved exact, but nothing yet says what the circuit does, and working that out from gates is the part that has to carry over to the puzzle.
• warmup/00_source.v is sitting there with the answer in it.
• This is the one chance to try a technique on a problem whose answer can be checked afterwards, so that file is not opened.
• The question: is there an input sequence that drives S high, and what is the shortest one?

Why a solver

• The third also answers something the other two cannot.
• UNSAT is a proof. "No input of K edges works" is not "I did not find one", it is "there is not one".

What kind of SAT this is

• Not plain combinational SAT.
• The warm-up has 16 flip-flops and the puzzle has 92, so what the circuit does depends on what it has already been shown.
• The technique is bounded model checking, and section 25 covers the encoding it rests on.

• Two things make the sweep cheap rather than expensive.
• The formula for depth K is a prefix of the formula for K+1, so the pipeline encodes once at the largest depth it needs and asks the shorter questions by asserting the goal literal one step earlier, as an assumption.
• The encoder folds any gate whose inputs are already constant, and after reset most of the design is constant for the first several steps.

Which solver

• python-sat bundles several CDCL solvers behind one interface.
• Rather than pick one on reputation I timed all of them on this design's own two workloads, the depth question and the fourteen incremental enumeration queries of section 27, and took the fastest total.
• Same formula, same machine, best of three.

• The depth question is small enough that every one of them is inside a rounding error of the others.
• The enumeration separates them, because it is fourteen incremental queries against a solver that has to keep and reuse what it learned between them, and that is where CDCL implementations differ.
• CaDiCaL 3.0 wins, so that is what SAT_BACKEND names in the pipeline, and it is the only line that has to change to swap it.

What came back

• Unroll the extracted warm-up gates, encode, ask, sweep K:

one unrolling to 11 edges: 362 variables, 1012 clauses

K =  6 edges   UNSAT
K =  7 edges   UNSAT
K =  8 edges   SAT
A = 11111000 = 248
B = 11111000 = 248
A + B = 496

• Eight edges, because the warm-up shifts in eight bits.
• No gate was traced by hand and 00_source.v was never opened.
• Output: warmup-solution/06_sat_solve.txt.

Easter egg 7, which is the constant it came back with

• The warm-up raises success when A + B == 496, and 496 is not arbitrary.
• It is the third perfect number, equal to the sum of its own proper divisors:

496 = 1 + 2 + 4 + 8 + 16 + 31 + 62 + 124 + 248

• It is also 2^4 x (2^5 - 1) = 16 x 31, which is Euclid's form 2^(p-1) x (2^p - 1) with p = 5.
• And it is a well chosen constant for an eight-bit adder: A + B ranges over 0 to 510, and A + B = 496 has exactly 15 solutions, A from 241 to 255, out of 65,536 input pairs.
• The solver returned A = B = 248, the largest proper divisor of 496 and the middle of those 15.
• Any of the 15 would have been correct, and an earlier run of this pipeline returned 242 and 254, so the specific pair is the solver's choice and not a property of the circuit.
• That is the one number on this page that is allowed to move between runs.

---

16. The puzzle inventory, and easter egg 2

• Same extractor, no changes, pointed at puzzle.gds.
• Three rows of the inventory table in section 11 do not belong in a standard-cell design, and all three point at the same place.
• **The bounding box came back as `(0.00, -52.72) ..
• (200.00, 300.00)`.** The placement rows of a standard cell design start at y = 0, so something is drawn 52.72 um below the chip.
• The placement histogram buckets anything that is neither a standard cell nor a via, and on the puzzle that bucket is not empty:

21 x INTERNAL_3
15 x INTERNAL_7

• 36 placements of two structures with no pins, no transistors, and names no PDK uses.
• The layer histogram, checked against the sky130 layer map, flagged one layer the map does not know: 200/0, carrying two polygons, one inside each of those two structures.
• Diffing the puzzle's layer set against the warm-up's narrows it further, since both went through the same flow.
• Three layers appear in the puzzle and not the warm-up.
• Two are boring: 66/15 and 81/23 live only inside standard cells, so they are present because the puzzle instantiates conb_1 and diode_2 and the warm-up has neither.
• Only 200/0 is drawn outside every cell, so only 200/0 was added by hand.
• 36 bars, two widths, 1.38 um and 4.14 um, exactly 1:3, all at y = -52.72, spanning x = 1.33 to 198.67.
• Dividing the gaps by the narrow width, every gap is 1, 3 or 7:

widths : . - - . . . - . . - . - . . - . . - - - . - - . . . - . . . - . - . . -
gaps   : 1 1 1 3 3 1 1 7 1 3 1 1 3 3 1 3 1 3 1 7 1 3 1 1 7 1 3 1 1 3 3 1 1 3 1

• Short mark, long mark at 3, gap 1 inside a letter, 3 between letters, 7 between words.
• That is International Morse timing exactly, and it decodes with no ambiguity to:

PER ARENAM AD ASTRA

• Latin, roughly "through the sand, to the stars", a play on per aspera ad astra.
• Full decode: Easter-Eggs/02_easter_egg.txt.

---

17. The layer map, the via census, and the puzzle netlist

• Stage P2. The four-step algorithm in section 12 needs one thing before it can run: which GDS layers are conductors, which are cuts, and which are neither. sky130's layer map answers that.

• Grouping the overlapping shapes per conductor layer on the puzzle:

• Checking the coordinate transforms without an answer key. Every via cut has to land on metal on both sides.
• If a rotation or a mirror were applied wrongly, cuts would sit with metal on one side only.
• This check needs no golden file, so unlike section 14 it works on the puzzle too:

cut mcon   li1  -> met1 : 17188/17188 bridged
cut via    met1 -> met2 :  3779/3779  bridged
cut via2   met2 -> met3 :   951/951   bridged
cut via3   met3 -> met4 :   687/687   bridged
cut via4   met4 -> met5 :   108/108   bridged

• 22,713 of 22,713 cuts bridged, none floating.
• The design that came out:

• Zero shorts, zero floating outputs and zero undriven nets on both designs.
• That last row matters because a single unrecovered connection splits one net into two, and the circuit becomes a different circuit with no error reported anywhere.
• The result is a plain structural Verilog netlist, puzzle-solution/02_extracted_netlist.v:

// Recovered from puzzle/puzzle.gds by geometry alone.
// No netlist, DEF or source file was read to produce this.
// 728 logic cells, 738 nets, 0 nets with a driver count other than one.
module puzzle_extracted (I, clk, enable, rst_n, success, O);
  input  I;
  ...
  sky130_fd_sc_hd__xor2_2  u12_xor2_2  (.A(net_268), .B(net_256), .X(net_260));
  sky130_fd_sc_hd__a21oi_2 u13_a21oi_2 (.A1(net_244), .A2(net_245), .B1(net_240), .Y(net_246));
  sky130_fd_sc_hd__nand2_2 u14_nand2_2 (.A(net_200), .B(net_649), .Y(net_255));
  sky130_fd_sc_hd__a22o_2  u15_a22o_2  (.A1(net_051), .A2(net_653), .B1(net_272), .B2(net_296), .X(net_276));
  ...
  sky130_fd_sc_hd__and3_2  u23_and3_2  (.A(net_139), .B(net_140), .C(net_135), .X(O[0]));
endmodule

• 728 instances and 738 nets, with no meaningful names in it, which is exactly as far as geometry can take anyone.

---

18. Cell semantics, and what the PDK gets wrong

• Stage W4 and P3. A netlist of cell names is useless without knowing what the cells do.
• That comes from the sky130 Liberty file, which is the same file the synthesiser read when it built this design in the first place.
• The pipeline parses it and generates simulation models: 03_cell_models.v.
• For combinational cells, each output pin carries a boolean function:

cell ("sky130_fd_sc_hd__xor2_2") {
    pin ("X") { direction : "output";  function : "(A&!B) | (!A&B)"; }
}

• For sequential cells, an ff group names the state pair, its clock, its next state, and its level-sensitive clear or preset:

cell ("sky130_fd_sc_hd__dfstp_2") {
    ff ("IQ","IQ_N") { clocked_on : "CLK";  next_state : "D";  preset : "!SET_B"; }
    pin ("Q") { direction : "output";  function : "IQ"; }
}

• That is enough to derive every cell, so no truth table is written by hand anywhere in this repository.
• The same parsed functions are used by the simulator and by the SAT encoder, which keeps the simulated circuit and the solved circuit literally the same object rather than two descriptions that have to agree.
• It also settles reset polarity, and that one is load-bearing: dfrtp has a clear and resets low, dfstp has a preset and resets high.
• This design has four dfstp_2, so any tool option that zeroes every flop at reset turns it into a circuit with no solution at all.
• Four things in the PDK are worth flagging, because each has a reading that parses cleanly and is wrong.

• A secondary one, less interesting but worth knowing: the human-readable equations in the comment headers of the PDK's own Verilog models do not always agree with the cell they sit above.
• The machine-generated Liberty function strings are consistent, so those are what I parse, and I never read the comments.
• Generated models: puzzle-solution/03_cell_models.v.

---

19. The sample waveform: easter eggs 3, 4, 5 and 6

• With a netlist and no description of its behaviour, I went back to the one file I had been ignoring: puzzle/example_inputs.vcd.
• First in a text editor, which I had not done.
• The first nine lines hold two easter eggs.
• Easter egg 3, the $version field:

Leave no stone unturned! But for this file, consider looking at it in a
waveform viewer instead.

• No simulator writes that. iverilog writes "Icarus Verilog", so the line was put there by hand.
• Easter egg 4, two lines above it, the $date field:

Sat Dec 31 23:59:60 2016

• A second numbered 60, which most date parsers reject because most date libraries assume a minute has 60 seconds numbered 0 to 59.
• It is a leap second, and a real one: 2016-12-31 23:59:60 UTC is the most recent leap second inserted, so that minute had 61 seconds.
• It was a Saturday.
• Then the same file in Surfer, which gave nothing useful.
• success is low for the whole trace.
• O[7:0] sits at zero, changes nine times in a burst near the end, and goes back to zero.
• As hex that burst is 54 52 59 20 41 47 41 49 4e, which says nothing as a number.
• I read it in decimal, hex and binary, got nothing, and moved on.
• Easter egg 5 is what fixed that, and it is not in any file.
• Re-reading the puzzle statement, the blog post links in passing to another Jane Street post about using ASCII waveforms to test hardware designs.
• Read as a curiosity it is a curiosity.
• Read as an instruction it is what makes the output side readable.
• I do not normally display a bus as ASCII.
• One right click later, those same nine bytes read:

T R Y   A G A I N

• So the chip does not return a status code, it returns text.
• The block the hint image says to ignore is a ROM of English sentences, and the sample waveform is a recording of a wrong grid being rejected.
• That pointed the same question at the input side, and the input side is easter egg 6.
• Two counts point at it before any decoding: both frames of the sample contain exactly 38 ones, identical rather than similar, and in both frames columns 7 through 10 are empty in every row, a perfectly rectangular block of 44 dead cells.
• Eleven rows, seven usable columns each.
• Standard ASCII needs seven bits.
• So group the bits in sevens, one row per character, least significant bit first:

. . 1 . 1 . 1 . . . .   0010101 ->  84 -> 'T'
. . . 1 . 1 1 . . . .   0001011 -> 104 -> 'h'
1 . 1 . . 1 1 . . . .   1010011 -> 101 -> 'e'

• Frame 0 gives The night s, frame 1 gives ky awaits .

The night sky awaits

• The file I had written off on day one carries the theme in its inputs.
• Full decode, all 22 rows: Easter-Eggs/06_easter_egg.txt.

The interface, measured rather than assumed

• The same file settles the protocol, which up to here I had been guessing at.
• The method is counting rising edges of clk in the recorded trace and reading what each signal does on each one.

• 121 = 11 x 11. So it is a fixed 121-cell frame, not a free-running stream, and the verdict begins on the edge immediately after the frame ends.
• That is where the 121-bit frame and the 122-edge window come from, and both get proved from the gates in section 25 rather than left as a reading of one trace.

---

20. Checking the netlist against the recorded chip

• The sample waveform is a recording of the real chip: known inputs, known outputs.
• That makes it a test the extracted netlist has to pass, and one that could not have been fitted to, because the trace existed before my extractor did.
• Stage P4. The pipeline's own bit-parallel simulator replays the recorded inputs into the extracted netlist and compares every output at every rising edge:

312 rising edges replayed, 624 outputs compared, 0 mismatches

• A netlist built from polygon coordinates alone reproduces the recorded silicon at every edge.
• From here on, wherever the netlist and a hypothesis disagree, the netlist is taken as correct.
• If P4 ever reports a mismatch the pipeline stops, because every later stage would be interpreting a circuit that does not exist.
• Output: puzzle-solution/04_vcd_replay.txt.
• The same stage checks the clock tree, which would otherwise be an assumption.
• There are 32 clock buffers in three levels, one clkbuf_16 feeding 16 clkbuf_8 feeding 15 clkbuf_4, and every one of the 92 flip-flop clock pins traces back through them to the single primary input clk.
• There is no gated clock anywhere in this design, so the whole thing can be reasoned about one rising edge at a time, which every later stage relies on.

---

21. Register-level structure

• 728 anonymous cells, known correct, and not understood at all.
• Reading them gate by gate does not work, for a specific reason rather than a vague one.
• Combinational logic does not survive synthesis in any recognisable form.
• The optimiser is free to rewrite any acyclic block of gates into any other block with the same truth table, and it does, so the shape on the die is the shape the optimiser preferred, not the shape anyone wrote.
• Net net_412 corresponds to nothing in anybody's source file.
• Flip-flops are different. A flop is a physical cell with a name in the library, it holds a value across a clock edge, and no optimiser can make it not do that.
• So the flops are real objects, and the useful question is not what each gate does but which flops feed which.

The graph

• Stage P5. Build a directed graph with one node per flip-flop, and an edge from a to b when a's output reaches b's data, clear or preset input through combinational logic only, not through some third flop.
• Constructing it means walking backwards from each flop's D through the gate cone and stopping the moment a flop output or a primary input is reached.
• 92 nodes.
• Cheap to build, and it throws away exactly the part that was not meaningful.

Why cycles are the thing to look for

• A cycle in that graph means a flop's next value depends on its own current value.
• That is precisely the difference between state that accumulates and state that merely delays.
• A shift register is a chain, so it is a path and has no cycle.
• A counter has to look at its own value to know what to count to next, so it has one.
• Same for accumulators, and for any state machine whose next state depends on its current state.
• The reason this is worth building a graph for, rather than being a preference, is that a synthesiser cannot remove a cycle.
• It can retime a loop, re-encode it, or merge flops inside it, but it cannot turn it into a directed acyclic graph, because a DAG has a bounded memory of the past and a loop does not.
• Feedback is a behavioural property, not a syntactic one.
• So the cycles in the register graph are the one structural feature of the original design guaranteed to still be there after everything else was optimised away.

Why Tarjan

• What I want is not "is there a cycle" but "what are the maximal groups of flops that can all reach each other".
• That is the definition of a strongly connected component, and Tarjan's algorithm computes all of them in a single depth-first traversal, in time linear in nodes plus edges.

• Tarjan gives the answer in one pass and the implementation is 30 lines.
• Output: puzzle-solution/05_register_structure.txt.

What came back

• Twenty-three groups of exactly two flops. Two bits of state that update together and look at each other, which is a two-bit counter, twenty-three times over.
• Simulating them later confirms it, and confirms something a little unusual: they saturate at 3 rather than wrapping, so each one counts up to two and then records that it overflowed instead of rolling back to zero.
• That is why there is no magnitude comparator anywhere on this die.
• Counting to exactly two and comparing for equality is cheaper than counting properly and comparing for greater-than.
• One group of nine, whose external inputs are enable and rst_n but not I. Nine bits of feedback state that never look at the data, so something that tracks where you are in the frame rather than what is in it.
• One group of eight, whose external inputs include I. Eight bits driven by the data, so a byte-wide accumulator of some sort.
• One group of four with no external inputs whatsoever. Four flops that talk only to each other and to nothing outside, so something that free-runs once started.
• Those four are also the four dfxtp_2, the only flops in the design with no reset at all, which is why section 30 has to prove their power-up state does not matter.

The one thing worth decompiling

• success is a single flip-flop, u28_dfrtp_2, and it is not in the list above because its feedback group has size one: it feeds only itself.
• Its set condition is a wide AND tree, and unlike the counters that tree is worth expanding through the combinational logic and printing, stopping at flop outputs and ports:

D = (((!u390.Q & (!u419.Q & (((u451.Q & u449.Q) & u460.Q) & ((!u459.Q & !u461.Q)
  & !(((u453.Q | u447.Q) | u454.Q)))))) & (((!u26.Q & u350.Q) & ((((((
  !u622.Q & u600.Q) & (u596.Q & !u614.Q)) & (!u232.Q & u601.Q)) & (!u625.Q
  & u597.Q)) & ((((u647.Q & !u651.Q) & (!u661.Q & u595.Q)) & (!u603.Q &
  u634.Q)) & (u635.Q & !u602.Q))) & (((!u215.Q & u197.Q) & (u233.Q &
  !u231.Q)) & (!u226.Q & u198.Q)))) & ((((((!u106.Q & u178.Q) & (u107.Q &
  !u179.Q)) & (!u121.Q & u153.Q)) & (!u108.Q & u180.Q)) & ((((u190.Q &
  !u118.Q) & (!u194.Q & u209.Q)) & (!u126.Q & u188.Q)) & (u117.Q & !u189.Q
  ))) & (((!u122.Q & u141.Q) & (u142.Q & !u124.Q)) & (!u123.Q & u143.Q))))
  ) | (u28.Q & (u26.Q | !u350.Q)))

• Read for structure rather than detail, there is one group of eleven near-identical two-bit comparisons, (!u622.Q & u600.Q), (u596.Q & !u614.Q) and so on.
• Then a second group of eleven more of exactly the same form.
• Then one separate eight-flop comparison against a fixed pattern, u451 & u449 & u460 & !u459 & !u461 & !(u453 | u447 | u454).
• And the whole thing ORs with u28.Q, which is the self-loop: once high, success stays high.
• Eleven of one thing, eleven of another, one eight-bit thing, everything compared against two.
• The same treatment applied to any of the 23 counter pairs expands into megabytes of repeated subexpression, because a counter's cone reaches the same nets by many different paths and a printed tree has no way to share them.
• So decompiling works for the control logic and fails completely for the counters, which is why the counters get probed instead, in section 24.

---

22. Where the counters sit on the die: easter egg 8

• The blog post says the circuit is physically arranged to hint at what it does, so look closely at the layout.
• Looking at the layout directly gives nothing: 9,875 placements, none of them labelled.
• But my extractor numbers instances uNNN by their position in the GDS reference list, so once the counters are identified by name, uNNN back to (x, y) is a lookup rather than a search.
• That is why this egg comes now and not in section 9.
• The layout does hint at the function, but only to someone who already has the netlist.

• The whole checker is a single vertical column at x = 114.8 to 126.3 um on a die 200 um wide: eleven, a gap, eleven, plus one off to the side.
• Twenty-three, which is the number the SCC analysis gave, arranged in a way that says the twenty-three are not interchangeable.
• That arrangement also explains why there are 23 counters and not 33.
• Eleven rows plus eleven columns plus eleven of whatever the third family is would be 33.
• The missing ten are the rows: the grid streams in one cell per clock, row-major, so only one row is ever in flight, and a single counter cleared at each row boundary serves all eleven rows.
• Columns and the third family are interleaved across the whole frame, so each one needs its own counter that persists for the entire 121 cycles.
• So the floorplan gives the input format as well as the shape of the rule set, and it says there is a third constraint family I have not identified.

---

23. The first hypothesis, and why it was wrong

• At this point the gates have said the following, with no interpretation on my part:

• Two of something per row and two per column, on an 11 x 11 grid of bits, is a description of a well known family of pencil puzzles: Star Battle, also called Two Not Touch.
• That family adds a rule the counters cannot express: no two of the marked cells may touch, not even diagonally.
• So the working hypothesis was the whole family at once: two stars per row, two per column, and no two adjacent including diagonally.
• A note on the word "star", because nothing in the gates says it.
• The gates say "exactly two ones per row".
• The word comes from the two easter eggs already in hand: the input frames of the sample waveform spell The night sky awaits, and the Morse bar code under the die spells PER ARENAM AD ASTRA, to the stars.
• That is a naming convention and not a constraint, and nothing that follows depends on it being right.
• Stage P6. The hypothesis is tested rather than assumed: z3 is asked for 25 grids that satisfy it perfectly, and all 25 are fed into the extracted netlist through the bit-parallel simulator.

25 grids satisfying two per row, two per column, no touching
accepted by the netlist: 0
what the chip said instead: {'TRY AGAIN': 25}

• Twenty-five generated, zero accepted, and the chip answered the same way to all of them.
• Two conclusions follow.
• There is a constraint I have not found, almost certainly the third family of eleven counters.
• And reading gate cones will not find it, because section 21 already showed the counter cones are unreadable.

---

24. Probing one grid cell at a time

• The eleven unidentified counters each watch some set of grid cells.
• Their logic is unreadable, so they get measured instead.
• Stage P7. The experiment is the simplest one available:

For each of the 121 grid positions in turn, run the chip with a one at that position and zeros everywhere else, and record which counters increment.

• If counter 4 ticks when the only one in the frame is at cell (3, 7), then cell (3, 7) belongs to whatever counter 4 is watching.
• That is 121 separate runs of a 121-cycle frame, and it takes 0.04 seconds, because the pipeline's simulator packs one trial per bit of a Python integer and runs all 121 in a single pass.

column counters 11   irregular groups 11   shared row counters 1

• The rows come back as zero, which is what the 23-versus-33 argument in section 22 predicted, and the way they come back as zero confirms the input format.
• The row counter is cleared at every row boundary, so at the end of the frame it always reads zero no matter what went in.
• Sampling it in the cycle each one arrives instead, it moves in 110 of 121 trials, and the 11 it misses are exactly cells

10  21  32  43  54  65  76  87  98  109  120

• which is column 10 of every row: the last cell of a row, where the counter is bumped and cleared on the same edge. 110 = 121 - 11.
• A single shared row counter only works if the grid arrives row-major at one cell per clock, so that measurement is a direct confirmation of the protocol read off the waveform in section 19.
• And the eleven mystery counters watch eleven irregular contiguous blobs whose sizes sum to exactly 121.
• They tile the grid:

     0  1  2  3  4  5  6  7  8  9 10
  0  A  A  A  A  A  B  B  C  D  D  E
  1  A  A  F  A  A  B  C  C  D  D  E
  2  A  A  F  B  B  B  B  C  C  D  E
  3  A  A  F  B  G  G  G  E  C  C  E
  4  F  A  F  B  G  E  E  E  E  E  E
  5  F  F  F  B  G  G  G  E  H  H  H
  6  B  B  B  B  B  B  G  E  H  I  I
  7  B  J  J  J  G  G  G  E  H  I  I
  8  B  J  J  K  E  E  E  E  H  I  I
  9  B  B  J  K  K  E  E  E  H  H  H
 10  B  J  J  K  E  E  E  E  E  E  E

region sizes  A=14 B=21 C=7 D=5 E=28 F=8 G=11 H=9 I=6 J=8 K=4   sum = 121

• Irregular regions that tile the board, two per region, two per row, two per column, no touching.
• That is Star Battle exactly, and the missing constraint was the regions.
• The 25 grids of section 23 all failed because none of them respected regions, which I did not know existed.
• Output: puzzle-solution/06_region_map.txt.

---

25. Finding the 121 bits

• This is the largest stage in the pipeline, and the whole result rests on it.
• Stage P8, and everything in it runs on the extracted netlist plus the Liberty functions, with no knowledge of what the puzzle is.

25.1 What is actually being asked

• Let the frame be a vector of 121 boolean variables,

x = (x_0, x_1, ..., x_120),   x_i in {0, 1}

• where x_i is the bit presented on I at the i+1-th enabled rising edge.
• Row-major, so x_i is grid cell (row i div 11, column i mod 11), from the protocol measured in section 19 and confirmed in section 24.
• The chip is a deterministic finite state machine.
• Write s_t for the contents of its 92 flip-flops after t clock edges, s_0 for the state reset leaves behind, and d for the one-edge transition the gates implement:

s_(t+1) = d(s_t, x_t)

• success is one bit of s_t, so define

F(x) = the value of success in s_122

• which is d composed with itself 122 times, starting from s_0, driven by the 121 bits of x and then by whatever I happens to be on the last edge.
• Every part of F is known exactly: 728 gates whose behaviour came out of the Liberty file and which have already been checked against a recording of the real chip in section 20.
• Two questions:

does there exist x* with F(x*) = 1?           and is x* the only one?

• Note what is not in that statement.
• There is no hidden key, no unknown constant, no parameter being fitted.
• The circuit is fully known; what is unknown is which of its 2^121 possible inputs it accepts.

25.2 The size of the space, and two cheap outs I checked first

2^121 = 2,658,455,991,569,831,745,807,614,120,560,689,152
      = 2.658 x 10^36

• At a billion frames per second a sweep takes 8.4 x 10^19 years, about six billion times the age of the universe.
• A sweep is not a slow option, it is not an option.
• Before reaching for a solver I checked whether the structure lets me cheat.
• Is F linear over GF(2)? If it were, the chip would be an LFSR or a CRC, the whole 121-bit frame would be a linear map, and Gaussian elimination would invert it in about 121^3 = 1.8 million operations.
• The definition of an affine map over GF(2) is

F(u xor v) = F(u) xor F(v) xor F(0)

• so it can be tested directly rather than argued about.
• The pipeline runs random frames u, v and u xor v as three lanes of one bit-parallel pass and compares the predicted final state against the measured one across all 92 flip-flops, not just success:

20 of 20 predictions failed

• The state update is nonlinear.
• That kills linear algebra, and it kills every correlation attack that depends on the same property.
• The counters are the reason: a saturating counter is not an affine function of its inputs.
• So: search, but not a blind one.

25.3 Throwing away what cannot matter, the cone of influence

• Not every net in the design can affect success.
• Walk backwards from success through combinational logic and through flip-flops, collecting everything reachable, and stop when nothing new appears.

cone of influence of success: 471 of 738 nets

• The entire output generator falls outside it, which makes sense: O[7:0] depends on success and on the message pointer, and success does not depend on O.
• That drops 267 nets and, once multiplied by 122 time steps, a great deal of formula.
• This is sound rather than heuristic: a net outside the cone cannot change success under any assignment, so removing it cannot change whether the question is satisfiable.

25.4 Making time into space, the unrolling

• A SAT solver has no notion of "later", so time has to become more variables.
• For each step t from 1 to K+1 and each net n in the cone there is a literal L(t, n).
• Three rules define them all.

• So step t settles the combinational logic from the state step t-1 left behind plus the inputs applied on edge t, and then the flops capture.
• L(t+1, n) is what a probe would read after t clock edges, which is the convention that makes the depth arithmetic come out without an off-by-one.
• The free variables are one per (input, step) for I, which is where the 121 bits live.
• rst_n, enable and clk are pinned to 1 across the whole window, because the protocol says the frame is shifted in with reset released and enable high.
• The important consequence: the flops disappear. After unrolling there is no state and no sequencing left, only a large combinational circuit and a lot of variables.
• That is what bounded model checking is for.

25.5 Why the encoder is hand written and not yosys

• The first version of this pipeline used yosys. It returned the right answer.
• It was replaced because of what it could not do, and that decides the shape of the rest of this section.

The one question, and where 122 comes from

• The chip takes a 121-bit frame, one bit per enabled rising edge, and settles success on the edge after the last cell arrives, which is the interface stated at the top of this page.
• 121 cells in plus one verdict edge is a 122-edge window, and that is the unroll depth.
• bounded model checking unrolls a sequential circuit K edges deep into pure combinational logic, assert the property on the frame you care about, hand the result to a SAT solver, and read the inputs off the model.
• yosys implements exactly that as sat -seq K, so it is where I started.

What yosys is

• yosys is an open-source synthesis framework.
• Its day job is the forward direction: read Verilog, elaborate it into generic gates, optimise, and map onto a real cell library.
• sat -seq K is its formal model checking feature: it unrolls the elaborated design K edges deep, encodes the result, and calls a SAT solver built into the binary.

What I did with it

• Roughly this, once per depth:

read_verilog puzzle-solution/03_cell_models.v
read_verilog puzzle-solution/02_extracted_netlist.v
prep -top puzzle_extracted
sat -seq 122 -set-def-inputs -set success 1 -show I

• Read the cell models, read the 728-cell netlist, elaborate, unroll 122 deep, constrain success to 1, print the input trace.

How it went

• It worked, and it gave the right answer.
• What it could not do was amortise, and what it could not express was a second solution.

• The 17 calls differ from each other only in which literals are asserted.
• The formula is the same object every time.
• A command-line invocation cannot keep that object: each run re-parses, re-elaborates and re-encodes before it can assert anything.
• The uniqueness proof and the ROM enumeration are worse than slow, they are inexpressible.
• sat returns one satisfying assignment and has no interface for "now give me a different one", so blocking a model means writing out a new design with that frame excluded and elaborating the whole thing again.

• The decision to move to a Tseitin encoder came out of a question I asked on Mathematics Stack Exchange
• So I wrote the encoder.

25.6 What a Tseitin encoder is

• A SAT solver accepts one input form: conjunctive normal form, a conjunction of clauses, each clause a disjunction of literals.
• A netlist is not in that form, so something has to translate it.
• The naive translation is substitution: replace success by its gate's expression, replace each operand by its own, and recurse until only input variables are left.
• Substitution is exponential.
• Distributing | over & duplicates both operands, so depth d costs O(2^d) terms, and 122 copies of this circuit is thousands of levels deep.
• The formula is unwritable long before it is unsolvable.
• Tseitin's encoding is linear. Mint one fresh variable per gate output and write down only the local equivalence between that variable and its own inputs.
• Nothing is substituted and nothing is expanded.

• Each bundle permits exactly the rows of that gate's truth table and forbids the rest, so the variable is pinned to the gate's output under every satisfying assignment.
• Inversion is free. !x is the literal x with its sign flipped, so an inverter mints no variable and writes no clause.
• Once the Liberty function strings are parsed every cell in the library reduces to AND, OR and XOR over signed literals, which is why the encoder has three shapes and no more.
• The whole circuit is the conjunction of every gate's bundle.
• Cost is 3 or 4 clauses and 1 variable per gate, independent of depth.
• Asking a question is one more clause: the unit clause (success) pins the output high, and the solver either returns a model or proves there is none.
• The encoding is not equivalent to the circuit, it is equisatisfiable. It carries auxiliary variables the circuit does not have, so the two formulas are not the same function.
• What holds is a bijection: every behaviour of the circuit extends to exactly one model of the CNF, and every model restricts to exactly one behaviour.
• That bijection is load-bearing twice over.
• A blocking clause built over the 121 input literals removes exactly one frame and nothing else, which is what makes the uniqueness proof sound; and the same trick over the output bus is what enumerates the ROM.
• Time becomes space by unrolling. Copy the combinational logic once per clock edge, give copy t its own variables, and define copy t+1's flop outputs from copy t's flop inputs.
• A 122-edge question is then a single combinational formula with no sequencing left in it.

25.7 Why Tseitin fits this problem

25.8 What else could encode this, and why I did not use it

• OpenROAD is not needed either. I ran it on the warm-up source early on, to see how much information the forward flow removes before trying to reverse it.

25.9 Making the circuit into clauses, and why the translation is honest

• Section (VI) covers what Tseitin encoding is and why substitution does not work.
• What matters here is the exact statement, because the two results below depend on it being exactly true rather than approximately.
• Write Def(g, t) for the three or four clauses that define gate g at step t, and let

PHI_K  =  reset clauses
          AND  Def(g, t)  for every gate g in the cone and every step t <= K+1
          AND  L(K+1, success)

• Soundness. Take any assignment satisfying PHI_K.
• Each wire variable is pinned by its own clauses to the value its gate produces from its inputs, so reading the assignment off in step order reproduces a genuine simulation of the circuit.
• The last clause forces success high at step K+1.
• Therefore the 121 values assigned to the I variables are a real frame that really unlocks the chip.
• Completeness. Take any frame that unlocks the chip.
• Simulate it, and write every net's value at every step into the corresponding variable.
• Every Def(g, t) is satisfied because the gate really does compute that, and the goal clause is satisfied because success really is high.
• So the assignment satisfies PHI_K.
• The two directions together mean PHI_K is satisfiable exactly when a K-edge unlocking frame exists.
• That is what makes UNSAT a proof rather than a failure, and it is why the encoder folds and shares gates but does nothing that would change the set of solutions.

25.10 How big the formula is, and what the encoder does to shrink it

• Written out naively, one fresh variable and three or four clauses per gate per step:

• The difference is two rules applied while the clauses are being written, both of which preserve the encoded function exactly.

• Folding fires that often for a specific reason.
• rst_n, enable and clk are constants across the whole window, so every gate that depends only on them collapses.
• Every flop's capture expression is (not clr) and (pre or d), and for the 84 dfrtp_2 the preset is a constant 0 while for the 4 dfstp_2 the clear is, so both of those gates fold away at every one of the 122 steps before anything interesting happens.
• And immediately after reset most of the design is holding a known value, so the folding propagates forward through several steps of real logic before it runs out.
• A ninefold smaller formula is not just faster to solve.
• It is faster to build, and building it was the larger cost.

25.11 The depth question, and why one encoding answers both halves

• I want the smallest K for which PHI_K is satisfiable, because that number is the protocol.
• PHI_K is a prefix of PHI_(K+1): the extra clauses all define fresh variables belonging to the extra step, and definitional clauses over fresh variables can always be satisfied whatever the prefix assigns.
• So asking the K-edge question inside the larger formula gives the same answer as asking it in the smaller one.
• In practice the pipeline encodes once at the largest depth it needs and asks the shorter question by asserting the goal literal one step earlier, as an assumption rather than as a clause.

one unrolling to 122 edges   14498 variables   43111 clauses

K = 121 edges   UNSAT
K = 122 edges   SAT

• 121 edges is provably impossible. Not "I could not find one".
• So 121 cells in and the verdict on the next edge is exactly the protocol, and it agrees with the edge count read off the sample waveform in section 19 without ever having looked at it.

25.12 Uniqueness

• The solver returns one satisfying assignment.
• That does not by itself say there is not another.
• Take the 121 input literals from the answer, negate each one, and add their disjunction as a single clause.
• That clause says "not this exact frame" and says nothing about anything else, which is why it is built over exactly those 121 literals and not over the auxiliary variables: two different assignments to the auxiliaries would be the same frame.
• Re-solve.

blocking that assignment and re-solving: UNSAT  ->  the key is unique

• There is exactly one 121-bit frame that unlocks this chip, established at the gate level, without assuming anything about what the puzzle is.

25.13 Why the solver finds it in milliseconds and a sweep never would

• A CDCL solver never enumerates candidates.
• It runs a loop of four things.

• The learned clause is the part that matters.
• It does not remove one candidate, it removes every assignment sharing the responsible pattern, which is typically an enormous region of the space, and it prevents the solver from ever making that class of mistake again.
• For this instance there is a second reason it is easy, and it comes from the shape of the goal.
• success is an AND of 23 two-bit equality tests plus one eight-bit comparison.
• Asserting success = 1 therefore propagates backwards with no search at all: an AND can only be 1 if every input is 1, so all 23 counters are pinned to exactly two and the total is pinned to 22 before a single input bit has been decided.
• The solver starts from an almost fully determined final state and works backwards through the counters to the frame, rather than starting from 121 free bits and working forwards.
• That is why the two depth questions and the uniqueness proof together take 0.02 seconds of solving, inside a stage that spends most of its 0.16 seconds building and loading the formula.
• Output: puzzle-solution/07_sat_proof.txt.

25.14 The answer it returned

• 121 = 11 x 11, so lay it out as a square:

. . . . . . . * . * .
* . . . . * . . . . .
. . . . . . . * . * .
* . * . . . . . . . .
. . . . * . * . . . .
. . * . . . . . * . .
. . . . * . . . . . *
. * . . . . * . . . .
. . . * . . . . . . *
. . . . . * . . * . .
. * . * . . . . . . .

• Exactly two in every row, exactly two in every column, two in each of the eleven regions from section 24, and no two touching, not even diagonally.

---

26. Solving it a second time, differently

• Two independent confirmations are worth more than one careful one.
• Stage P9 solves the same puzzle again with nothing in common with P8.

solutions to the probed constraint set: 1 (that is all of them)
matches the SAT key: True

• Different tool, different encoding, different inputs, same 121 bits.
• The first method never learns what the puzzle is; it searches the recovered netlist directly.
• The second never learns what the netlist is.
• They agree.

---

27. Every string the chip can print: easter egg 9

• Stage P10, and this is the stage that could not be written with a command-line solver.
• My first version of this was guesswork.
• Once the chip was answering correctly I drove it with the four cases I could think of and read O[7:0] on each: nothing, everything, something wrong, and the answer.
• Four messages.
• I wrote that up.
• Then I noticed that what I had was not a measurement of the ROM.
• It was a list of the grids I happened to try, which is a different thing, and nothing said the list was complete.
• So it was replaced with an enumeration.
• Unroll the netlist from reset with all 121 input bits free, take the cone of O[7:0] and success together, and ask the solver to enumerate every value the output bus can take on the first output edge.
• Four come back: (, B, E, T.
• Then, for each of those, enumerate every value the bus can take on the second edge given the first.
• T splits into R and W; the others do not split.
• Two characters separate every message, so when the enumeration returns UNSAT the catalogue is closed and nothing else is reachable.
• Five prefixes, fourteen SAT queries, the last one UNSAT.
• Each prefix hands back the grid that produced it, and all five grids are then simulated in one bit-parallel pass to read the rest of each string.

• The T split is where the fifth message came from.
• One branch is TRY AGAIN.
• The other returns a grid the gates answer with TWO NOT TOUCH, the other name of Star Battle, and the chip prints it only when that exact rule is the one broken.
• To confirm the trigger rather than assume it, z3 was asked for 40 more grids in that class, all 40 driven through the netlist, plus 20 controls that are two per row and two per column and no-touch but wrong on regions:

40 of 40  counts correct and touching     ->  TWO NOT TOUCH,  success = 0
20 of 20  counts correct except regions   ->  TRY AGAIN,      success = 0

• Exact condition: every count right, adjacency wrong.
• It is not reachable by sweeping. 60 random 22-star grids and 60 grids constructed to have two stars in every row and every column all came back TRY AGAIN, because none of them also got the regions right.
• Finding it also meant my recovered RTL was wrong.
• It had four verdicts, and the 540-grid equivalence run had passed only because none of its grids reached the fifth case.
• So the RTL got a fifth verdict, and 24 grids built by z3 to be counts-right-and-touching joined the vector set, which is where the 564 in the next section comes from.
• An equivalence run is only as good as its vectors, and these vectors were extended by a solver result rather than by guesswork.
• Output: puzzle-solution/10_message_catalogue.txt.

---

28. Writing the RTL, and proving it matches the gates

• Both solves confirm the answer.
• Neither confirms that the circuit is understood, and that is what the challenge asks for.
• Stage P11 writes behavioural RTL for the whole chip from scratch, in terms of rows, columns, regions and stars, then proves it equivalent to the gates rather than asserting it.
• The proof is a simulation: iverilog compiles the cell models, the extracted netlist, my RTL and one testbench together, and vvp drives both descriptions from the same reset with the same stimulus, comparing every cycle of success and every cycle of the full output byte.
• Two independent descriptions, two independent simulators, one vector set:

EQUIVALENCE: 0 success mismatches, 0 O mismatches over 564 grids

• The gates are simulated by iverilog, which has never seen my RTL, and the RTL is simulated by iverilog, which has never seen the geometry.
• Outputs: puzzle-solution/08_recovered_rtl.v and puzzle-solution/09_equivalence.txt.

The RTL behind each block

• The nine blocks of section 6, in the same order, with the lines of 08_recovered_rtl.v that implement each one.

1. Scan position counter

localparam N = 11;

reg [3:0] col, row;
reg       done, done_d;

wire running   = enable & ~done;
wire last_col  = (col == N-1);
wire last_cell = last_col & (row == N-1);

if (running) begin
  if (last_col) begin
    col <= 0;
    row <= row + 1'b1;
    if (last_cell) done <= 1'b1;
  end else begin
    col <= col + 1'b1;
  end
end

• This is the only thing that knows where in the frame the chip is.
• col counts 0 to 10 and wraps, row advances on each wrap, and done latches when cell 120 arrives and stops the scan for good.
• Four flops for col, four for row, one for done.
• Nothing here looks at I, so the position and the payload are independent, which is what lets every other block be written as "on a star, at this position, do this".

2. Region decoder

wire [10:0] cell_no = row * N + col;

always @* begin
  region_id = 4'd0;
  case (cell_no)
    11'd0:   region_id = 4'd0;
    11'd1:   region_id = 4'd0;
    ...
    11'd13:  region_id = 4'd5;
    ...
    11'd120: region_id = 4'd4;
  endcase
end

• A 121-entry constant lookup, position to region id, with no state at all.
• It is the largest purely combinational block in the design, 147 cells and zero flops, because synthesis flattens the case into AND and OR gates over the eight counter bits.
• The table it holds is the region map, and that map is the one piece of the design that could not be read out of the gates.
• It came from probing: one star at one position, 121 times, watching which counter incremented.

3. Column star counters

reg [1:0] ccnt [0:N-1];

if (star) begin
  if (ccnt[col] != 2'd3) ccnt[col] <= ccnt[col] + 1'b1;
end

if (ccnt[i] != 2'd2) all_ok = 1'b0;

• Eleven counters of two bits each, 22 flops, one per column, each incremented when a star lands in its column.
• They saturate at 3 instead of wrapping, so a third star sticks at 3 and can never roll back around to a passing 2.
• Two bits is enough because the only question ever asked is whether the final value equals 2, and anything above 2 is equally wrong.

4. Region star counters

reg [1:0] gcnt [0:N-1];

if (star) begin
  if (gcnt[region_id] != 2'd3) gcnt[region_id] <= gcnt[region_id] + 1'b1;
end

if (gcnt[i] != 2'd2) all_ok = 1'b0;

• Identical to the column counters, and the same 22 flops, with one difference: the index is region_id from the decoder rather than col.
• That single change of index is the whole reason the design needs the region decoder, and it is what turns a two-per-row-and-column puzzle into a Star Battle.
• It is also why the first hypothesis failed: 25 grids that were perfect on rows and columns were all rejected here.

5. Row star counter and no-touch checker

reg [1:0]   rowcnt;
reg [N-1:0] prev_row, cur_row;
reg         prev_cell;
reg         adj_err, row_err;

wire above_l = (col > 0)   ? prev_row[col-1] : 1'b0;
wire above_c =               prev_row[col];
wire above_r = (col < N-1) ? prev_row[col+1] : 1'b0;
wire touches = prev_cell | above_l | above_c | above_r;

if (star) begin
  if (rowcnt != 2'd3) rowcnt <= rowcnt + 1'b1;
  cur_row[col] <= 1'b1;
  if (touches) adj_err <= 1'b1;
end
prev_cell <= star;

if (last_col) begin
  if ((rowcnt + (star && rowcnt != 2'd3)) != 2'd2) row_err <= 1'b1;
  rowcnt    <= 0;
  prev_cell <= 0;
  prev_row  <= cur_row | (star << col);
  cur_row   <= 0;
end

• Two jobs share one block because they share the same memory of the recent past.
• There is one row counter rather than eleven.
• Only one row is ever in flight, so rowcnt is checked against 2 at the last column and cleared in the same cycle, which is where the 11 + 11 + 1 arrangement on the die comes from.
• The (rowcnt + star) term in the check exists because the eleventh star of a row arrives on the same edge the row is being judged.
• The no-touch check only ever looks backwards.
• When a star arrives, the four neighbours that have already been seen are the cell to the left and the three above it, so those four are all it needs; the forward neighbours will run the same test themselves when their turn comes.
• prev_cell holds the left one and prev_row holds the row above.
• In the gates this is a single 12-deep shift register of I tapped at positions 1, 10, 11 and 12, which is the same object: 11 cells back is directly above, so 10, 11 and 12 back are the three above and 1 back is the left.
• 16 flops, being 2 for rowcnt, 11 for prev_row, 1 for prev_cell, and the two error flags, which latch and never clear.

6. Total star counter

reg [7:0] total;

if (star) begin
  total <= total + 1'b1;
end

  wire counts_ok = ~row_err & (total == 8'd22) & all_ok;

• Eight bits, not five, because it has to count all the way to 121 without wrapping.
• It is only ever compared for equality, against 22 for the verdict and against 0 and 121 for the two degenerate messages, so no magnitude comparator is built.
• This counter is redundant against the eleven column counters, which already force 22 stars between them, and the chip carries it anyway because the output stage needs to tell an empty grid from a full one.

7. Success logic

reg succ_q;

always @* begin
  all_ok = 1'b1;
  for (i = 0; i < N; i = i + 1) begin
    if (ccnt[i] != 2'd2) all_ok = 1'b0;
    if (gcnt[i] != 2'd2) all_ok = 1'b0;
  end
end

if (done & ~done_d)
  succ_q <= ~adj_err & ~row_err & (total == 8'd22) & all_ok;

assign success = succ_q;

• The 23 inputs to the AND tree are 11 column compares, 11 region compares and the row result, plus the total and the two error flags.
• done & ~done_d is a one-cycle pulse on the edge after the last cell, so the verdict is computed once, on edge 122 and not edge 121, and that is exactly why the SAT solver proved 121 edges unsatisfiable and 122 satisfiable.
• succ_q is written nowhere else, so it holds its value for the rest of time.
• At gate level that shows up as the | (u28.Q & ...) term feeding the flop back into itself.

8. Output stage

wire counts_ok = ~row_err & (total == 8'd22) & all_ok;

always @* begin
  if      (total == 8'd0)             j = 0;
  else if (total == 8'd121)           j = 1;
  else if (counts_ok & ~adj_err)      j = 2;
  else if (counts_ok &  adj_err)      j = 4;
  else                                j = 3;
end

always @(posedge clk or negedge rst_n) begin
  if (!rst_n) begin
    optr <= 0; emitting <= 0; o_q <= 8'h00;
  end else if (done & ~done_d) begin
    emitting <= 1'b1; optr <= 5'd1; o_q <= rom[0];
  end else if (emitting && optr < mlen) begin
    o_q  <= rom[optr];
    optr <= optr + 1'b1;
  end else begin
    o_q <= 8'h00;
  end
end

assign O = o_q;

• The largest block on the die at 225 cells, and the one the provided layout image labels as safe to ignore.
• It is a five-way selector into a small ASCII ROM, clocked out one character per cycle starting on the same edge success settles.
• j picks the message: 0 for EMPTY SKY, 1 for BIG BANG, 2 for (* TWO STARS *), 3 for TRY AGAIN and 4 for TWO NOT TOUCH.
• Index 4 is the one that took a solver to find, because reaching it means getting every count right and breaking only the adjacency rule.
• The 12 flops are the character pointer and the 8-bit output register.
• optr is declared five bits here and the gates only build four of them, since the longest message is 15 characters.

9. Clock tree

always @(posedge clk or negedge rst_n) begin

• Every sequential element in the design is on that one line, and the buffer tree is inserted by synthesis to drive 92 clock pins from a single pad.
• It appears in the extracted netlist as 32 buffers in three levels, one clkbuf_16 at the root and clkbuf_8 then clkbuf_4 below it:

sky130_fd_sc_hd__clkbuf_16 u201_clkbuf_16 (.A(clk), .X(net_660));
sky130_fd_sc_hd__clkbuf_8 u1_clkbuf_8 (.A(net_660), .X(net_505));
sky130_fd_sc_hd__clkbuf_4 u0_clkbuf_4 (.A(net_505), .X(net_000));

• Every one of the 92 clock pins traces back through these buffers to clk with no gating anywhere, which is what makes it safe to reason about the whole chip one rising edge at a time.

---

29. The answer

• Stage P12 and P13. Drive the recovered key in and read O[7:0] cycle by cycle:

edge 122   0x28  '('    success = 1
edge 123   0x2a  '*'
edge 124   0x20  ' '
edge 125   0x54  'T'
edge 126   0x57  'W'
edge 127   0x4f  'O'
edge 128   0x20  ' '
edge 129   0x53  'S'
edge 130   0x54  'T'
edge 131   0x41  'A'
edge 132   0x52  'R'
edge 133   0x53  'S'
edge 134   0x20  ' '
edge 135   0x2a  '*'
edge 136   0x29  ')'

(* TWO STARS *)

• (* ... *) is Verilog attribute syntax and also an OCaml comment.
• Inside it is the rule the 728 gates spend the whole frame checking.
• P13 writes a waveform with success high, which was not provided with the puzzle: puzzle-solution/14_success_inputs.vcd.
• It is shaped deliberately like example_inputs.vcd, same six signals, same timescale, same 10 ns clock, so the two open side by side in Surfer.
• success first goes high at t = 1,255,000 ps, rising edge 126, which is enabled edge 122.

---

30. What the pipeline checks rather than assumes

• Each of these could quietly be wrong, so each is measured on every run rather than argued about once.

• Two places are allowed to move if the SAT back end is swapped, and only two.
• The warm-up has 15 valid answers, so the pair it returns is the solver's choice.
• And each message in the catalogue is illustrated by an example grid that produces it, where any grid in the class would do.
• Neither is a result, and neither changes if the back end does not.

---

31. Making it fast

• The first working version was twenty numbered Python scripts shelling out to yosys and iverilog for every question, and it took about four minutes.
• Almost all of that was process startup and Verilog elaboration, repeated hundreds of times to ask hundreds of nearly identical questions.
• Folding it into one file that keeps its state in memory took it to 17 seconds.
• Everything after that came from measurement rather than from guessing, in two rounds.

• Every one of those changes was checked the same way: run the pipeline, then diff every file in puzzle-solution/ and warmup-solution/ against the previous version.
• Both directories are byte-identical before and after all of it. Nothing below trades a result for a second.

The first round

Not computing something nothing reads.

• Three of the 4.87 seconds in P2 were inside one call: shapely.unary_union, once per conductor layer, merging 10,819 li1 polygons into 5,472 islands and so on up the stack.
• What that call computes is the exact merged outline of the union, with the interior boundaries dissolved.
• Nothing downstream ever reads an outline.
• What the extractor needs is the connected components of the relation "these two polygons touch", plus the ability to ask which component a given point landed in.
• Those components can be had directly: one STRtree per layer, one proximity query per layer over the raw polygons, and union-find over the pairs that come back.
• It gives the identical partition, for a reason worth writing down:

distance(p, A union B)  =  min( distance(p, A), distance(p, B) )

• so merging shapes first and then asking whether something is within 60 nm can never give a different answer from asking about the members directly.
• The transitive closure is the same set either way.
• Measured on puzzle.gds, the two approaches agree island for island on all six layers.

unary_union then stitch     3.08 s
union-find on raw polygons  0.28 s

• Eleven times faster, and it deletes code rather than adding any.

Doing the arithmetic once for everything, instead of once per shape.

• Flattening the hierarchy means applying each placement's rotation, mirror and translation to every polygon in the cell it places.
• That is 31,844 affine transforms on the puzzle, done one shapely call at a time.
• shapely 2.0 can hand back the coordinates of a whole array of geometries as one numpy array, and take them back the same way.
• So: pull every polygon's coordinates out in one call, build one array of per-polygon transform coefficients, apply the whole transform as four multiplies and two adds over the entire array, and put the coordinates back in one call.

one shapely call per polygon     0.54 s
one numpy pass over all of them  0.09 s

• The same idea applies twice more.
• Polygons are built in bulk from concatenated coordinate arrays rather than one Polygon(...) at a time.
• And the interior point used to locate a pin or a via is taken once per cell definition and then moved by the same cheap transform, rather than transforming the polygon at every placement and asking shapely for a fresh interior point each time.
• An affine map sends interior points to interior points, so the two are equivalent, and there are 66 cell definitions and 9,875 placements.

Union-find on integers instead of on tuples.

• The union-find keys were (layer, index) tuples in a dictionary.
• They are now plain integers into one flat list, with a layer offset added in.
• Same algorithm, same path compression, no hashing and no tuple allocation on a loop that runs 120,000 times.
• This one has a visible side effect worth being straight about.
• Net names are assigned by sorting on the union-find root, so changing what a root is renumbered the internal nets.
• The circuit did not change: the two netlists were compared as partitions of pins into nets, with ports attached, and they are identical on both designs, 738 nets and 84 nets, which is the same test section 14 uses to prove the extraction correct in the first place.
• Only the arbitrary net_NNN labels moved.

Encoding once and asking many times.

• The old code built the CNF from scratch for K=121, again for K=122, and a third time for the uniqueness re-solve, then a fourth for the enumeration.
• Now the depth question is one encoding asked twice by assumption plus one blocking clause, so one solver is built where there were three.
• On top of that the encoder folds constants and shares identical gates as it writes:

• Loading a formula into the solver is a per-clause call across the Python boundary, so a formula nine times smaller loaded a third as often is most of the 1.15 s to 0.18 s.

Using the other cores.

• The 564-grid equivalence run was a single vvp process stepping 564 grids of 140 cycles through 728 gates, and it was the largest single item left at 5.5 seconds.
• Compiling with iverilog turned out to be 0.07 s of that, so the fix is not about compilation at all.
• The testbench now reads +shard and +shards and runs only the trials whose number falls in its shard, while still stepping the same random stream, so the trial list is partitioned rather than resampled and every grid is still covered exactly once.
• The pipeline compiles once and launches one vvp per core.
• Determinism survives, deliberately: the shards are collected in shard order rather than completion order, and the shard count itself never appears in the output, so the transcript is identical on a machine with two cores and one with sixteen.

The second round

Asking the spatial index a cheaper question.

• The single largest item left in extraction was one call: STRtree.query(polygons, predicate="dwithin", distance=0.06), 0.27 s on the puzzle.
• Handing the tree a distance predicate makes it decide every candidate pair itself, one exact polygon-to-polygon distance at a time, from inside the traversal.
• Splitting that in two is much cheaper.
• Grow each polygon's bounding box by the tolerance, ask the tree only for the pairs whose grown boxes overlap, which is a pure box test, and then run the exact distance test on the survivors as one vectorised shapely.dwithin call over two arrays.
• The prefilter can only ever return a superset, since two shapes within 60 nm always have bounding boxes within 60 nm, so the exact test decides and the answer cannot change.
• Verified rather than assumed: the two produce the identical edge set, 35,296 pairs, on puzzle.gds.

one tree query with a distance predicate   0.265 s
box prefilter, then one vectorised test    0.075 s

Cardinality is a boolean constraint, not arithmetic.

• The three z3 stages state "exactly two stars in this row" 33 times per solve.
• Written the obvious way, Sum([If(b, 1, 0) for b in row]) == 2, that hands z3 an integer arithmetic problem over 121 indicator variables and makes it carry a theory it does not need.
• AtMost and AtLeast are z3's own cardinality constraints and stay inside the boolean theory, which is where this problem lives.
• Two smaller things in the same loop.
• Blocking a found grid was written as Or([v != bit ...]), which builds 121 disequality nodes; it is now Or([Not(v) if bit else v ...]), a plain clause of literals.
• And reading the model uses m[v] rather than m.evaluate(v), which is a lookup rather than an evaluation call.

All of a cell's pin marks in one shapely call.

• Building the 66 cell definitions cost 0.26 s, and almost all of it was two loops that called shapely once per shape.
• Deciding which li1 polygons a pin label sits on was polygon.buffer(0.005).intersects(point) for every polygon of every labelled pin, which is 4,934 buffer constructions and 4,934 predicate calls.
• It is now one STRtree per cell definition and one proximity query per cell, with the hits sorted back into the original order so the numbering downstream is unchanged.
• Taking the interior point of each pin rectangle was representative_point() once per rectangle.
• It is now one shapely.point_on_surface call over the whole array, which is the same function vectorised.

per-cell definition work   0.26 s  ->  0.03 s

• The merged LEF is 5 MB and was being parsed once per extraction, so twice per run.
• It is parsed once now.

Shards, not hyperthreads.

• nproc reports 16 on this machine and the shard count was taken from it, but the machine has 8 physical cores.
• The equivalence simulation is one interpreter loop per shard and gains nothing from a sibling thread on the same core, so the extra eight processes were pure contention.

• Linux publishes the sibling map under /sys/devices/system/cpu/*/topology, so the shard count comes from that where it exists and falls back to the logical count everywhere else.

The third round

• The second round left extraction dominated by two Python loops that walked hit tables one entry at a time.

The cut lookup.

• Every via and every pin mark used to come back from locate in a dictionary keyed by a (key, layer) tuple, which the caller then read back one dict.get at a time.
• That is about 50,000 tuple constructions to build the dictionary and 50,000 more to take it apart, for a question whose answer is one integer per mark.
• It now returns a single integer array parallel to the marks, minus one where a mark landed on nothing, and the caller groups it with bincount and unique.

A cut that landed on conductor number zero was being dropped.

• The filter was [c for c in found if c], and 0 is a real conductor index, so the first li1 polygon in the array was invisible to every cut that landed on it.
• That is what cut mcon 17182/17188 in the old log was: not six floating vias, six that the filter threw away. The warm-up lost twenty the same way.
• All six were redundant, joining nets that other paths already joined, so the partition is identical either way, which is why nothing downstream ever caught it.
• The log now reads 17188/17188, which is what this document already claimed.

Net numbering is now a function of the geometry.

• A component is rooted at its lowest-numbered polygon rather than at whichever node the union order happened to leave on top.
• Net names are assigned by sorting on that root, so this is the difference between a numbering that is stable across code changes and one that is not.
• It renumbered the anonymous nets once. The partition was verified identical net for net, 738 of 738 and 84 of 84, before and after, by comparing each net's set of (instance, pin) connections.
• The union-find rewrite that made this possible was worth nothing measurable, about 0.02 s. It was kept for the stable numbering, not for the clock.

What I tried and did not keep

What I did not do, and why

• Each of the three main results is still cross-checked by a tool that did not produce it:

---

32. Solving it in hardware

• Once 08_recovered_rtl.v came out of the gates the chip stopped being unknown: it is an 11 x 11 Star Battle validator with one region map wired into it. The puzzle still has to be solved, and the pipeline does that with a SAT solver in Python.
• Which raises the obvious follow-up. Does the solving half have to be software?
• full-solver/ is the answer. solver.v is told the region map and produces the 121-bit frame. validator.v is the recovered chip. A sequencer between them holds the chip in reset while the search runs, then drives it through exactly the protocol the die already has. Nothing in the loop is software.
• It is deliberately kept to one side. RUN.sh does not touch it, the main pipeline does not depend on it, and deleting the folder changes nothing else in this repository.

How the solver searches

• A Star Battle row holds two stars that cannot touch, so a row is one of the 45 column pairs (a,b) with b >= a+2.
• All 45 are judged in one combinational block, so a clock either descends a level or backs up one. It never merely tries a candidate, and the serial version of the same search would be about 45 times slower.
• The pruning is where the cost actually is:

• The one that matters asks whether a region can still be finished. If region g needs n more stars and has fewer than n cells left in the rows below, the branch is already dead. Two orders of magnitude out of one test.
• Column feasibility is worth four clocks in ten thousand. It is in there because it costs two mask compares, not because it earns its keep.
• It is applied without looping over candidates. A region that needs at least one star from this row is short by one, a region that needs two is short by two, so two mask compares shared by all 45 candidates decide it. Columns use the same trick against the rows remaining.
• Sharpening availability to exclude the cells the row above already blocks would reach 6,941 clocks, at the price of eleven population counts per candidate. That is not a trade worth making here.

Clock by clock, all three designs

• The warm-up's 8 and the puzzle's 122 are both minimum depths, proved by the same SAT pass returning UNSAT one edge shorter.
• The full-solver's 10,370 is 244 + x, where x is whatever the search costs. The 244 is fixed: two 121-cell frames, one handover clock and one verdict clock. Only x depends on the puzzle, and an easier region map solves in a few hundred.

Does it work

edge 121      region map loaded, 121 cells
edge 10247    solved, x = 10126 clocks (1 to set up, 10125 to search)
edge 10370    success high, O reads "(* TWO STARS *)"

• The frame the solver builds is bit for bit the 121-bit key that SAT pulled out of the netlist, and the chip prints (* TWO STARS *).
• The testbench never sees the answer. It knows the region map, and it checks the frame that comes back against the rules of Star Battle itself: two per row, two per column, two per region, nothing touching.
• validator.v is 08_recovered_rtl.v split into the seven blocks it is made of, one per rule. The split is only worth anything if it changed nothing, so it is run against the gate netlist over the same 564 grids the main pipeline uses:

grids compared         564
success mismatches     0
O[7:0] mismatches      0

Running it

bash full-solver/run.sh                # the pipeline, then the equivalence proof
bash full-solver/run.sh --only pipe    # just the pipeline, which is what writes the VCD

• Only iverilog is needed for the pipeline. The equivalence run also reads puzzle-solution/02_extracted_netlist.v and 03_cell_models.v, so bash RUN.sh at the top has to have run once.
• The transcript is in full-solver/run.log and the waveform in full-solver/full_solver.vcd.

---

33. Easter eggs, collected

Note :

• In Easter Egg (3), I ran a sample RTL to see how iverilog produces a normal VCD file :

  iverilog -g2012 -o sim.out counter.v tb_counter.v vvp sim.out less counter.vcd # or: cat counter.vcd

• To which is comes up as :

$date
	Tue Aug 18 04:49:16 2026
$end
$version
	Icarus Verilog
$end
$timescale
	1ps
$end

• you can see it prints the name of the tool and not a human message.

---

Note :

• A perfect number is a positive whole number that equals the sum of its positive proper divisors, leaving out the number itself;

  496 (1 + 2 + 4 + 8 + 16 + 31 + 62 + 124 + 248)

Note* :

• A total of 9 Easter Eggs = number of positive proper divisors of 496 (PLEASE TAKE THIS AS A JOKE)

*Revision : The above statement was true till I found the 11th Easter Egg :(

---

34. Directory layout

├── CHALLENGE.md         # The main challenge 
├── RUN.log              # The complete run log
├── RUN.sh               # Main Orchestrating bash
├── README.md            # This file
├── requirements.txt     # Python dependencies 
├── GDS-to-RTL           # Reverse Recovery scripts
├── General-GDS-to-RTL   # The same extractor, for any sky130 GDS you have
├── puzzle               # Provided Puzzle files
├── warmup               # Provided warmup files
├── puzzle-solution      # Puzzle solution files
├── warmup-solution      # warmup solution files
├── full-solver          # An RTL solver that drives the recovered chip, kept separate
├── TwoNotTouch-Interactive-Puzzle    # Interactive Two Not Touch Puzzle, browser and desktop (TRY THIS!)
├── Easter-Eggs          # List of easter eggs
├── Images               # Images of waveforms, layouts, schematics
├── pdk                  # SKY130 PDK
└── Personal-Notes       # Ignore this

---

35. Files the run produces

---