RU version is available. Content is displayed in original English for accuracy.
Advertisement
Advertisement
⚡ Community Insights
Discussion Sentiment
77% Positive
Analyzed from 1632 words in the discussion.
Trending Topics
#https#more#solution#solve#jane#used#street#com#challenge#problem

Discussion (46 Comments)Read Original on HackerNews
just for info: https://en.wikipedia.org/wiki/GDSII will tell you about the GDS format. It apparently stands for Graphic Data System II (originally developed by Calma in the late 1970s).
[1] https://www.degate.org/
[2] https://github.com/DegateCommunity/Degate
Now if he is presenting his tools as a good way to solve this problem, something you should use, or any such - that would be a bad thing. Good tools for this are complex and need to be done as part of a large team. If good tools that others should use is the goal then he should join some other group making those tools. I'm sure there is an existing open source project (maybe KiCAD - I'm not in this space so that is the only name I can come up with but maybe their goals are different?) that does this and would welcome more help.
This resonates so much. I had a similar feeling after going to my very first operations research lecture. Solving seemingly incomprehensibly complex problems by framing them as a bunch of simple constraints and getting a solution seemed like such magic.
Let me help you: work on figuring out how to spend the millions of dollars every year Jane Street will pay you to clock in. I've heard private aviation is expensive, for example. :)
At least by the looks of it, Jane Street appears to be an odd one to genuinely value competence.
Also, yosys has support for doing “assertion checking”, which I used in my solution: https://sunaabh.com/systems/2026/08/18/jspuzzle.html
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...
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.
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 in detail what my solution looked like, though I intend to write some follow up posts that are a bit more in the weeds of the solution. And frankly, the code I used is pretty ugly but it got the job done.
This is my first blog post, so if you have any feedback please let me know. All the writing, all the code was done by me, by hand, in vim.
[0] https://blog.janestreet.com/can-you-reverse-engineer-an-asic...
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 think journey is the goal and yours was certainly more educational :)
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.
As for what to do next, I used to spend way too much of my late-2000s time on puzzle hunts (particularly the Melbourne Uni one [1]) and this tickled the same part of my brain. Unfortunately they're no longer a thing, but it definitely sounds like you'd enjoy something similar.
[1]: https://www.puzzles.wiki/wiki/MUMS_Puzzle_Hunt
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.
So that was the missing part for me! I did it from scratch (with custom Python script with gdstk and shapely) (the GDS file does have the cells annotated, so not a big problem but still). I was thinking about scripting the "trace net" tool in klayout but decided that's going to probably bring its own can of worms...
I'd like to do a full writeup but haven't had the time.
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!
(Or did they close yesterday?)
https://blog.janestreet.com/can-you-reverse-engineer-an-asic...
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.
What did you expect?
I recently solved a (in)famously hard challenge (disobey conference hacker ticket) more or less by accident. I say by accident because I have always ignored this challenges as they generally require a lot of patience and motivation to solve. Some years they haven't been solved at all. This year I had a GPT sub with some unused quota so I thought let's see how far it gets.
And it crunched through the whole thing in an evening and morning (occasional poking from me to keep going and steer it right).
Like anon, I learned nothing except that the agents have become really good at solving puzzles. Last time I had thrown a puzzle on them was Advent of code, with GPT3 I think and it struggled so much I gave up my experiment on day 7 or something.
>Personally, I did not learn that much from that experience
Fire is hot, water is wet, etc
These GDS design files have a lot more structure to them.
But, they do have a hardware division, and Jane Street has a podcast that talks about some of the things they do https://signalsandthreads.com/?tag=hardware