Through Sand and Star · Logica Digitalis

When researching hardware to build my next hacks, I accidentally ran into an interesting puzzle posed by Jane Street. Essentially, they gave us a GDS file and we must reverse engineer it to understand what the circuit does. Technically, we only need to find an input that raises success, but let's solve the more general problem.

First and foremost, let's plan how to solve this.

Intuition

After looking at the layout, we know the design is small. The output generator is likely some kind of scrambler. From what I learned in college years ago, this would likely be implemented with a linear-feedback shift register (LFSR), because XORs are cheap.

If we look at the clusters near success, it is even smaller. The puzzle designer probably did not use a cryptographic function here. If it is not a one-way function, we can use Z3 to solve it. If Z3 cannot handle it, then we need proper reverse engineering, which I am not too worried about.

Symbolic execution has a path-explosion problem. However, if we know the input length, we can unroll the circuit and solve it efficiently.

Essentially, we want to turn GDS back into Boolean gates, throw it into an SMT solver, and hopefully call it a day.

Layout

The first thing we need to do is parse the GDS file. Being a true engineer, the first thing I do is refuse to read their documentation and look for a GDS opener online.

GDS layout

The bottom looks like Morse code. Decode it:

PER ARENAM AD ASTRA

Nice, we got our first Easter egg. Still, we need to turn this into a netlist. In software reverse engineering, we want our binary to have symbols. Without those, looking at a stripped binary is a pain. For hardware, we want the same thing: annotations in the layout instead of solely physical shapes.

Turn it into a netlist

Luckily, the GDS keeps the standard-cell names and pin labels. We know which boxes are NAND gates, flip-flops, and muxes. Public SkyWater models tell us what they do. KLayout can then recover which labeled pins are connected.

So anyway, I vibe-coded the extractor and simulator with Claude using warm up as the validator.

Guess the input size

Openning the VCD file in emacs, the header has

$date
  Sat Dec 31 23:59:60 2016
$end
$version
    Leave no stone unturned! But for this file, consider looking at it in a waveform viewer instead.
$end
$timescale
    1ps
$end

Sat Dec 31 23:59:60 2016 this looks out-of-place. Why do we have 60 as second here? Is this a hint toward something? So I open Google again. It turns out leap second is a thing. TIL.

Anyway, visualizing the waveforms and looking at the edges where enable changes (from C4 to C125 and from C160 to C281), we get two exact 121-cycle periods.

Look at the cycle

This is probably the input length.

Solve it

The way I think about this is circuit has states and transitions. We assign symbolic variables to the states and perform 121 transitions then we would have the final Boolean formula. We find input so that success is true.

So anyway, I prompted LLM to write the script using Z3 to do that and we get the answer input:

0000000101010000100000000000010101010000000000001010000001000001000000100000101000010000000100000010000010010001010000000

We can simulate the circuit with this input and get the answer (* TWO STARS *). Did we reverse engineer it though? No, but the puzzle obviously has something to do with stars, an $11 \times 11$ grid, and “two stars.” Without any additional context, I asked Google:

What are the things that have 11x11 grids and stars, relating to TWO STARS?

and got:

The things you are referring to are Star Battle logic puzzles, which are also widely known as Two Not Touch.

So this is a Star Battle checker, with solution:

The 121-bit input, shown as an 11×11 grid.

It has exactly two stars in every row, column, and hidden region, with no two stars touching.

The hidden regions are eleven irregular shapes that tile the board — the part Z3 has to recover later. Colored in, the solution above lands two stars in each:

What is the circuit doing?

Now we trace backward from success. The 92 registers turn into a much smaller set of things:

two mod-11 counters for the column and row;
an 8-bit total-star counter that must equal 22;
a per-row counter that must equal two at the end of every row;
eleven counters indexed by column;
eleven counters indexed by a hidden region map;
a 12-bit shift register used for adjacency checks.

The shift register is read at delays 1, 10, 11, and 12. On an 11-wide grid, those are left, up-right, up, and up-left. If any of them is set when a new star arrives, the adjacency-error flag latches.

The region map is easy to recover once we know what to ask. Feed a grid with one 1, see which region counter moves, and repeat for all 121 cells. Solving the recovered Star Battle board gives the same grid as Z3.

Hunting Easter eggs

So far we have PER ARENAM AD ASTRA and the leap second easter egg. Are there more?

Let's solve for potential output strings. Since we already have our Z3 pipeline, we can constrain the verdict state, run the output generator, and ask whether any other state is reachable.

We get five messages:

Message	Trigger
(* TWO STARS *)	the unique solution
TWO"NOT TOUCH	all counts pass, but two stars touch
EMPTY SKY	all zeros
TRY AGAIN	generic failure
BIG BANG	all ones

Until this point, most of our results came from probing, Z3, simulation, and guessing from observable inputs and outputs. A program that behaves like a Star Battle checker could still have hidden states, just like malware or backdoors. Dynamic analysis alone cannot cover this. We need static analysis—if only there were a decompiler like Ghidra or IDA for hardware.

In the old days, my blog would end here. However, with LLMs, building a prototype is now cheap.

Concept of a tool

Before building the tool, we must know what we want to build.

The whole circuit is a big blob of Boolean logic. Humans cannot comprehend that. An LLM, having a bigger context, can do a better job for a bigger small board. But can we compress the circuit into a denser representation: pseudocode with structural recovery?

So we want to know what are LFSR, counters, registers, ... The decompiler output must be readable as well: lift expressions to if, for, or fold repetitive information/constants.

If we vibe code this, we want to use open source designs as the test sets. We also have Z3, which is useful for validation. The metrics we care about could be as simple as line counts, or simply LLM-as-judge.

So, after a few prompts, we have a prototype compiler that works, at least on small-scale designs:

Introduce GREW - Slop hardware decompiler

Let's look at the decompiler output.

ctr0 and ctr1 are mod-11 counter: this is the grid size
We also have a bunch of cap-3 counter: they are star count rules
All the long wires are look-up tables that we neither want nor need to read
Our initial lsfr assumption is indeed correct: look at all the XORs!

module puzzle (
    input I,
    input clk,
    input enable,
    input rst_n,
    output [7:0] O,
    output success);
  // ---------------- recovered state ----------
  reg [3:0] ctr0;        // mod-11 counter
  reg [3:0] ctr1;        // mod-11 counter
  reg [7:0] lfsr0;       // 4 transition rules, 256 reachable values
  reg [11:0] sh0;        // shift register
  reg [7:0] acc0;        // accumulator
  reg [3:0] sat0;        // saturating counter, cap 15
  reg [1:0] sat1;        // saturating counter, cap 3
  reg [1:0] sat2;        // saturating counter, cap 3
  reg [1:0] sat3;        // saturating counter, cap 3
  reg [1:0] sat4;        // saturating counter, cap 3
  reg [1:0] sat5;        // saturating counter, cap 3
  reg [1:0] sat6;        // saturating counter, cap 3
  reg [1:0] sat7;        // saturating counter, cap 3
  reg [1:0] sat8;        // saturating counter, cap 3
  reg [1:0] sat9;        // saturating counter, cap 3
  reg [1:0] sat10;       // saturating counter, cap 3
  reg [1:0] sat11;       // saturating counter, cap 3
  reg [1:0] sat12;       // saturating counter, cap 3
  reg [1:0] arr0 [0:10]; // saturating counters, cap 3
  reg flag0, r0, success_q, flag1, flag2, flag3;
  // success requires !flag0   (proved)
  // success requires !flag2   (proved)
  // success requires !flag3   (proved)
  // O[0]..O[7] (all 8) requires flag0   (proved)
  // success requires flag1   (proved)
  // sh0 is read at delays [1, 10, 11, 12]; ctr0 advances with it, counts mod 11

  // ---- shared subexpressions
  wire t6 = ctr1 in {7, 13};
  wire t14 = !(ctr1[0] & ctr1[2]) & !((ctr1[0] ^ ctr1[2]) & ctr1[3]) & !(ctr1[1] ^ ctr1[3]);
  wire t15 = !((!(ctr0[3] & (ctr1[0] ^ ctr1[2] ^ ctr1[3] ^ (ctr1[2] & ctr1[1]))) & ctr1 not in {6, 15}) | t14 | ctr1 in {9, 12} | t6);
  wire t18 = !((ctr1 in {0:1, 8:9} | ((ctr1[0] ^ ctr1[2]) & ctr1[1])) ^ ctr0[2] ^ (ctr0[1] & (ctr1[0] ^ ctr1[1])));
  wire t22 = (ctr0[1] & (ctr1[0] ^ ctr1[1]) & !((ctr1 in {0:1, 8:9} | ((ctr1[0] ^ ctr1[2]) & ctr1[1])) ^ ctr0[2])) | (t18 & ctr1[0] & ctr0[0] & (ctr0[1] ^ ctr1[0] ^ ctr1[1]));
  wire t24 = !ctr0[2] | ctr1 in {0:1, 8:9} | ((ctr1[0] ^ ctr1[2]) & ctr1[1]);
  wire t26 = t24 & ctr1 not in {3, 11};
  wire t27 = (t22 & ((ctr1[0] ^ ctr1[2] ^ ctr1[3] ^ (ctr1[2] & ctr1[1]) ^ ctr0[3]) | !t24 | !(ctr1 not in {3, 11}))) | (!t26 & (ctr1[0] ^ ctr1[2] ^ ctr1[3] ^ (ctr1[2] & ctr1[1]) ^ ctr0[3]));
  wire t28 = (!(ctr0[3] & (ctr1[0] ^ ctr1[2] ^ ctr1[3] ^ (ctr1[2] & ctr1[1]))) & ctr1 not in {6, 15} & (t14 | ctr1 in {9, 12} | t6)) | t15;
  wire t29 = t15 | (t27 & !t28);
  wire t30 = ctr1 == 12 | (ctr1 in {4:6, 9:12} & t29);
  wire t32 = !(ctr1 >= 13 | (!(ctr1 not in [7:13]) & t30 & !(ctr1 == 13)));
  wire t33 = ctr1 in {4:6, 9:11} ^ t29;
  wire t34 = !(t27 ^ t28);
  wire t35 = (ctr1 in {0:1, 8:9} | ((ctr1[0] ^ ctr1[2]) & ctr1[1])) ^ ctr0[2] ^ (ctr0[1] & (ctr1[0] ^ ctr1[1])) ^ (!(ctr1[0] & ctr0[0]) | !(ctr0[1] ^ ctr1[0] ^ ctr1[1]));
  wire t36 = !t35;
  wire t37 = (ctr1[0] & ctr0[0]) | (ctr0[1] ^ ctr1[0] ^ ctr1[1]);
  wire t38 = t22 ^ ctr1[0] ^ t26 ^ ctr1[2] ^ ctr1[3] ^ (ctr1[2] & ctr1[1]) ^ ctr0[3];
  wire t39 = !t38;
  wire t41 = t36 & t37 & t39 & !(ctr1[0] ^ ctr0[0]) & (!(ctr1[0] & ctr0[0]) | !(ctr0[1] ^ ctr1[0] ^ ctr1[1]));
  wire t43 = !(ctr1[0] & ctr0[0]) & (ctr1[0] | ctr0[0]) & (ctr0[1] ^ ctr1[0] ^ ctr1[1]);
  wire t44 = t37 & (!(ctr1[0] & ctr0[0]) | !(ctr0[1] ^ ctr1[0] ^ ctr1[1]));
  wire t45 = !((ctr1[0] ^ ctr0[0]) | t44);
  wire t46 = !(t36 & t45);
  wire t47 = !(t46 & t39);
  wire t48 = !(t36 | t45);
  wire t49 = t37 | !(ctr1[0] | ctr0[0]);
  wire t50 = !t49;
  wire t51 = !(t36 | t50);
  wire t52 = t45 | t35;
  wire t53 = !t52;
  wire t54 = !((t51 | t53 | t39) & t34);
  wire t55 = t39 | t45;
  wire t56 = t37 & !(ctr1[0] ^ ctr0[0]) & (!(ctr1[0] & ctr0[0]) | !(ctr0[1] ^ ctr1[0] ^ ctr1[1]));
  wire t57 = !t36 | (ctr1[0] ^ ctr0[0]);
  wire t58 = !(t37 & t18 & (!(ctr1[0] & ctr0[0]) | !(ctr0[1] ^ ctr1[0] ^ ctr1[1])));
  wire t59 = t30 ^ ctr1 not in [7:12];
  wire t60 = !t59;
  wire t61 = (t33 ? (t34 ? t56 | (t57 & t58 & t38) : t55 & (t43 | t47)) : (t34 | t41 | !(t36 | t43 | t39 | t45)) & (!(t47 | t48) | t54)) | t60;
  wire t62 = !(t50 & t18);
  wire t63 = !(t43 & t18);
  wire t64 = !(t63 | t38);
  wire t65 = !(t58 | t38);
  wire t66 = t59 | (!(t34 | (t33 & (t62 | t39) & !t64)) & (t33 | t65)) | (t34 & (!(t33 | t43 | t38 | t45 | t35) | !(t46 | t39)));
  wire t67 = (t43 | t45 | t35) & t38;
  wire t68 = !t33;
  wire t69 = t60 | !((t33 | ((t54 | !(t38 | t48)) & (!(t36 | t43 | (t37 & t39 & !(ctr1[0] ^ ctr0[0]) & (!(ctr1[0] & ctr0[0]) | !(ctr0[1] ^ ctr1[0] ^ ctr1[1]))) | t45) | t34 | t41))) & (t51 | t34 | t43 | t67 | t68 | t45));
  wire t70 = t66 & t32 & t69;
  wire t71 = !(t44 | t38 | t35);
  wire t72 = t44 | t35;
  wire t73 = !(t39 | t48);
  wire t74 = !t72;
  wire t75 = !((t33 | (t34 ? (t52 & t39) | (t46 & t73) : t71 | ((t50 | t38) & t72))) & t60 & ((t34 & t72) | t68 | ((t56 | t74) ? t39 : t73)));
  wire t76 = t57 & t39 & t49;
  wire t77 = (t33 & (!(t34 | (t62 & t39) | t67) | (t34 & t64))) | t60 | (!((t76 | t73) & t34) & ((t34 & t37 & t18 & (!(ctr1[0] & ctr0[0]) | !(ctr0[1] ^ ctr1[0] ^ ctr1[1]))) | t76 | t73) & t68);
  wire t78 = t75 & t32 & t77;
  wire t79 = t44 | t39 | t35;
  wire t80 = !((t38 & t48) | t34);
  wire t81 = (((((t57 & t58) | t38) & t79) | t34) & (t51 | !(t34 & (t53 | t38))) & t68) | t59 | (t33 & ((t34 & t47 & t79) | (t80 & ((ctr1[0] ^ ctr0[0]) | t44 | t39 | t35) & (t56 | t38 | t74))));
  wire t82 = ((t34 | t41 | !(t39 | t63)) & !((t38 ? t51 | t43 | t45 : t36 | t43 | t45) & t34) & t68) | (t33 & (!t34 | ((t43 | t38 | t35) & t63)) & (!t80 | (t36 & t55))) | t60;
  wire t83 = !(t34 & t47);
  wire t84 = t59 | ((t83 | t73) & (t34 | t71 | t65) & t68) | !((t83 & (t34 | t73 | ((t43 | t35) & t39 & t63))) | t68);
  wire t85 = t32 & t82 & t84;
  wire t87 = t32 & t61 & t81;
  wire t88 = !t87;
  wire t93 = acc0 == 121;
  wire t94 = acc0 == 0;
  wire t95 = !((!success_q & r0) | t93 | t94);
  wire t96 = !success_q & !t93 & !t94 & r0;
  wire t97 = !(t95 | t96);
  wire t100 = !((!t93 & (success_q | r0)) | t94);
  wire t101 = !(t95 | t100);
  wire t106 = !(t96 | t100);
  wire t107 = t95 & t106;
  wire t108 = !(t95 | (t96 & t100));
  wire t109 = t107 | t108;
  wire t110 = !t109;
  wire t111 = !(t95 | t96 | t100);
  wire t120 = !((sat0 not in [8:11] & float0 & sat0 not in [4:7]) | sat0 in {0:2, 4:6});

  always @(posedge clk or negedge rst_n)
  if (!rst_n) begin <reset> end
  else begin
    if (enable) begin
      if (!flag1) begin
        for (ctr1 = 0; ctr1 <= 10; ctr1++)  for (ctr0 = 0; ctr0 <= 10; ctr0++) begin
          sh0 <- {sh0[10:0], I};
          if (I) begin
            if (t32 & t61 & t81 & t82 & t84) sat1 <- min(sat1 + 1, 3);
            if (t75 & t61 & t81 & t77) sat2 <- min(sat2 + 1, 3);
            if (t66 & t77 & t82) sat4 <- min(sat4 + 1, 3);
            if (!(t87 | t70 | t78 | t85)) sat6 <- min(sat6 + 1, 3);
            if (t66 & t32 & !(t87 | t85) & t69 & t77) sat8 <- min(sat8 + 1, 3);
            if (t66 & t32 & t69 & t82 & !(t87 | t78)) sat9 <- min(sat9 + 1, 3);
            if (t75 & !(t87 | t70) & t77 & t82 & t84) sat11 <- min(sat11 + 1, 3);
            arr0[ctr0] <- min(arr0[ctr0] + 1, 3);
            if ((ctr0 != 0 & sh0[11]) | (sh0[9] & ctr0 != 10) | (sh0[0] & ctr0 != 0) | sh0[10])
              flag2 <- 1;
          end
          if (ctr0 == 10 & (sat5[1] ? sat5[0] | I : !(sat5[0] & I))) flag3 <- 1;
        end
      end
      if (ctr0 == 10 & ctr1 == 10) flag1 <- 1;
    end
    acc0 <- acc0 + (enable & !flag1 & I);
    if (!flag0) sat0 <- 0;
    else sat0 <- min(sat0 + 1, 15);
    if (ctr0 == 10 & enable) sat5 <- 0;
    else if (ctr0 != 10 & enable & !flag1 & I) sat5 <- min(sat5 + 1, 3);
    if ((sat0 == 15 & flag1) | (flag1 & !flag0) | (!enable & !flag0) | (sat0 == 15 & !enable))
      lfsr0 <- lfsr0;
    else if ((flag0 & !sat0[0] & flag1) | (flag0 & !enable & !sat0[3]) | (flag0 & !enable & !sat0[2]) | (flag0 & !sat0[1] & !enable) | (flag0 & !sat0[3] & flag1) | (flag0 & !sat0[1] & flag1) | (flag0 & !sat0[2] & flag1) | (flag0 & !enable & !sat0[0]))
      lfsr0 <- {lfsr0[1] ^ lfsr0[3] ^ lfsr0[5] ^ lfsr0[7], lfsr0[2] ^ lfsr0[4] ^ lfsr0[5], lfsr0[0] ^ lfsr0[1] ^ lfsr0[4] ^ lfsr0[5], lfsr0[2] ^ lfsr0[5] ^ lfsr0[6] ^ lfsr0[7], lfsr0[0] ^ lfsr0[3] ^ lfsr0[4] ^ lfsr0[6], lfsr0[1] ^ lfsr0[2] ^ lfsr0[3] ^ lfsr0[4], lfsr0[0] ^ lfsr0[3] ^ lfsr0[5] ^ lfsr0[6] ^ lfsr0[7], lfsr0[1] ^ lfsr0[2] ^ lfsr0[7]};
    else if (!I & enable & !flag1)
      lfsr0 <- {lfsr0[2], lfsr0[1] ^ lfsr0[3] ^ lfsr0[5] ^ lfsr0[7], lfsr0[3], lfsr0[0], lfsr0[1], lfsr0[5], lfsr0[4], lfsr0[6]};
    else
      lfsr0 <- {lfsr0[2], !(lfsr0[1] ^ lfsr0[3] ^ lfsr0[5] ^ lfsr0[7]), lfsr0[3], lfsr0[0], lfsr0[1], lfsr0[5], lfsr0[4], lfsr0[6]};

    if (enable & !flag1 & I & !t70 & !t78 & !t88 & !t85) sat3 <- min(sat3 + 1, 3);
    if (enable & !flag1 & I & !t87 & !t78 & !t85 & t70) sat7 <- min(sat7 + 1, 3);
    if (enable & !flag1 & I & !t87 & !t70 & t78 & !t85) sat10 <- min(sat10 + 1, 3);
    if (enable & !flag1 & I & t85 & !t87 & !t70 & !t78) sat12 <- min(sat12 + 1, 3);
    if (flag1) begin
      flag0 <- 1;
      if (!flag0) begin
        r0 <- sat1 == 2 & sat2 == 2 & sat3 == 2 & sat4 == 2 & sat6 == 2 & sat7 == 2 & sat8 == 2 & sat9 == 2 & sat10 == 2 & sat11 == 2 & sat12 == 2 & acc0 == 22 & flag2 & !flag3 & all(arr0 == 2);
        success_q <- sat1 == 2 & sat2 == 2 & sat3 == 2 & sat4 == 2 & sat6 == 2 & sat7 == 2 & sat8 == 2 & sat9 == 2 & sat10 == 2 & sat11 == 2 & sat12 == 2 & acc0 == 22 & !flag2 & !flag3 & all(arr0 == 2);
      end
    end
  end

  assign O[0] = flag0 & ((t97 & !sat0[3] & ((sat0[0] & !sat0[1]) | sat0 in {7, 15} | sat0 in {2, 10}) & t100) | (t101 & !(sat0 not in [9:11] & sat0 not in {1:2, 5}) & t96) | t110 | (!((sat0[0] & !sat0[1] & (sat0[2] | sat0[3])) | sat0 in {2:3, 10:15}) & t111) | (t95 & t106 & (lfsr0[6] ^ ((sat0 in {0:9, 12:13} & sat0 not in {6, 14}) | (!sat0[0] & sat0[3]))))) & (sat0 in {2, 4:7} | t107 | t108) & sat0 != 15;
  assign O[1] = flag0 & (sat0 in {1, 5} | sat0 == 8 | t107 | t108) & ((t101 & ((sat0 not in [8:11] & float0 & sat0 not in [4:7]) | (sat0[0] & !sat0[2]) | sat0 in {0:2, 4:6}) & (sat0 in {1:2, 9:10} | t120 | sat0 in {4:5, 12:13}) & t96) | t110 | (sat0[2] & sat0[1] & !sat0[3] & t111) | (t95 & t106 & !((sat0[2] | sat0[1]) ^ lfsr0[0] ^ (!(sat0[0] | sat0[1]) | sat0 <= 3 | (!sat0[0] & sat0[3])))) | (t97 & (sat0 in {7, 15} | !sat0[0]) & !sat0[3] & t100)) & sat0 != 15;
  assign O[2] = flag0 & (sat0 == 5 | t107 | t108 | sat0 in {0, 8}) & sat0 != 15 & ((t101 & !(sat0[0] & sat0[1]) & sat0 <= 11 & t96) | t110 | (t97 & sat0[1] & !sat0[3] & (sat0[2] | !sat0[0]) & t100) | (t95 & t106 & (lfsr0[4] ^ (sat0 not in {8:9, 11:12} & sat0 in {0:1, 6:14}))) | (sat0 <= 3 & t111 & (sat0[0] | !sat0[1])));
  assign O[3] = flag0 & ((t97 & t100 & sat0 in {1, 6}) | ((!(sat0[2] | (sat0[0] & sat0[3])) | !((sat0[0] & !sat0[1]) | sat0[3])) & t111 & (sat0[0] | !sat0[1]) & sat0 in {1, 4:15}) | ((lfsr0[1] ^ ((sat0 in {6, 14} | !(sat0[2] | (!(sat0[0] & sat0[1]) & (sat0[0] | sat0[1]))) | sat0 in {0:6, 15}) & sat0 in {0:2, 5:14})) & t95 & t106) | t110 | (t101 & !((sat0[1] | ((sat0[2] | !sat0[0]) & (sat0[0] | !sat0[2]))) ^ sat0 in {1:2, 5}) & t96)) & (sat0 == 7 | sat0 == 8 | sat0 == 2 | t107 | t108) & sat0 != 15;
  assign O[4] = flag0 & ((sat0 >= 2 & t111 & !(sat0[0] & (sat0[2] | sat0[3])) & sat0 <= 9) | (t95 & t106 & ((sat0 in {0:9, 12:13} & (sat0[2] | (sat0[1] & !sat0[0]) | (!sat0[0] & sat0[3]))) ^ lfsr0[3])) | t110 | (t101 & (!(t120 | (sat0[1] & (sat0[0] | !sat0[2])) | sat0 in {4:5, 12:13}) | sat0 in {8, 10}) & t96)) & (sat0 <= 2 | t107 | t108) & sat0 != 15;
  assign O[5] = flag0 & ((sat0 == 5 & ((!success_q & r0) | t93 | t94) & (success_q | t93 | t94 | !r0) & ((!t93 & (success_q | r0)) | t94)) | (t101 & t96 & sat0 in {3, 7}) | t110 | (t95 & t106 & !(((sat0 not in {2, 7:14} | ((sat0[2] | sat0[1]) & !sat0[0] & sat0[3])) & (sat0[1] | !sat0[0])) ^ lfsr0[5])) | (sat0 == 3 & ((!success_q & r0) | t93 | t94) & (success_q | t93 | t94 | !r0) & (t93 | !(success_q | r0)) & acc0 != 0)) & sat0 != 15 & (sat0 == 3 | t107 | t108);
  assign O[6] = flag0 & (sat0 == 7 | sat0 == 8 | t107 | t108 | sat0 in {0:2, 4:6}) & (((sat0[1] | !(sat0[0] & (sat0[2] | sat0[3]))) & t111 & sat0 <= 9) | (t101 & t96 & sat0 not in {3, 7} & sat0 <= 12) | t110 | (t95 & t106 & !(((sat0[2] & (sat0[1] | !sat0[0])) | sat0 in {1, 3}) ^ lfsr0[2])) | (t97 & sat0 in {0:2, 4:7} & t100)) & sat0 != 15;
  assign O[7] = flag0 & t109 & !(lfsr0[7] ^ (sat0 in [4:6] | ((!(sat0[2] | sat0[1]) | (sat0[0] & sat0[1])) & (!sat0[0] | sat0[3])))) & t95 & t106 & sat0 != 15;
  assign success = success_q;
endmodule

  // ---------------- legend ----------------
  // ctr0[3:0] = {dfrtp#39, dfrtp#38, dfrtp#41, dfrtp#40} (msb..lsb)
  // ctr1[3:0] = {dfrtp#66, dfrtp#67, dfrtp#69, dfrtp#68} (msb..lsb)
  // lfsr0[7:0] = {dfstp#4, dfstp#3, dfstp#2, dfstp#1, dfrtp#36, dfrtp#35, dfrtp#34, dfrtp#33} (msb..lsb)
  // sh0[11:0] = {dfrtp#46, dfrtp#48, dfrtp#51, dfrtp#50, dfrtp#54, dfrtp#42, dfrtp#49, dfrtp#44, dfrtp#52, dfrtp#45, dfrtp#53, dfrtp#43} (msb..lsb)
  // arr0[0:10] : 2-bit saturating
  // sat0[3:0] = {dfxtp#4, dfxtp#1, dfxtp#3, dfxtp#2} (msb..lsb)
  // sat1[1:0] = {dfrtp#25, dfrtp#28} (msb..lsb)
  // sat2[1:0] = {dfrtp#26, dfrtp#29} (msb..lsb)
  // sat3[1:0] = {dfrtp#32, dfrtp#30} (msb..lsb)
  // sat4[1:0] = {dfrtp#74, dfrtp#31} (msb..lsb)
  // sat5[1:0] = {dfrtp#55, dfrtp#57} (msb..lsb)
  // sat6[1:0] = {dfrtp#70, dfrtp#84} (msb..lsb)
  // sat7[1:0] = {dfrtp#71, dfrtp#77} (msb..lsb)
  // sat8[1:0] = {dfrtp#72, dfrtp#79} (msb..lsb)
  // sat9[1:0] = {dfrtp#73, dfrtp#78} (msb..lsb)
  // sat10[1:0] = {dfrtp#81, dfrtp#75} (msb..lsb)
  // sat11[1:0] = {dfrtp#80, dfrtp#76} (msb..lsb)
  // sat12[1:0] = {dfrtp#82, dfrtp#83} (msb..lsb)
  // acc0[7:0] = {dfrtp#62, dfrtp#65, dfrtp#63, dfrtp#64, dfrtp#58, dfrtp#59, dfrtp#60, dfrtp#61} (msb..lsb)
  // flag0    = dfrtp#1
  // r0       = dfrtp#2
  // success_q = dfrtp#3
  // flag1    = dfrtp#37
  // flag2    = dfrtp#47
  // flag3    = dfrtp#56
  // arr0 is indexed directly by ctr0:

We can slice it out, or throw the whole text, into LLM and ask it to explain it for us. This requires no agent and we can actually audit their outputs.

Full output from Gemini with this context alone

Based on a detailed analysis of the Verilog code, this module is a hardware validator for a grid-based logic puzzle known as Star Battle (also known as "Two Not Touch").

Here is the complete reverse engineering of what the module is doing and what each variable represents.

1. High-Level Overview: What is this?

The module takes a serial bitstream (I) representing an 11x11 grid (121 bits total), evaluated one cell per clock cycle in a left-to-right, top-to-bottom fashion. The goal of a Star Battle puzzle is to place exactly two stars (represented by 1s) in every:

Row
Column
Region (The board is divided into 11 uniquely shaped regions)

Furthermore, the "Two Not Touch" rule dictates that no two stars may touch each other, not even diagonally.

If you feed the module the correct 121-bit solution, the success output goes high, and the module decrypts and prints out a 16-character string (likely a CTF flag) on the output O.

2. What are the Flags?

flag1: End of Input Flag. Triggered when ctr1 == 10 and ctr0 == 10 (the 121st and final cell of the grid). It transitions the hardware from the "reading inputs" state to the "evaluating/outputting" state.
flag0: Output Phase Flag. It is set to 1 one clock cycle after flag1. It turns on the output character generator, allowing sat0 to count from 0 to 15 to spit out the 16-byte message on O.
flag2: Adjacency Violation Flag. It is set to 1 if any two stars are touching.
flag3: Row Violation Flag. It is set to 1 at the end of any row if that row does not contain exactly two stars.

3. What are the other variables?

Grid Navigation:

ctr0 and ctr1: These are modulo-11 counters representing the X (column) and Y (row) coordinates of the 11x11 grid currently being scanned.
sh0: A 12-bit shift register that remembers the last 12 bits (cells) inputted. It is used exclusively to check the "no touching" rule. When a 1 is inputted, it checks sh0[0] (left neighbor), sh0[9] (top-right neighbor), sh0[10] (top neighbor), and sh0[11] (top-left neighbor). If any are 1, it trips flag2.

The Star Counters (Saturating Counters):

acc0: Counts the total number of stars on the board. The winning condition expects exactly 22.
sat5: Counts the number of stars in the current row. It resets to 0 at the start of a new row. Used to evaluate flag3.
arr0[0:10]: An array of 11 counters keeping track of the number of stars in each of the 11 columns. The winning condition requires all(arr0 == 2).
sat1, sat2, sat3, sat4, sat6, sat7, sat8, sat9, sat10, sat11, sat12: Notice how there are exactly 11 of these? These count the number of stars in the 11 irregularly shaped regions of the board. The massive block of combinational logic (t6 through t88) simply defines the geometric borders of these regions based on the current ctr1 and ctr0 coordinates.

Winning States and Outputs:

success_q (and success): The ultimate win flag. True if all region counters = 2, total stars = 22, all column counters = 2, and no violations occurred (!flag2 and !flag3).
r0: A "Near-Miss" flag. It becomes true if you got all the math/counts perfectly correct, but you broke the rules by letting stars touch (flag2 & !flag3). The hardware likely outputs an alternate "troll" or failure message on O if this is met.
sat0: A 4-bit counter (0 to 15) used during the output generation phase to sequence the 16 characters of the final text string output O[7:0].
lfsr0: An 8-bit Linear Feedback Shift Register. During the puzzle input, it shifts and scrambles based on your inputs. By the end, its state serves as the "decryption key" for the giant block of assign O[x] = ... logic. Because there is only one valid solution to the Star Battle puzzle, this acts as a hash ensuring you cannot easily extract the final text without actually solving the board.

We didn't find new easter egg here. However, by reading the code, we are sure of it. This assumes our decompiler is not buggy of course.

Only now have we truly understood the logic. We can leverage this to recover the regions for the original puzzle itself (for fun) easily for example. By probing each cell by assigning it with a star, we can look at which region counter increases. Two cells belonging to the same region would increase the same counter.

The puzzle itself

Very nice easter egg: Jane Street Capital.

Conclusion

In the end we solve the puzzle and found multiple easter eggs:

PER ARENAM AD ASTRA - Through the sand to the stars.
Leap second
JSC
Rules of the game and failure messages: BIG BANG, EMPTY SKY, TWO"NOT TOUCH

However, hardware decompilation problem is still there.