To help with such tasks for real chips (given the good quality images) there is Degate[1][2] open source software.
Solving the Jane Street reverse engineering challenge
21–30 of 89 posts
Re: Solving the Jane Street reverse engineering challenge
#22Hi HN, I recently solved the Jane Street reverse engineering challenge [0], and I wrote a blog post on how I reached the answer. It's a moderately technical and (hopefully) entertaining run through of the process. I hope you enjoy reading it as much as I enjoyed doing the challenge (though, as you'll read, it was also quite a frustrating process). My github is on the post if you were interested in seeing a bit more i…
> It turns out that this ‘sky130’ thing is like a … standard? Or something for making chips. Very cool seeing someone completely naive going into this :) If you want to read more about a bit more... cheaty way to do this, I have written about using formal verification machinery to straight up force the solution out of the netlist here: https://atx.name/electronics/asic-re/ . Could be a bit of an infohazard, but I thi…
I'll definitely be reading this thankyou! I think this would have been a much better way to approach it, it's a bit of a joke in the piece that I always do things the hard way, but it's a genuine mystery to me why I operate this way.
I should add I have an EE degree (but have never worked as an EE), so even though I don't know industry standards like this sky130 thing, it's not completely foreign to me.
Re: Solving the Jane Street reverse engineering challenge
#23I wonder how far a LLM could get with this. It will be cool when we get to the point where you can decap a chip, take a picture, and then an LLM can create an emulator for that chip.
I'd say they could solve it much faster than I could. Some of the other commenters are mentioning tools that would have made this so much easier, and I'd assume an LLM would know to use them
Re: Solving the Jane Street reverse engineering challenge
#24Nice! I ended up using the KLayout Python API to parse the GDS and extract the netlist, which was actually quite nice to use.
Also, yosys has support for doing “assertion checking”, which I used in my solution: https://sunaabh.com/systems/2026/08/18/jspuzzle.html
Re: Solving the Jane Street reverse engineering challenge
#25Hi HN, I recently solved the Jane Street reverse engineering challenge [0], and I wrote a blog post on how I reached the answer. It's a moderately technical and (hopefully) entertaining run through of the process. I hope you enjoy reading it as much as I enjoyed doing the challenge (though, as you'll read, it was also quite a frustrating process). My github is on the post if you were interested in seeing a bit more i…
> It turns out that this ‘sky130’ thing is like a … standard? Or something for making chips. Very cool seeing someone completely naive going into this :) If you want to read more about a bit more... cheaty way to do this, I have written about using formal verification machinery to straight up force the solution out of the netlist here: https://atx.name/electronics/asic-re/ . Could be a bit of an infohazard, but I thi…
Nice solution and good easter egg find!
Re: Solving the Jane Street reverse engineering challenge
#26Hi HN, I recently solved the Jane Street reverse engineering challenge [0], and I wrote a blog post on how I reached the answer. It's a moderately technical and (hopefully) entertaining run through of the process. I hope you enjoy reading it as much as I enjoyed doing the challenge (though, as you'll read, it was also quite a frustrating process). My github is on the post if you were interested in seeing a bit more i…
Incredible amount of determination, but you really did make it hard for yourself! You can install librelane to get the whole open silicon tool suite and the sky130 PDK. Circuit extraction can be done with magic. Going from a spice netlist to verilog netlist is pretty mechanical and not a hard transform to write. You almost immediately have something that can be simulated and a good baseline for further reversing.
> Incredible amount of determination
That's very kind of you. At some point I had put so much of myself in to it that I was in too deep and the only was out was to keep digging.
I'll take a look at librelane thanks!
Re: Solving the Jane Street reverse engineering challenge
#27Congrats on solving the challenge! I also briefly wrote about my approach here, with less pictures but going into slightly more detail about how to convert circuits to z3 equations: https://gist.github.com/KarelPeeters/dba417c2690cf0505ac9079...
That's really interesting that you actually used z3 to extract the output from the circuit! It hadn't occurred to me that it would be possible to do that. I suppose I got a little fixated on my approach of running a verilog simulation, and I only used z3 to solve one part (though the hardest part I think). How did you get a $DAYJOB involving formal verification?
Yeah I briefly considered switching to a simulator to get the final output, but then luckily realized the Z3 setup I had was already acting as a super-powered simulator anyway!
I'm not actually using formal verification at $DAYJOB, there we're using MILP solvers (which are closely related to SAT solvers) as part of the compilation flow when scheduling operations onto hardware accelerators.
I have been interested in formal verification for hardware for a while, but so far haven't found an opportunity to apply it. There are some great resources online though: the ZipCpu blog at https://zipcpu.com/formal/formal.html and SymbiYosys website at https://symbiyosys.readthedocs.io/en/latest/. I hindsight I could probably have used SymbiYosys instead of Z3, it would have saved me from having to walk the graph and map the gates to equations myself.
Re: Solving the Jane Street reverse engineering challenge
#28I have used Codex (Sol 5.6 or whatever) to solve this problem. It turns the problem into Z3, then iteratively work through the problems until it figured out the solution. Personally, I did not learn that much from that experience. So I am glad that there's other people working on it as well. I am mostly interested in the techniques used to solve this.
> Personally, I did not learn that much from that experience.
What did you expect?
Re: Solving the Jane Street reverse engineering challenge
#29I'm not sure I've ever seen such a vicious case of NIH-syndrome. Regardless, congrats on the solve!
Re: Solving the Jane Street reverse engineering challenge
#30I love this person!