ASIC Challenge Writeup
This is my solution for the Jane Street Reverse Engineering an ASIC Challenge
Initial Thoughts
I saw the challenge on the front page of HackerNews, with the headline "Can you reverse engineer an ASIC?" I answered: No, I couldn't; I actually thought this page would teach me about reverse engineering ASICs, so I clicked the page. Realizing it was a challenge, I decided to give it a shot since I was pretty curious about the ecosystem of ASICs, considering I was learning SystemVerilog and FPGAs, and I also find these kinds of things to be fun.
My initial thought was to convert the ASIC design to a netlist then to Verilog, essentially reversing the chip design process. Reading the full challenge document confirmed this.
Process
Exploration
My first step was to explore my options: I cloned the repository, then read the comments on HackerNews, and saw the sky130 pdk mentioned.
The challenge said to see if you could figure out what the chip did. I opened the ASIC design for both the puzzle and the warm-up in klayout; I didn't find it extremely helpful as I couldn't figure out the functionality of the chip from it. However, for the puzzle layout, I did notice that the success = 1 condition was likely confirmed before output generation (challenge description validates this). Given my knowledge (well, a lack of it), I decided to reverse engineer the design without considering the physical layout of the chip.
My plan was to tackle the warm-up first. Knowing the rules, I got Claude's input and help here.
Steps
I converted the design to a netlist using the magic library. I also installed volare and the sky130pdk.
Using magic, I was able to find the top cell in the design (adder_demo) to operate on.
Then, I gave Claude the sky130pdk and told it to extract the cell Verilog from the pdk into its own library.
I converted the netlist into cell-level Verilog. Then, I converted the cell-level into gate-level Verilog by mapping each cell to the equivalent sky130 Verilog (Claude extracted the pdk to Verilog and made a header).
Fortunately, I'm more comfortable with gate-level Verilog —it's more like typical reverse engineering.
Within this, I noticed power connections; they seemed like junk (as it was for the physical hardware), so I set up a script to strip the power connections.
The next step: minimizing the gate-level code. This was done through a yosys pipeline that applied multiple minimization and compression techniques. I figured it was fine to reduce the complexity of the code as I believed —given my experience— the synthesis process had already applied transformations that removed traces of the original source.
I decided to apply inlining: for example, the combination of x=y+1 and c=x+y could be inlined to target c as c=(y+1)+y, removing the variable x.
As the identifiers were long and verbose —a distraction— I wrote a script to rename identifiers, stripping the sky130 prefix in front.
Comparing my Verilog to the original warm-up, I noticed that buses were not added back through the pipeline. The pipeline continues, reconstructing buses originating from a shift register. In the warm-up, you can see the registers a_reg and b_reg; at the end of the pipeline, these same registers existed.
After exploring the final Verilog, I realized that reverse engineering this logic by hand would be hard, if not impossible.
At this point, it dawned on me that boolean logic is a giant system of equations —and I could put it through a massive algebraic solver. After doing my research, I learned that whole field of SAT solving existed. So, I set up the yosys solver and pointed it at the Verilog to see how I could reverse the success output to find the inputs. After constant tweaking (and figuring out how to use the solver), I did finally figure it out.
| # | Stage | Tool | Output File | Lines |
|---|---|---|---|---|
| 0 | list-cells | list_cells.tcl |
none —finds top cell | |
| 1 | extract | gds2spice.tcl |
adder_demo.spice |
523 |
| 2 | convert | spice2v.py |
adder_demo.v |
1,680 |
| 3 | strip-power | strip_power.py |
adder_demo_nopower.v |
1,128 |
| 4 | minimize | yosys | adder_demo_abc.v |
133 |
| 5 | inline | inline_wires.py |
adder_demo_inlined.v |
114 |
| 6 | rename | rename_wires.py |
adder_demo_readable.v |
114 |
| 7 | buses | bus_reconstruct.py |
adder_demo_bus.v |
44 |
| 8 | ports | bus_ports.py |
adder_demo_ports.v |
44 |
| - | SAT | yosys |
Table showing stages, files, and line count for the warmup run
Puzzle
After reverse engineering the warm-up through my constructed pipeline, I decided to throw my hands at the actual puzzle itself.
I ran the pipeline on puzzle.gds. However, my output Verilog was mostly junk —I still saw sky130pdk cells in my final output. This was caused by the sky130 cell library only containing the cells that the warm-up used —I then added the new sky130 cells to the library.
I ran the solver again, giving me workable output. I then ran the SAT solver. Unfortunately, it gave me junk —still, even after changing the constraints and clock cycles across numerous iterations. Due to the weird output, I decided to run a testbench against my output Verilog and the gate-level code from the netlist to diagnose a divergence in the pipeline.
The pipeline had an issue: the sky130 library did not include certain cells, causing them to be erased in the final output. After updating the library again, I reran the divergence check: it now reported that both files were functionally equivalent.
Subsequently, I was confident I could get the SAT solver to work again. The input, I, had a width of a single bit, and i_reg existed as a bus. Therefore, this implied that I was a shift register. This meant that the input for I would be a sequence of bits over clock cycles. From the puzzle description page, I needed to look for an output string. The output, O, was a bus with 8 bits, the same size as an ASCII code point. This also meant that the output was a shift register outputting a character with every clock cycle.
I reprogrammed the SAT solver with the new constraints. Firstly, I wanted to find the minimum number of clock cycles to set success to 1. Through numerous solver runs, I found the minimum to be 124 cycles. Up to this point, O had no output —after, the minimum number of cycles, it would hopefully output characters with each subsequent clock.
To find O, I created a testbench with the sequence of I driving success to 1, passing it to the design. Then I extended all the input by varying amounts to test how long O extended. Once I found it stopped generating, I turned O into ASCII: the secret, (* TWO STARS *), followed by a null terminator at the end. Finally, I verified this solution across the gate-level Verilog. The testbench worked, meaning the secret had been found.
| # | Stage | Tool | Output File | Lines |
|---|---|---|---|---|
| 0 | list-cells | list_cells.tcl |
none —finds top cell | |
| 1 | extract | gds2spice.tcl |
puzzle.spice |
2,994 |
| 2 | convert | spice2v.py |
puzzle.v |
12,236 |
| 3 | strip-power | strip_power.py |
puzzle_nopower.v |
8,464 |
| 4 | minimize | yosys | puzzle_abc.v |
1,893 |
| 5 | inline | inline_wires.py |
puzzle_inlined.v |
968 |
| 6 | rename | rename_wires.py |
puzzle_readable.v |
968 |
| 7 | buses | bus_reconstruct.py |
puzzle_bus.v |
955 |
| 8 | ports | bus_ports.py |
puzzle_ports.v |
934 |
| - | SAT | yosys |
Table showing stages, files, and line count for the puzzle run
Conclusion
Overall, I'm quite happy with my performance. I'm just a high schooler but I do enjoy programming —and I've been doing it for a while. I find hardware design cool: it forces you to think out of the box (compared to my software engineering background), and I do love a good challenge in addition to learning new things. Last summer, I took a class on quantum and classical computing. The classical side included combinational logic (but didn't continue to clocks), and we drew the diagrams and wrote the equations for it. To learn Verilog, after class each night, I would turn the diagrams into the HDL, albeit messy and inefficient as it was gate-level. After the course concluded, I learned clocking. Whilst learning RTL Verilog, I decided to jump to SystemVerilog because it was also an industry standard and the language was more expressive. Currently, I plan to implement a RISCV RV32I CPU on an FPGA board.
Information in this section accurate as of solve time: ~11:15pm, August 9th, SGT
Easter Eggs
I found the Jane Street logo in the puzzle diagram.