This will be a very simplified overview, the actual code is very messy and long.

GDSII -> Netlist

Using the python-gdsii library, you can extract information from the GDS file, including the name of each structure. This lets you find the standard cells fairly easily:

with open(gds_path, "rb") as f:
    lib = gdsii.library.Library.load(f)

# get our top module
top = lib[-1]
module_name = top.name.decode("ascii")

for elem in top:
    # make sure its a structure, not text or a boundary
    if not isinstance(elem, (gdsii.elements.SRef, gdsii.elements.ARef)):
        continue
    sname = elem.struct_name.decode("ascii")
    entry = struct_shapes.get(sname)
    if entry is None:
        continue

    # grab its metadata
    groups, struct_cuts = entry
    if not groups and not struct_cuts:
        continue

    # make sure its a cell
    is_cell = sname.startswith("sky130_fd_sc_hd__")

Note the groups variable: this contains further information about the cell, such as its pin names and locations. We'll take note of these for routing.

To extract the actual nets,

# create an empty grid
grid = defaultdict(list)

# go through every metal rect
for i, (x0, y0, x1, y1) in enumerate(rects):
    # get its layer and current net id
    layer = rect_layer[i]
    node = rect_node[i]

    # go through every cell it intersects
    for bx in range(x0 // GRID, x1 // GRID + 1):
        for by in range(y0 // GRID, y1 // GRID + 1):
            bucket = grid[(layer, bx, by)]
            for j in bucket:
                # if it intersects with another rect on the layer, merge their net ids
                if rects_touch(rects[i], rects[j]):
                    # datastruct for finding the unions of the nets
                    dsu.union(node, rect_node[j])
            bucket.append(i)

By then using our pin names and locations, we can find which net each pin belongs to and which pin is driving it. Now we can trivially create our Verilog netlist!

From here, I did some quality of life steps:

Netlist -> Solution

SAT Solver

My very first idea was to temporally unroll the netlist over a certain number of cycles (so as to get a directed acyclic graph), convert it to CNF (conjugate normal form; basically into a flat product of sums), and put it into a SAT solver. And this idea worked great. Within ~2hrs of starting, I had a solution that passed and submitted it, content with myself. However, after re-reading the blog post, I felt that this wasn't in the spirit of the challenge. I didn't understand the design in any meaningful way (I also still had 6 days before move-in for college and was very bored).

Failed Methods

One approach that could have worked great was using Hardware Analyzer (HAL), and I tried getting it to work, but the plugin I wanted to use (module_identification) didn't support Sky130. I'm sure someone could add support or otherwise use HAL to their advantage, but I decided to stick to what I knew best, python and willpower.

Manual Analysis

In my manual analysis, I looked at each module I had and annotated the pins to what I thought their meaning was. To do this, I tweaked my netlist exporter to accept a json file that provided name mappings for both the modules and the nets. Here is a sample:

{
  "name_mappings": {
    "net_196": "advance",
    "net_245": "ctr_bit2",
    "net_246": "ctr_bit3",
    "net_255": "ctr_bit1",
    ...
    "net_718": "completed_comb",
    "net_472": "all_pos_equal_2",
    "net_530": "dont_shift",
    "net_279": "last_loop"
  },
  "module_name_mappings": {
    "puzzle": "puzzle",
    "group_y00": "group_y00",
    ...
    "group_y07": "pos_2_5_2b_counter",
    "group_y08": "pos_6_7_2b_counter",
    "group_y09": "pos_8_10_2b_counter_and_res"
  },
  "inline_combo_nets": [
    "net_667",
    "net_668",
    "net_447"
  ],
  "buses": {
    "value_code": [
      "net_159",
      "net_190",
      "net_203",
      "net_212"
    ],
    ...
    "position_10_one_count": [
      "net_720",
      "net_723"
    ]
  }
}

One initial observation that is plot-relevant is that the success (or completion, if you failed) signal goes high on the 121st cycle.

Modulo 11 Counters

Here was one of the modules I had to decode (simplified a bit, and with added comments):

// sky130_fd_sc_hd__and4bb_2 inst_804 @ [23.46, 152.32 um]
// equals ten?
assign mod11_counter__net_302 = (~(position[0] | position[2])) & position[3] & position[1];

// sky130_fd_sc_hd__nor2_2 inst_805 @ [25.76, 157.76 um]
// bit 0 value: if == 10: 0, alternate otherwise
assign mod11_counter__net_439 = ~(mod11_counter__net_302 | position[0]);

// sky130_fd_sc_hd__a21oi_2 inst_865 @ [39.56, 152.32 um]
// will bit 1 be 0?
assign mod11_counter__net_443 = ~(position[1] | position[0]);

// sky130_fd_sc_hd__and3_2 inst_797 @ [27.14, 146.88 um]
// bit 1 carry out (if pos[0] == 1, then you *know* it bit 0 carry out this cycle)
assign mod11_counter__net_411 = position[1] & position[0];

// sky130_fd_sc_hd__a211oi_2 inst_864 @ [34.04, 152.32 um]
// bit 1 value, proof is left as exercise to reader
assign mod11_counter__net_435 = ~(mod11_counter__net_302 | mod11_counter__net_443 | mod11_counter__net_411);

// sky130_fd_sc_hd__and4_2 inst_876 @ [27.14, 146.88 um]
// bit 2 carry out
assign mod11_counter__net_432 = position[1] & position[0] & position[2];

// sky130_fd_sc_hd__xor2_2 inst_873 @ [28.98, 141.44 um]
// bit 2 value
assign mod11_counter__net_407 = mod11_counter__net_411 ^ position[2];

// sky130_fd_sc_hd__a41oi_2 inst_874 @ [28.06, 157.76 um]
// bit 3 carry out
assign mod11_counter__net_464 = ~(position[3] | (position[1] & position[0] & position[2]));

// sky130_fd_sc_hd__a221oi_2 inst_800 @ [28.98, 163.20 um]
// bit 3 value
assign mod11_counter__net_473 = ~((mod11_counter__net_432 & position[3]) | mod11_counter__net_464 | mod11_counter__net_302);

always @(posedge clk or negedge rst_n) begin
    position[0] <= mod11_counter__net_439;
    position[1] <= mod11_counter__net_435;
    position[2] <= mod11_counter__net_407;
    position[3] <= mod11_counter__net_473;
end

In fact, I found that there were two of them- the carry out of one of which was the enable signal to the other.

2-bit Saturating Counters

Additionally (ha ha), several of the modules had 2 bit saturating counters (meaning they dont overflow):

// sky130_fd_sc_hd__nor2_2 inst_343 @ [123.74, 233.92 um]
assign sample_one_at_position_4 = ~(pos_2_5_2b_counter__net_648 | pos_2_5_2b_counter__net_656);

// sky130_fd_sc_hd__o21a_2 inst_335 @ [115.92, 228.48 um]
assign position_4_one_count_lsb_next = (sample_one_at_position_4 | position_4_one_count[0]) & pos_2_5_2b_counter__net_651;

// sky130_fd_sc_hd__a21o_2 inst_333 @ [109.94, 233.92 um]
assign position_4_one_count_msb_next = (position_4_one_count[0] & sample_one_at_position_4) | position_4_one_count[1];

// sky130_fd_sc_hd__and2_2 inst_332 @ [113.16, 239.36 um]
// this signal is an output of the module
assign position_4_one_count_is_2 = position_4_one_count[1] & (~position_4_one_count[0]);

always @(posedge clk) begin
    position_4_one_count[0] <= position_4_one_count_lsb_next;
    position_4_one_count[1] <= position_4_one_count_msb_next;
end

Counting them all up, there were 23 in total.

Value Code

After those (relatively) easy modules, I was faced with an issue: I had no clue what the other modules were doing. So I took this opportunity to write a script that would identify likely buses by checking if there are nets that have very similar operations performed on each other. This gave me one group of gates that was helpful (these assignments were spread out across multiple modules):

// sky130_fd_sc_hd__and4bb_2 inst_1444 @ [115.92, 103.36 um]
assign group_y03__net_322 = (~(net_159 | net_212)) & net_203 & net_190;

// sky130_fd_sc_hd__and4b_2 inst_449 @ [115.00, 125.12 um]
assign group_y04__net_359 = (~net_212) & net_203 & net_159 & net_190;

// sky130_fd_sc_hd__and4bb_2 inst_448 @ [115.92, 130.56 um]
assign group_y04__net_374 = (~(net_190 | net_203)) & net_212 & net_159;

// sky130_fd_sc_hd__and4bb_2 inst_439 @ [115.92, 141.44 um]
assign group_y04__net_403 = (~(net_159 | net_203)) & net_212 & net_190;

// sky130_fd_sc_hd__or4b_2 inst_447 @ [124.20, 141.44 um]
assign group_y04__net_391 = (~net_212) | net_203 | net_159 | net_190;

// sky130_fd_sc_hd__nor4_2 inst_1477 @ [120.52, 59.84 um]
assign group_y01__net_215 = ~(net_190 | net_159 | net_212 | net_203);

// sky130_fd_sc_hd__or4b_2 inst_1482 @ [121.90, 59.84 um]
assign group_y01__net_216 = (~net_159) | net_203 | net_212 | net_190;

// sky130_fd_sc_hd__or4b_2 inst_1471 @ [111.32, 70.72 um]
assign group_y02__net_235 = (~net_190) | net_203 | net_212 | net_159;

(and many more...)

You might notice a trend with these- they look a lot like they are encoding something, which is then being decoded! In fact, there are 11 instances in which they are being decoded / checked for equality.

Solution

Now is a good time to take a second and see if you can figure it out. Here are the key findings I had at this point:

Pause to see if you can solve it.

Not yet? Well, me too. I tried some unsuccessful methods to extract the method: investigating the mystery value, trying to understand the output generation, and analyzing my SAT solver solution. I knew the counters would sweep an 11x11 matrix or grid, but had no idea what to do with that. The missing piece came when I looked at what exactly the decoders were being used for - they were enabling/disabling 2b counters. To dig further, I made a quick testbench to probe the mystery value at each cycle, laid out over the grid, and saw this:

6  6  6  6  6  8  8  5  4  4  9
6  6  0  6  6  8  5  5  4  4  9
6  6  0  8  8  8  8  5  5  4  9
6  6  0  8  1  1  1  9  5  5  9
0  6  0  8  1  9  9  9  9  9  9
0  0  0  8  1  1  1  9  2  2  2
8  8  8  8  8  8  1  9  2 10 10
8  7  7  7  1  1  1  9  2 10 10
8  7  7  3  9  9  9  9  2 10 10
8  8  7  3  3  9  9  9  2  2  2
8  7  7  3  9  9  9  9  9  9  9

Now, I had an idea of the challenge. It was to "place" exactly two of something in every row (which requires 1x 2b counter), column (requiring 11x 2b counters), and coded region (requiring 11x 2b counters; for a total of 23). Upon realizing that I checked my SAT solver solution and, sure enough, it met exactly those criteria. Unfortunately I was robbed of the chance of creating that solution myself, but I probably would have used a SAT solver for it anyways.

What I would do differently