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...

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. :)

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...

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.

[1] https://www.degate.org/

[2] https://github.com/DegateCommunity/Degate

Also, yosys has support for doing “assertion checking”, which I used in my solution: https://sunaabh.com/systems/2026/08/18/jspuzzle.html