Degate is even a bit overkill, it is meant for when you only have images of the physical chip. This challenge has the full GDS files, which are the files that are sent to the fab for manufacturing. They still contain information about all of the separate layers. In this case they even contained the stdcell names, making even full transistor and logic function extraction unnecessary.

A lot of places claim they want to hire extremely smart autists, and some do. But these types of employees are incredibly hard to manage. Imagine herding cats. So if you don't invest a lot of effort in building an environment to let this person cook, go down the right rabbit holes and not rub others the wrong way, a person like this is a huge liability to the org.

Google says "Jane Street has global office locations in New York, London, Hong Kong, Singapore, Amsterdam, and Chicago" so if you're really at a loss where to spend your money, I would recommend searching for yacht dealerships in those cities. I'm sure it won't be a problem anymore.

oh boy here we go again

Since this was for fun, and the goal was learning at least as much as solving the problem that is just fine. More people should get NIH for those purposes.

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.

I first thought you were teasing Jane Street instead of OP. Maybe shows that OP is a good culture fit for Jane Street :)

No spoilers! But thanks I did find out after I published, I just thought it was funnier not to know while I was working on it

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?

> 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 think journey is the goal and yours was certainly more educational :)

I really enjoyed the writing, cheers. And yes, you may have done it the hard way, but you probably learnt 10x more by doing that.

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

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.

z3 is also just so thoroughly optimized that even if your formulation of the constraints is inefficient it is faster. it is a great library that lets you solve pretty complicated DP problems with a few dozen lines of code.

Z3 is an SMT solver, not a SAT solver. You'd probably be looking for something more like Yices, Bitwuzla, cvc5, etc.

> Personally, I did not learn that much from that experience.

What did you expect?

The fact that agents can solve these is telling and the Infosec Capture The Flag community is trying to figure out how to approach.

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.

>I have used Codex (Sol 5.6 or whatever) to solve this problem.

>Personally, I did not learn that much from that experience

Fire is hot, water is wet, etc

> Submissions close on September 4th, 2026.

https://blog.janestreet.com/can-you-reverse-engineer-an-asic...

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

This would need good image recognition, but maybe not so far out of the realm of possibility.

These GDS design files have a lot more structure to them.

Probably this is just an unfamiliar domain for most non-hardware folks, so it's a nice challenge that might introduce Jane Street to some people they might want to interview for non-hardware roles.

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