The right levels of abstraction

Getting to a standardized netlist

Despite knowing this was likely a non-starter, I first tried to follow the circuit at transistor-level for funsies. This was very interesting, but I quickly found myself trying to understand how each gate works from first principles and realized this would be hard to scale. 

Zooming in on the 3D view on GDS viewer felt deeply overwhelming, like I was a rat in New York:

I needed to go at least one level of abstraction up, and luckily Jane Street gave a hint here: the useful intermediate representation was the standard-cell netlist. The chip used the open SkyWater 130 nm library, so the metadata gave information on cell identity and where they were placed. The next step was therefore to recover the metal connections between named cell pins and use this to build a topologically-equivalent logic model.

I basically had all the nodes of the graph (the cells, and their different flavors) and now just had to figure out how they composed. My mental model here was like a cake - I knew the ingredients but needed to figure out how they were put together to get to the final baked good.

Extractor validation

I used gdstk to flatten + read the GDS, then Shapely to join all touching conductors on each routing layer (the via macros connected each of the layers.) The cell pin shapes from the Sky130 PDK attached those anonymous metal components back to their logical ports, and so I was able to see that the final Verilog held 738 logical total instances across 67 cell types (this gave me some hope: 67 is a reasonable number of ingredients). Also, I can't help but worry that 67 isn't coincidental. The interactive diagram below (which I encourage you to play with, it took forever to get right) uses placed pin data for these 728 routed instances.

I'm making this sound like it was easy - it definitely took some experimentation as connectivity errors can sneak in - eg: a complete-looking netlist can still have misplaced vias / an incorrect pin attachment may fail much much later. I used Jane Street’s worked adder (from the Github) as a stress-test: the extractor code had to recover the adder's exact connectivity, then reproduce the A + B = 496 result.

Here's the full interactive netlist and how it maps directly to the geometry. Getting to the netlist was incredibly useful - it represented a pretty clean leap up the abstraction mountain.

Validating the recovered logic

After playing around with the netlist, I was able to extract Boolean models using the Sky130 Liberty details, and simulated the resulting Verilog with Icarus. The supplied example attempts were a useful (second) validation target. Clock for clock, the rebuilt circuit emitted the same TRY AGAIN message.

One sub-network in the output block seemed useless, but JS already flagged this. To double-check, a backward dependency slice showed that this sub-network could not affect the final success, and four-state simulation with the official cell models showed that it could not change the final output. I therefore left it outside the success analysis + recorded it as an extraction limitation, but flagged it for the below easter-egg hunting!

In addition to having the netlist, I could see that the example input contained 121 bits. I give more details on the intuition behind this in the below diagram, but dividing the input into eleven 11-bit rows, noting seven bits per row least-significant-first as ASCII, and treating the remaining four as zero helped decode “The night s” and “ky awaits”. After some Googling, the 11 x 11 structure + night sky reference led me to Star Battle (and Jane Street had posted on it before):

Isolating the success logic

I actually thought about stopping there - "The night sky awaits" seemed like a pretty cool easter egg to get to, but having gotten this far, I knew I needed to actually solve the system using a SAT solver to get to the final string - luckily I'm familiar with these given my other matrix multiplication research.

The full flattened model had 92 flip-flops, but (as Jane Street warned), I found only 79 could influence success. I normalized that meaningful sub-section with Yosys and translated its basic gates into the Z3 SMT solver: 490 ANDs, 341 ORs, 181 NOTs, and 79 state elements. Lastly, I unrolled 121 enabled rising edges followed by the check clock.

Z3 did its thing, and returned a stream of bits satisfying the constraints: to double-check, I blocked that stream and attempted to solve again, getting UNSAT. This proved that the stream was the single unique solution.

I was quite surprised at how quickly the solver found the solution. I'm used to SAT/SMT solvers in the context of the Brent equations for matrix multiplication, and my usual experience is them grinding for days before returning UNSAT. I'm not still entirely sure why this worked so well, but I believe this is due to the wide AND tree / nature of the game. Asking for success = 1 forces every local equality simultaneously: eg: every row, column and region counter must equal two, and every adjacency check needs to remain clear. Because of this, the Z3 solver receives many small constraints rather than one opaque 121-bit search, which helped it wade through the 2^121 total states.

The unique bitstream solution contains two set bits in every row and column, two in each of eleven irregular regions, and no adjacent set bits. These are the rules of a two-star Star Battle, further confirming what I had already guessed above.

Play it for yourself - it's horribly hard:

Verification against the complete netlist

Finally, with great anticipation, I streamed the 121 recovered bits through the complete extracted netlist using the official Sky130 models. After 121 enabled clocks, a low-enable check clock set success to high. The output then produced fifteen bytes.

I do hobbyist fast matrix multiplication research, so am familiar with just how valuable a couple of bytes can be, but DAMN I had to work for these 15 lil numbers.

Here's how it went down: