Jane Street ASIC Puzzle
Jane Street recently announced a hardware puzzle. I came across it on hackernews, and was intrigued enough to take a look and spend a significant amount of time on it after work this week.
I work in hardware, so you can imagine how interesting I must have found this to continue staring at VS code after 8 hours of it in the office.
The puzzle involves reverse engineering an ASIC, starting from a GDS and figuring out:
- What the design does
- What the success condition is
The latter is the main part of the puzzle: finding what sequence of inputs causes a success output signal to go high. Immediately, it is clear that there is only one input bit, 8 output bits, a clock, reset and the success signal. We are almost certainly dealing with a serial input, which means we’ve definitely got some state machines in there along with all the combinational logic.
Now I was really intrigued. Time to dig in to this.
GDS and KLayout
Now is the time to admit that I had only superficially seen a GDS file before, and certainly never stared too close at one. In their challenge GitHub, Jane Street suggests viewing the schematic, so this is what I did. After spending some time being confused about what all the layers mean, I found this incredibly useful resource which lists the SKY130 standard layer used for each encoding, e.g., layer 69/20 is met2 (metal layer 2).
I also discovered that KLayout has a Python API, which was great news. Step 1 then, was extracting a netlist from the GDS.
The API made this somewhat easy. Each routing layer (local interconnect, metal 1, metal 2, etc.) can be identified by its unique code, and these explicitly describe the connections between cells. We query the API to extract these connections: first the intra-layer connections (e.g., everything that’s connected via the local interconnect or on one metal layer). Then, we use the contacts/vias, which have their own identifier, to join connected components going up the stack.
What we get at the end of this is a graph of standard cells, and their connectivity — a netlist! The KLayout API has a nice internal representation of the netlist here, which gives us a good string representation of the entire circuit.
Cool! I have to admit, I found this part really interesting, having never looked at a GDS before — I hadn’t realised how much information you can extract from just the layers.
Also, pretty cool to see the Jane Street logo in the corner on metal layer 2 xD
!image.png
Emitting RTL
We now want to turn this netlist into RTL. Before we can do that, we need to actually pull some logic out of these standard cells. Each of them can be reduced to a simple set of gates: AND, OR, NOT, XOR (and their inverses), and a set of flops with associated clock.
We first convert to an internal logic IR representation:
class Expr:
def __init__(self, output, op, inputs):
self.output = output
self.op = op
self.inputs = inputs
def __repr__(self):
return f"{self.output} = {self.op}({', '.join(map(str, self.inputs))})"
I did this originally with the idea of hand-rolling a compiler that would turn this IR into a set of z3 SMT solver predicates. However, I decided to just go with Yosys in the end, so this IR step ended up being somewhat unnecessary. It is fairly simple though, we just go through each net and turn it into an Expr, looking up a table that looks like this: (courtesy of Codex)
"sky130_fd_sc_hd__and2": lambda p: ("X", AND(p["A"], p["B"])),
"sky130_fd_sc_hd__and3": lambda p: ("X", AND(p["A"], p["B"], p["C"])),
"sky130_fd_sc_hd__and4": lambda p: ("X", AND(p["A"], p["B"], p["C"], p["D"])),
"sky130_fd_sc_hd__and2b": lambda p: ("X", AND(NOT(p["A_N"]), p["B"])),
"sky130_fd_sc_hd__and3b": lambda p: ("X", AND(NOT(p["A_N"]), p["B"], p["C"])),
"sky130_fd_sc_hd__and4b": lambda p: ("X", AND(NOT(p["A_N"]), p["B"], p["C"], p["D"])),
"sky130_fd_sc_hd__and4bb": lambda p: ("X", AND(NOT(p["A_N"]), NOT(p["B_N"]), p["C"], p["D"])),
We can then emit actually verilog from this representation! Admittedly, I didn’t feel like doing this part, so I just let Codex do it for me. It does a lot of scaffolding work to set up the ports list, and declare all the wires (if combinational) and regs (if the net is used as the output of a flop), turns DFF expressions into actual verilog flops, and emits the correct syntax for all combinational logic.
It’s not awfully interesting, this part, but by the end of it, I can throw Yosys at puzzle.v and:
sunaabh@JARVIS:~/jspuzzle$ yosys -p "read_verilog puzzle.v; hierarchy -top puzzle; proc; flatten; opt -full; dffunmap; async2sync; stat" yosys -p "read_verilog puzzle.v; hierarchy -top puzzle; proc; flatten; opt -full; dffunmap; async2sync; stat"
/----------------------------------------------------------------------------\
| |
| yosys -- Yosys Open SYnthesis Suite |
| |
| Copyright (C) 2012 - 2020 Claire Xenia Wolf <claire@yosyshq.com> |
| |
| Permission to use, copy, modify, and/or distribute this software for any |
| purpose with or without fee is hereby granted, provided that the above |
| copyright notice and this permission notice appear in all copies. |
| |
| THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES |
| WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF |
| MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR |
| ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES |
| WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN |
| ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF |
| OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. |
| |
\----------------------------------------------------------------------------/
Yosys 0.33 (git sha1 2584903a060)
-- Running command `read_verilog puzzle.v; hierarchy -top puzzle; proc; flatten; opt -full; dffunmap; async2sync; stat' --
1. Executing Verilog-2005 frontend: puzzle.v
...
8. Printing statistics.
=== puzzle ===
Number of wires: 1487
Number of wire bits: 1494
Number of public wires: 705
Number of public wire bits: 712
Number of memories: 0
Number of memory bits: 0
Number of processes: 0
Number of cells: 1441
$and 502
$dff 4
$mux 109
$not 281
$or 411
$sdff 88
$xor 46
End of script. Logfile hash: a313f1cb75, CPU: user 0.15s system 0.02s, MEM: 18.38 MB peak
Yosys 0.33 (git sha1 2584903a060)
Time spent: 32% 4x opt_expr (0 sec), 19% 2x read_verilog (0 sec), ...
It compiles!
Solution
In order to find the success condition, I first started digging around the emitted verilog to see what I could figure out. This was not exactly a fruitful endeavour, as the code is unsurprisingly obfuscated. One thing I did discover though is what looks like a modulo-11 4-bit counter:
always @(posedge n_2213 or negedge rst_n) begin
if (!rst_n) begin
n_832 <= 1'b0;
n_20 <= 1'b0;
n_319 <= 1'b0;
n_380 <= 1'b0;
n_2254 <= 1'b0;
n_2419 <= 1'b0;
end else begin
n_832 <= n_2501;
n_20 <= n_2303;
n_319 <= n_2440;
n_380 <= n_2235;
// These aren't relevant
n_2254 <= n_2396;
n_2419 <= n_2477;
end
end
I know its a counter because the D inputs to this flop look like this:
assign n_2303 = ~((n_934 & n_1526) | n_2374 | n_2164)
assign n_1526 = (~n_319 & ~n_380 & n_832 & n_20);
assign n_2164 = (n_20 & n_319 & n_934);
assign n_2374 = ~((n_319 & n_934) | n_20);
n_2164 is checking whether bits n_20, n_319, n_934 are all set. I’ve noticed n_934 is like a global enable signal that gates everything. Then, we can gather that n_2303 checks if n_20 and n_319 are both high, and goes high if they are. Combined with n_2374 , this gives us n_20 ^ n_319, a toggle on bit 1 of the counter.
n_1526is clearly checking whether bits n_832andn_20 are set, while n_319 and n_380 aren’t. This is the modulo-11 check: we are checking if bits 1 and 3 of the counter are set, and clear the counter if they are.
So we have something that counts to 10! This is what I found in roughly 1 hour of staring at numbers and letters…so this is certainly not a sustainable approach.
I then pivoted to something I had in mind since the start — a SAT solver approach. Yosys has built in support for this. However, we’re still missing something at this point. I know what the success condition is (success = 1'b1 ) of course, but I don’t know when it should happen. It’s clear from the logic that we have some state machines in the design, and so the success condition is likely a function of time as well as the inputs:
Luckily, we can infer quite a bit from the provided example simulation. From this sim, we can see that after enable goes high, we feed in our input bitstream for exactly 121 cycles of clk, before enable is de-asserted again and the output reads: 0x54 0x52 0x59 0x20 0x41 0x47 0x41 0x49 0x4e — TRY AGAIN.
Oh?
The sim then repeats this for a different input bitstream (again over 121 cycles), with the same output. We are dealing with a serial lock.
The great thing about this is it tells us exactly when success needs to go high: 121 cycles after enabled. So this is exactly what I told yosys:
(Glossing over some additional constraints required to make sure the SAT solver doesn’t turn rst_n and enable on and off as it pleases)
# assuming enable goes high on cycle 4, set success to go high 121 cycles later
sat -seq 140 -set-at 125 success 1 -show O -show success
We get the following solution:
124 \O 0 0 00000000
124 \success 0 0 0
---- ----------------------------------------- ----------- --------- -------------
125 \O 40 28 00101000
125 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
126 \O 42 2a 00101010
126 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
127 \O 32 20 00100000
127 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
128 \O 84 54 01010100
128 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
129 \O 87 57 01010111
129 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
130 \O 79 4f 01001111
130 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
131 \O 32 20 00100000
131 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
132 \O 83 53 01010011
132 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
133 \O 84 54 01010100
133 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
134 \O 65 41 01000001
134 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
135 \O 82 52 01010010
135 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
136 \O 83 53 01010011
136 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
137 \O 32 20 00100000
137 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
138 \O 42 2a 00101010
138 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
139 \O 41 29 00101001
139 \success 1 1 1
---- ----------------------------------------- ----------- --------- -------------
140 \O 0 0 00000000
140 \success 0 0 0
This gives:
0x28 → ‘(’
0x2a → ‘*’
0x20 → ‘ ‘
0x54 → ‘T’
…
0x53 → ‘S’
0x20 → ‘ ‘
0x2a → ‘*’
0x29 → ‘)’
Solution: (* TWO STARS *)
This, as I discovered, is how comments are written in Ocaml:
(* This is a comment *)
// This is not a comment
with two stars!
The Input Sequence
I was curious what the input sequence that produced this looks like. We can do this with -show I on the same yosys command.
(Admittedly, I had some help from Codex here in helping me connect the dots)
Taking the first 11 cycles of enable being high:
---- ----------------------------------------- ----------- --------- -------------
3 \I 0 0 0
3 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
4 \I 0 0 0
4 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
5 \I 0 0 0
5 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
6 \I 0 0 0
6 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
7 \I 0 0 0
7 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
8 \I 0 0 0
8 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
9 \I 0 0 0
9 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
10 \I 1 1 1
10 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
11 \I 0 0 0
11 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
12 \I 1 1 1
12 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
13 \I 0 0 0
13 \enable 1 1 1
So, taking the first enable as cycle 0, the input is high on cycle 7 and 9.
The next set of 10:
---- ----------------------------------------- ----------- --------- -------------
14 \I 1 1 1
14 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
15 \I 0 0 0
15 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
16 \I 0 0 0
16 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
17 \I 0 0 0
17 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
18 \I 0 0 0
18 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
19 \I 1 1 1
19 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
20 \I 0 0 0
20 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
21 \I 0 0 0
21 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
22 \I 0 0 0
22 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
23 \I 0 0 0
23 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
24 \I 0 0 0
24 \enable 1 1 1
---- ----------------------------------------- ----------- --------- -------------
I is high on cycles 0 and 5.
This trend continues, with I only being high for 2 cycles out of each set of 11. This harkens back to the modulo-11 counter, it’s not a coincidence that we have 11 sets of 11 = 121 total cycles here — it is kind of begging us to put it on a grid:
. . . . . . . * . * .
* . . . . * . . . . .
. . . . . . . * . * .
* . * . . . . . . . .
. . . . * . * . . . .
. . * . . . . . * . .
. . . . * . . . . . *
. * . . . . * . . . .
. . . * . . . . . . *
. . . . . * . . * . .
. * . * . . . . . . .
It’s a star battle!
Some AI-driven exploration
At this point, I was happy enough to let Codex take a shot at parsing the obfuscated RTL to see what it could discover. There’s some pretty fun easter eggs in there. First, it seems like the TRY AGAIN message comes from a ROM. There are actually 3 more messages in ROMs: EMPTY SKY, BIG BANG, and TWO NOT TOUCH.
This is awesome, these ROMs are basically debugging hints for anyone that tries to brute force the solution. It seems like the logic that picks the output mux select checks the number of “stars” in the input bitstream. If not enough, we get an “empty sky”. If there are too many, we have a “big bang”. If the number is correct (two per row), but they don’t follow the star battle rules, we get “two not touch”, which is a hint that we need to solve the two not touch game!
The actual solution is decidedly not in a ROM but instead ciphertext that needs to be deciphered with a keystream bit, which gets decoded correctly if success goes high and enable is de-asserted. Presumably, this path activates when the input bitstream satisfies the star battle rules.
Conclusion
This was really fun. I love the two-star theming, the solution was very satisfying, and it all just feels incredibly clever. It was also a great learning experience for me, familiarising myself with the (reverse of) the synthesis flow, and confronting the physics of the GDS. Thank you to whoever designed this puzzle!
I aimed NOT to use AI as far as possible to solve this challenge, and for the most part it wasn’t involved in the overall method I used, with the exception of some implementation. However, it’s surprisingly good at parsing obfuscated RTL and deducing the logic being implemented, which led to some super fun discoveries!