Reconstructing a Jane Street ASIC from GDS geometry and solving it with z3
- Sources: primary, discussion
- Summary: The author recovers a netlist from roughly 17,000 polygons by testing layer adjacency and polygon overlap, then lifts it to Verilog. The 120-cycle circuit is inverted by expressing the desired final state as z3 constraints rather than searching a 120-bit input space.
- Why it matters: Both halves of the method transfer outside the puzzle, to netlist recovery from layout and to constraint-solving instead of brute-forcing a wide input.