Notes

A few weeks ago Jane Street released one of their puzzles: a challenge to reverse engineer a chip that they had designed:

We’ve designed an ASIC, and we’re giving you its final mask: all of its metal, routing, and active transistor layers, along with some sample inputs and outputs.

Your job is to reverse engineer it. First, recover a netlist from the layout. Then figure out the circuit’s true purpose. And then comes the puzzle within the puzzle: once you understand what the chip does, use it to tease out the output it’s looking for, and find the string value that’s your final answer

With two weeks before my freshman year of university started and seemingly infinite time after my internship ended, I decided that this would be a pretty fun puzzle to work on.

Turns out, you don’t really need to understand what the chip is actually doing internally to stimulate the expected output from it. In my method, I solve the chip as sort of a black-box, knowing little about the internal functionality of the chip but still recovering the solution with no idea what the chip does to generate it.

The Problem

The hardware people at Jane Street give prospective puzzle-solvers a .gds file to start their reverse engineering process. This .gds file is the last step in the chip design process, the file that you send to your foundry in order to get your chip manufactured.

Jane Street does a good job describing how one obtains this .gds file/the chip design flow on their puzzle website, but in short: chips start off as code in hardware description languages (HDLs), you have a tool that takes the function described in HDL and synthesizes it into a collection of connected logic gates (AND, OR, etc.) called a netlist; this process is akin to a compiler generating machine code. After that, another tool takes those logic gates and then performs a process called place and route, which entails placing those logic gates onto locations on the silicon die to meet certain requirements, and then _routing _those logic gates together through metal. Finally, a .gds file is outputted, which is a description of every polygon/shape needed for your fabricator to actually manufacture your chip with silicon.

Jane Street’s ASIC in a GDS Viewer (https://gds-viewer.tinytapeout.com). In the “exploded” view, you can see each layer of metal shapes that make up the final chip.

Puzzle solvers also get an example input/output sequence to the chip, which looks like this. From this, one can trivially discern what the chip is doing: you feed a 121-bit binary sequence into the chip and hope the “success” signal goes to 1, waiting for a string output which is meant to be your final answer. This means that the main goal of the puzzle is find the ground-truth 121-bit signal , which the chip may have clues about.

Recovering Netlist and Functionality

Before poking around the chip, I needed to get a functional model of the chip that I could simulate and feed inputs/receive outputs from. This meant going backwards in the chip design flow, trying to recover the netlist and connectivity from the .gds and then creating a behavioral piece of HDL code that mirrors the functionality of the chip. Contrary to the what the puzzle website says, this is actually quite a trivial process

not quite big of a problem as it seems…

Netlist

When you open the .gds file in a viewer such as TinyTapeout’s browser-based one you can click around the dense circuit-y regions and find groups of metal layers all starting with the names sky130_fd_sc_hd: these are actually the logic gates that make up the chip. Sky130 is Skywater’s 130nm Process Design Kit (PDK), a process design kit being a foundry’s standardized specification on how metal layers/transistors must be drawn and how those shapes behave electrically. So every sky130_fd_sc_hd__* in that file is a pre-designed logic gate.

sky130_fd_sc_hd__mux2_1, for example, is a 2 input multiplexer: a circuit that outputs either A0 or A1 (either of the two inputs) on X given the selection signal sent on S.

With this, we have the knowledge of all the logic/electrical cells that exist on the chip. The next step is to figure out the connectivity between each cell that exists. For this, we reference the PDK again:

Sky130’s metal stack description (https://vlsida.github.io/chip-tutorials/sky130.html)

The metal stack explains which layers conduct and which vias bridge them. Knowing this, we can use an open-source tool called KLayout to compute unions which polygons are overlapping on those layers. I had Claude write me a quick script that took the .gds file and the metal stack and used KLayout to output a.l2n (layout-to-netlist) file.

Functionality

With an .l2n we know what electrical cells exist and their interconnects, but we have no idea of the functionality. For this, you need to obtain the Liberty (.lib) file from the PDK, which is a list of the electrical cell’s pins, direction (input or output), and the boolean function that each output computes along with timing, power, and area information. You can obtain this file using ciel, an open-source PDK version manager.

I had Claude write me a small script to strip the Liberty file to a JSON table of the cells, each of their pins, and their functions (rejecting all the unnecessary information about timing and such) and then another to join that table against the .l2n and get a Verilog file that describes the functionality of the chip.

During this process, I also stripped the netlist of every electrical cell that wasn’t a logic cell, doing this by removing cells who’s only connections are VPWR/VGND/VPB/VNB/etc meaning that they can’t carry a signal and thereby can’t be logic. Out of the 9,875 cell instances in the layout, 8,221 were routing vias and another 880 were well taps and decoupling capacitors for the chip’s power delivery.

verilog generated by klayout

Solving the Chip

My first instinct was to go backwards from the success output and see what drove or modified that signal since the goal of the chip was to feed a bitstream that drove that signal to high. The main issue was that the Verilog, while able to be simulated and functionally correct, tells a human nothing obvious about the logic flow within the chip.

For this, I would need a tool that would let me trace the path from an input to an output or any two given pins. Thinking back to my Data Structures course, I saw that you could treat the netlist as a directed graph and do something like a recursive depth-first search (DFS) to find the path a bit would take from input to output and what pins it would encounter throughout. I outlined this idea to Claude, and it wrote me a script to take the Verilog file and output certain information about a given net. The main ones for solving were a cone and fanout command which let me know what computed a certain net or what a certain net affected downstream.

An example of using cone on the success output pin

When I used the script on the success signal, I got this huge multi-layered cone of multiple logic cells each of which had their own trees that fed into them. This was, again, too much to decipher by hand, so I went back to Claude and asked it to flatten that whole tree into one large expression that represented the end state of the cone through recursive substitution.

If you notice, the expression that determines success is a huge conjunction of ANDs, with a OR at the end. This pattern lets us know that success is checking if a certain state is achieved within the chip: an AND needs all of it’s inputs to be 1 to have an output of 1, meaning that the polarity of each part of the expression is it’s required bit value. We also can understand that there is only a single satisfying assignment that makes success go to one, making this a good candidate for a Satisfiability (SAT) Solver

(SAT) Solving the Chip

Note: from a hindsight perspective, I could have directly jumped to tasking a SAT solver to figure out the input sequence that setssuccess to high without doing the path tracing from input/output.

SAT solving Verilog files is quite straightforward. Yosys is an open source tool that has a sat command letting you unroll a design that takes N clock cycles into one huge Boolean formula. You can set any signal to high or low at any timestep and solve for the input bits that would get you to that state at that time.

The solver’s constraints came from the example_inputs.vcd file provided by Jane Street. In that file, signals reset were held low for two cycles (falling edge of the clk signal) and then set to high and enable set to high 1 cycle following reset to high and then held for 121 cycles then dropped.

This translated to this command:

sat -seq 128
    -set rst_n 1  
    -set-at 1 rst_n 0  -set-at 2 rst_n 0 -set-at 3 rst_n 0
    -set enable 1
    -set-at 1 enable 0  -set-at 2 enable 0  -set-at 3 enable 0 -set-at 4 enable 0
    -set-at 126 enable 0  -set-at 127 enable 0  -set-at 128 enable 0
    -set-at 128 success 1
    -show I -max 1

the -set parameter applies to every timestep of the solver, while the -set-at parameter overrides it at individual ones. -show only shows the single variable that we care about, which is is I’s bitsequence.

The output of the SAT solver, showing what the first few bits of I needs to be at every step in order to success to be 1 at the end

Verifying the solution

Once we have the bitstream that the solver yielded, we need to verify that success actually goes to high when the sequence is fed into the chip, and the solver isn’t just finding a shortcut somewhere. Another open source tool, Icarus Verilog, allows me to take the Verilog file generated by Klayout and another Verilog file from the Sky130 PDK that has the Verilog functionality for each electrical cell and actually simulate the chip’s functionality.

Feeding the bitstream and functionally simulating the chip yields success going to high and the solution

(* TWO STARS *)

The waveform dump after simulating the bitstream being fed into the chip

Note: you can actually solve the chip through the SAT solver itself. If you run the solver for a large amount of steps, the solver will actually solve for what the outputs would be after success is 1 for a long time. For example, running the solver for 150 steps:

00101000 = “(“, 00101010 = “*”, 00100000 = “ “, 01010100 = “T”, and so on

Solves for the the output onO after success goes to high. Converting the 8 bit binary values onO to text, you get the same answer “(* TWO STARS *)” as finding the bitstream and simulating the chip with it fed in:

Discussion

I mentioned at the start that you can treat the chip as a pseudo-black box and solve it without knowing its true functionality. This is because you don’t actually need to know what the chip does in order to break it and coax out the desired string from the chip. Even after solving, I still have no idea exactly what the chip’s internal mechanism is to raise success to high once the ground-truth bitstream is fed into it.

The problem initially seems quite open-ended and complicated; “reverse engineering” anything sounds quite intricate, much less reverse engineering a chip only given it’s metal layers. After some analysis, one realizes it’s akin to an algebra equation: given a function (the circuit) and a target output, find an input that produces it, which makes it much easier to approach.

Solving it this way is also much easier and takes a lot less effort. It’s quite a tedious task for an individual/solver to take the Boolean expressions of the logic gates and infer patterns that match a functionality structure that they recognize. I sidestep all the work that this entails by just solving for the target output directly without bothering with the internal functionality.

Overall, this was actually quite an enjoyable puzzle to solve/work through, and it really helped me grow as a hardware designer. I’ve never done anything related to physical design, and only worked with writing RTL for more low-latency applications. I got a nice insight in the ASIC design flow and what the steps are going from HDL to manufacturable silicon. I also got to use tools like KLayout and Yosys, which are tools that I’ve never worked with before. All in all, a great learning experience!