Python, Verilog, SystemVerilog ★ 0 ⋮ 0
Can you reverse engineer this ASIC?
My write-up on Jane Street's ASIC puzzle. It started with a Reddit comment and ended with a message hidden inside silicon. In between: a lot of staring at rectangles.
The HeadAche of a newcomer
Righteo.
So I'm scrolling through Reddit one day and someone drops try out our puzzle. Open it up. Jane street. Damn.
ASIC? puzzle??? Didn't matter. Read the synopsis, dove straight into the GitHub repo.
First thing I did: open the warmup GDS in KLayout. Obviously I understood nothing from it.
But I tinkered around a little. If you know the KLayout GUI, it hands you:
- layers
- a pile of names down the left side,
sky130_...something (I'd realise later these were the cells) - switches to turn them off and on. Disappear, reappear.
- and things like
how do I get to a coordinatein the GUI. Didn't know that would be useful later. - and then back to GitHub, once I'd had my fill.
Went through netlist.v next, power rails and all, and eventually clocked that the same names were showing up in KLayout's left-hand pane. Which sent me looking. What are cells? Why power rails? What are these layers? I've got an ECE background, mostly FPGA, none in ASIC. So it came easy enough.
One thing kept nagging though. GDS is a BINARY file. Do I take an ML-vision approach to it?
Nope. That wasn't the answer. The whole thing was hinted to be a make our own tools situation, as though the creators were expecting you to make your own EDA tool.
And the answer was sitting in the same post. Klayout. A few chats with an AI agent later and I found out it ships a python API. So, first job: write a python script that understands the GDS file.
Understand what, though? Cells. Which to me were nothing but gates. And gates have inputs and outputs. That's what I wanted. Every gate, every input, every output.
But before any of that, the tinkering paid off. The inter-metal via between metN and met(N+1) is drawn on the same GDS layer number as the LOWER of the two metals, datatype 44. So the met1 <-> met2 via lives on layer 68/44, met1's own number. Not on 69/44.
layers = {
"li1": ly.layer(db.LayerInfo(67, 20)),
"li1_pin": ly.layer(db.LayerInfo(67, 16)),
"mcon": ly.layer(db.LayerInfo(67, 44)), # li1 <-> met1
"li1_text": ly.layer(db.LayerInfo(67, 5)),
"met1": ly.layer(db.LayerInfo(68, 20)),
"met1_pin": ly.layer(db.LayerInfo(68, 16)),
"met1_text": ly.layer(db.LayerInfo(68, 5)),
"via1": ly.layer(db.LayerInfo(68, 44)), # met1 <-> met2
"met2": ly.layer(db.LayerInfo(69, 20)),
"met2_pin": ly.layer(db.LayerInfo(69, 16)),
"met2_text": ly.layer(db.LayerInfo(69, 5)),
"via2": ly.layer(db.LayerInfo(69, 44)), # met2 <-> met3
"met3": ly.layer(db.LayerInfo(70, 20)),
"met3_pin": ly.layer(db.LayerInfo(70, 16)),
"met3_text": ly.layer(db.LayerInfo(70, 5)),
"via3": ly.layer(db.LayerInfo(70, 44)), # met3 <-> met4
"met4": ly.layer(db.LayerInfo(71, 20)),
"met4_pin": ly.layer(db.LayerInfo(71, 16)),
"met4_text": ly.layer(db.LayerInfo(71, 5)),
"via4": ly.layer(db.LayerInfo(71, 44)), # met4 <-> met5
"met5": ly.layer(db.LayerInfo(72, 20)),
"met5_pin": ly.layer(db.LayerInfo(72, 16)),
"met5_text": ly.layer(db.LayerInfo(72, 5)),
}
METALS = ["li1", "met1", "met2", "met3", "met4", "met5"]Metals and vias figured out, connecting the two into a netlist was fine. But was it right?
Well. Fortunately or unfortunately, there is no way around a plain eye-to-screen check of the printed coordinates for every single cell. Manual labour. Rewarding, but manual labour.
After a lot of beating around the bush with Mr. AI, it was done.
Wait. Nah. The input ports? Where are those in the netlist?
I'd conveniently left out the massive clk tree while parsing the netlist for input ports.
So, back to eye-checking. A bit more appear-disappear in KLayout and I noticed every metal sitting on a /20 layer was landing on an input port or was connected to metal coming from the inputs.
But the connectivity? A simple bbox-walk did the trick. Overlap all of those /20 layer metals through the bbox logic, filter out the buffers, and there they were: the input ports and which gates they were connected to.
net_driver_map = {}
port_nets = {} # cluster_id -> port name, for nets that are top-level I/O
for net in top_circ.each_net():
net_name = net.name if net.name else ""
if net_name and not net_name.startswith("net_") and net_name not in POWER_NET_NAMES:
net_driver_map[net.cluster_id] = net_name
port_nets[net.cluster_id] = net_name
for sub in all_subcircuits:
if sub not in sub_to_name:
continue
inst_name = sub_to_name[sub]
for pin in sub.circuit_ref().each_pin():
if pin.name() in OUTPUT_PIN_NAMES:
net = sub.net_for_pin(pin.id())
if net and net.cluster_id not in port_nets:
net_driver_map[net.cluster_id] = f"{inst_name}.{pin.name()}"
def wire_label(net):
if net is None:
return "UNCONNECTED"
name = net.name if net.name else f"net_{net.cluster_id}"
if name in POWER_NET_NAMES:
return name
if str(name).startswith("net_18446"):
return "FLOAT"
return net_driver_map.get(net.cluster_id, f"net_{net.cluster_id}")
PASSTHROUGH_HINTS = ("clkbuf", "buf")
def is_passthrough(cell_type):
lower = cell_type.lower()
return any(h in lower for h in PASSTHROUGH_HINTS)
def resolve_port_connections(net, max_hops=8):
"""Returns a deduped list of (inst_name, pin_name, is_output) for every
REAL (non-filtered) gate pin connected to `net`, hopping transparently
through buffer/clkbuf cells along the way."""
seen_clusters = set()
frontier = [net]
results = []
seen_results = set()
hops = 0
while frontier and hops < max_hops:
hops += 1
next_frontier = []
for n in frontier:
if n.cluster_id in seen_clusters:
continue
seen_clusters.add(n.cluster_id)
for sub in all_subcircuits:
cell_type = sub.circuit_ref().name
for pin in sub.circuit_ref().each_pin():
pn = sub.net_for_pin(pin.id())
if not pn or pn.cluster_id != n.cluster_id:
continue
pin_label = pin.name() if pin.name() else ""
if not pin_label or pin_label in POWER_NET_NAMES:
continue
if sub in sub_to_name:
key = (sub_to_name[sub], pin_label)
if key not in seen_results:
seen_results.add(key)
results.append((sub_to_name[sub], pin_label, pin_label in OUTPUT_PIN_NAMES))
elif is_passthrough(cell_type):
for pin2 in sub.circuit_ref().each_pin():
if pin2.id() == pin.id():
continue
n2 = sub.net_for_pin(pin2.id())
if n2 and n2.cluster_id not in seen_clusters:
next_frontier.append(n2)
frontier = next_frontier
return results
def geometric_trace(port_name):
text_bbox = None
text_layer_for = {"li1": "li1_text", "met1": "met1_text", "met2": "met2_text",
"met3": "met3_text", "met4": "met4_text", "met5": "met5_text"}
for m in METALS:
for shape in top.shapes(layers[text_layer_for[m]]).each():
if shape.is_text() and shape.text_string == port_name:
text_bbox = shape.bbox()
start_layer = m
break
if text_bbox:
break
if not text_bbox:
return None
order = METALS # li1 .. met5, low to high
idx = order.index(start_layer)
frontier = [text_bbox]
def shapes_touching(layer_name, bboxes):
found = []
for s in top.shapes(layers[layer_name]).each():
sb = s.bbox()
for b in bboxes:
if sb.overlaps(b) or sb.contains(b.center()) or b.contains(sb.center()):
found.append(sb)
break
return found
all_path = list(frontier)
# walk down toward li1 (through the vias below the layer the label sits on)
via_below = {"met1": None, "met2": "via1", "met3": "via2", "met4": "via3", "met5": "via4"}
for i in range(idx, 0, -1):
cur = order[i]
below = order[i - 1]
via_name = via_below.get(cur)
if via_name:
frontier = shapes_touching(via_name, frontier)
all_path += frontier
# mcon is the li1<->met1 via, special-cased since it's named differently
if below == "li1" and cur == "met1":
frontier = shapes_touching("mcon", frontier)
all_path += frontier
frontier = shapes_touching(below, frontier)
all_path += frontier
best_name, best_dist = None, float("inf")
for sub in all_subcircuits:
if sub not in sub_to_name:
continue
for pin in sub.circuit_ref().each_pin():
net = sub.net_for_pin(pin.id())
if not net:
continue
for m in METALS:
for shape in l2n.shapes_of_net(net, l[m]):
b = shape.bbox()
for pb in all_path:
if b.overlaps(pb) or b.contains(pb.center()) or pb.contains(b.center()):
dx = max(b.left - text_bbox.center().x, 0, text_bbox.center().x - b.right)
dy = max(b.bottom - text_bbox.center().y, 0, text_bbox.center().y - b.top)
dist = math.sqrt(dx * dx + dy * dy)
if dist < best_dist:
best_dist = dist
best_name = (sub_to_name[sub], pin.name())
return best_nameOnce it worked on 04_final.gds I went straight for puzzle.gds. Sometimes you gotta run before you walk. And the script ran through every gate and input port and printed this, netlist first, then ports:
Netlist extracted from /home/kal-thir/Documents/Reverse_engineer_puzzle/warmup/puzzle.gds
Top cell: puzzle
Instance: U1 (Type: sky130_fd_sc_hd__o21a_2) (181.700, 16.320) um
VGND -> VGND
VPWR -> VPWR
A2 -> U2.X
A1 -> U389.X
B1 -> U646.X
X -> U1.X and so on nearly 706 cells (leaving out buffers of all kings and power cells, tap cells decap)!!*
Port: O[7]
<- U482.X (output drives this port)
Port: rst_n
-> U6.SET_B (input receives this port)
-> U7.SET_B (input receives this port)
-> U8.SET_B (input receives this port)
-> U90.RESET_B (input receives this port)
-> U91.RESET_B (input receives this port)
-> U92.RESET_B (input receives this port)
-> U93.RESET_B (input receives this port)
-> U94.RESET_B (input receives this port)
-> U95.RESET_B (input receives this port)
-> U96.RESET_B (input receives this port)
-> U97.RESET_B (input receives this port)
-> U98.RESET_B (input receives this port)
-> U99.RESET_B (input receives this port)
-> U100.RESET_B (input receives this port)
-> U101.RESET_B (input receives this port)
-> U102.RESET_B (input receives this port)
-> U104.RESET_B (input receives this port)
-> U105.RESET_B (input receives this port)
-> U106.RESET_B (input receives this port)
-> U107.RESET_B (input receives this port)
-> U108.RESET_B (input receives this port)
-> U109.RESET_B (input receives this port)
-> U110.RESET_B (input receives this port)
-> U111.RESET_B (input receives this port)
-> U112.RESET_B (input receives this port)
-> U113.RESET_B (input receives this port)
-> U114.RESET_B (input receives this port)
-> U115.RESET_B (input receives this port)
-> U116.RESET_B (input receives this port)
-> U117.RESET_B (input receives this port)
-> U118.RESET_B (input receives this port)
-> U119.RESET_B (input receives this port)
-> U120.RESET_B (input receives this port)
-> U121.RESET_B (input receives this port)
-> U122.RESET_B (input receives this port)
-> U123.RESET_B (input receives this port)
-> U124.RESET_B (input receives this port)
-> U125.RESET_B (input receives this port)
-> U126.RESET_B (input receives this port)
-> U127.RESET_B (input receives this port)
-> U128.RESET_B (input receives this port)
-> U129.RESET_B (input receives this port)
-> U130.RESET_B (input receives this port)
-> U131.RESET_B (input receives this port)
-> U132.RESET_B (input receives this port)
-> U133.RESET_B (input receives this port)
-> U134.RESET_B (input receives this port)
-> U135.RESET_B (input receives this port)
-> U136.RESET_B (input receives this port)
-> U137.RESET_B (input receives this port)
-> U138.RESET_B (input receives this port)
-> U139.RESET_B (input receives this port)
-> U140.RESET_B (input receives this port)
-> U141.RESET_B (input receives this port)
-> U142.RESET_B (input receives this port)
-> U143.RESET_B (input receives this port)
-> U144.RESET_B (input receives this port)
-> U145.RESET_B (input receives this port)
-> U146.RESET_B (input receives this port)
-> U147.RESET_B (input receives this port)
-> U148.RESET_B (input receives this port)
-> U149.RESET_B (input receives this port)
-> U150.RESET_B (input receives this port)
-> U152.RESET_B (input receives this port)
-> U153.RESET_B (input receives this port)
-> U154.RESET_B (input receives this port)
-> U155.RESET_B (input receives this port)
-> U156.RESET_B (input receives this port)
-> U157.RESET_B (input receives this port)
-> U159.RESET_B (input receives this port)
-> U160.RESET_B (input receives this port)
-> U161.RESET_B (input receives this port)
-> U162.RESET_B (input receives this port)
-> U163.RESET_B (input receives this port)
-> U164.RESET_B (input receives this port)
-> U165.RESET_B (input receives this port)
-> U166.RESET_B (input receives this port)
-> U167.RESET_B (input receives this port)
-> U168.RESET_B (input receives this port)
-> U169.RESET_B (input receives this port)
-> U170.RESET_B (input receives this port)
-> U171.RESET_B (input receives this port)
-> U172.RESET_B (input receives this port)
-> U173.RESET_B (input receives this port)
-> U174.RESET_B (input receives this port)
-> U175.RESET_B (input receives this port)
-> U305.RESET_B (input receives this port)
-> U317.SET_B (input receives this port)
Port: O[6]
<- U466.X (output drives this port)
Port: I
-> U59.A (input receives this port)
-> U60.A (input receives this port)
-> U61.A (input receives this port)
-> U62.A (input receives this port)
-> U63.A (input receives this port)
-> U64.A (input receives this port)
-> U65.A (input receives this port)
-> U66.A (input receives this port)
-> U67.A (input receives this port)
-> U68.A (input receives this port)
-> U69.A (input receives this port)
-> U70.A (input receives this port)
-> U72.A (input receives this port)
-> U73.A1 (input receives this port)
-> U151.A (input receives this port)
-> U283.A1 (input receives this port)
-> U311.A1 (input receives this port)
-> U399.A1 (input receives this port)
-> U402.A1 (input receives this port)
-> U406.A1 (input receives this port)
-> U408.A1 (input receives this port)
-> U409.A1 (input receives this port)
-> U410.A1 (input receives this port)
-> U411.A1 (input receives this port)
-> U412.A1 (input receives this port)
-> U414.A1 (input receives this port)
-> U417.A1 (input receives this port)
-> U420.A1 (input receives this port)
-> U422.A1 (input receives this port)
-> U423.A1 (input receives this port)
-> U425.A1 (input receives this port)
-> U426.A1 (input receives this port)
-> U428.A1 (input receives this port)
-> U460.B (input receives this port)
-> U502.A1 (input receives this port)
-> U600.A (input receives this port)
-> U605.A (input receives this port)
-> U607.A (input receives this port)
-> U610.A (input receives this port)
-> U624.A (input receives this port)
-> U625.A (input receives this port)
-> U626.A (input receives this port)
-> U628.B (input receives this port)
-> U633.A (input receives this port)
-> U648.B (input receives this port)
Port: O[5]
<- U469.X (output drives this port)
Port: O[4]
<- U468.X (output drives this port)
Port: O[3]
<- U467.X (output drives this port)
Port: enable
-> U47.DIODE (input receives this port)
-> U298.B (input receives this port)
Port: O[2]
<- U485.X (output drives this port)
Port: clk
-> U105.CLK (input receives this port)
-> U115.CLK (input receives this port)
-> U122.CLK (input receives this port)
-> U144.CLK (input receives this port)
-> U147.CLK (input receives this port)
-> U153.CLK (input receives this port)
-> U99.CLK (input receives this port)
-> U113.CLK (input receives this port)
-> U136.CLK (input receives this port)
-> U145.CLK (input receives this port)
-> U148.CLK (input receives this port)
-> U305.CLK (input receives this port)
-> U97.CLK (input receives this port)
-> U116.CLK (input receives this port)
-> U124.CLK (input receives this port)
-> U135.CLK (input receives this port)
-> U167.CLK (input receives this port)
-> U172.CLK (input receives this port)
-> U108.CLK (input receives this port)
-> U111.CLK (input receives this port)
-> U121.CLK (input receives this port)
-> U133.CLK (input receives this port)
-> U149.CLK (input receives this port)
-> U157.CLK (input receives this port)
-> U101.CLK (input receives this port)
-> U134.CLK (input receives this port)
-> U137.CLK (input receives this port)
-> U141.CLK (input receives this port)
-> U146.CLK (input receives this port)
-> U96.CLK (input receives this port)
-> U114.CLK (input receives this port)
-> U138.CLK (input receives this port)
-> U150.CLK (input receives this port)
-> U165.CLK (input receives this port)
-> U174.CLK (input receives this port)
-> U3.CLK (input receives this port)
-> U4.CLK (input receives this port)
-> U109.CLK (input receives this port)
-> U155.CLK (input receives this port)
-> U160.CLK (input receives this port)
-> U90.CLK (input receives this port)
-> U117.CLK (input receives this port)
-> U132.CLK (input receives this port)
-> U143.CLK (input receives this port)
-> U152.CLK (input receives this port)
-> U93.CLK (input receives this port)
-> U162.CLK (input receives this port)
-> U163.CLK (input receives this port)
-> U166.CLK (input receives this port)
-> U170.CLK (input receives this port)
-> U171.CLK (input receives this port)
-> U92.CLK (input receives this port)
-> U98.CLK (input receives this port)
-> U106.CLK (input receives this port)
-> U159.CLK (input receives this port)
-> U169.CLK (input receives this port)
-> U175.CLK (input receives this port)
-> U104.CLK (input receives this port)
-> U107.CLK (input receives this port)
-> U123.CLK (input receives this port)
-> U156.CLK (input receives this port)
-> U161.CLK (input receives this port)
-> U164.CLK (input receives this port)
-> U100.CLK (input receives this port)
-> U110.CLK (input receives this port)
-> U131.CLK (input receives this port)
-> U140.CLK (input receives this port)
-> U173.CLK (input receives this port)
-> U91.CLK (input receives this port)
-> U118.CLK (input receives this port)
-> U126.CLK (input receives this port)
-> U128.CLK (input receives this port)
-> U129.CLK (input receives this port)
-> U130.CLK (input receives this port)
-> U5.CLK (input receives this port)
-> U6.CLK (input receives this port)
-> U94.CLK (input receives this port)
-> U125.CLK (input receives this port)
-> U142.CLK (input receives this port)
-> U451.CLK (input receives this port)
-> U7.CLK (input receives this port)
-> U8.CLK (input receives this port)
-> U120.CLK (input receives this port)
-> U139.CLK (input receives this port)
-> U168.CLK (input receives this port)
-> U317.CLK (input receives this port)
-> U95.CLK (input receives this port)
-> U102.CLK (input receives this port)
-> U112.CLK (input receives this port)
-> U119.CLK (input receives this port)
-> U127.CLK (input receives this port)
-> U154.CLK (input receives this port)
Port: O[1]
<- U464.X (output drives this port)
Port: O[0]
<- U479.X (output drives this port)
Port: success
-> U52.B (input receives this port)
<- U109.Q (output drives this port)
-> U203.A1 (input receives this port)
-> U309.B1 (input receives this port)
-> U553.A (input receives this port)That's the input and output ports for puzzle.gds. Lovely.
The heaven of an FPGA developer.
Netlist and ports in hand, the rest was a piece of cake. Well. I'll speak for myself. A piece of cake for an FPGA developer. Let me explain.
The GitHub repo was very misleading at first. I kept thinking, how the heck do you get a def/lef file, and then a netlist, and then Verilog? How??
But hang on. Verilog. Right. It's just code connecting a bunch of behavioural modules and gates. Do you get it?
I never needed to get back to the original Verilog. I simply had to write it, out of the gates and ports already sitting in my hands. Simple. But only if the gates had a behaviour model that could actually be written.
So I had to check that first. Wrote a small script.
import re
from collections import defaultdict
from sky130_cells import base_type, FF_CELLS, PASSIVE_CELLS, POWER_PINS
INSTANCE_RE = re.compile(
r"^Instance:\s+(\S+)\s+\(Type:\s+(\S+)\)\s+@\s+\(([-\d.]+),\s*([-\d.]+)\)\s+um"
)
PIN_RE = re.compile(r"^\s+(\S+)\s+->\s+(\S+)\s*$")
class Instance:
__slots__ = ("name", "cell_type", "base", "x", "y", "pins")
def __init__(self, name, cell_type, x, y):
self.name = name
self.cell_type = cell_type
self.base = base_type(cell_type)
self.x = x
self.y = y
self.pins = {} # pin_name -> net_name
def __repr__(self):
return f"<Instance {self.name} {self.base} pins={self.pins}>"
class Netlist:
def __init__(self):
self.instances = {} # name -> Instance
self.net_readers = defaultdict(list) # net -> [(inst_name, pin_name)]
self.net_driver = {} # net -> (inst_name, pin_name)
self.clk_alias_nets = set() # nets that are really "clk"
def build_indices(self):
for inst in self.instances.values():
ff = FF_CELLS.get(inst.base)
out_pins = set(ff["outputs"]) if ff else None
for pin_name, net in inst.pins.items():
if pin_name in POWER_PINS:
continue
is_output = (out_pins is not None and pin_name in out_pins) or \
(out_pins is None and pin_name in _comb_output_pins(inst.base))
if is_output:
self.net_driver[net] = (inst.name, pin_name)
else:
self.net_readers[net].append((inst.name, pin_name))
# Detect clock-tree nets: read only as CLK, never driven by anyone here.
clk_candidate_nets = set()
for inst in self.instances.values():
if inst.base in FF_CELLS and "CLK" in inst.pins:
clk_candidate_nets.add(inst.pins["CLK"])
for net in clk_candidate_nets:
if net == "clk":
continue
if net in self.net_driver:
continue # actually driven by something -> not a bare clk-tree net
self.clk_alias_nets.add(net)
def resolve_clk(self, net):
return "clk" if net in self.clk_alias_nets else net
def _comb_output_pins(base):
from sky130_cells import COMB_CELLS
if base in COMB_CELLS:
return set(COMB_CELLS[base][1])
if base in PASSIVE_CELLS:
return set()
if base == "conb":
return {"HI", "LO"}
return set()
def parse_netlist(path):
nl = Netlist()
cur = None
with open(path) as f:
for line in f:
line = line.rstrip("\n")
m = INSTANCE_RE.match(line)
if m:
name, ctype, x, y = m.groups()
cur = Instance(name, ctype, float(x), float(y))
nl.instances[name] = cur
continue
m = PIN_RE.match(line)
if m and cur is not None:
pin, net = m.groups()
cur.pins[pin] = net
continue
# blank line or comment: instance block ends implicitly
nl.build_indices()
return nl
if __name__ == "__main__":
import sys
path = sys.argv[1] if len(sys.argv) > 1 else "netlist.txt"
nl = parse_netlist(path)
print(f"Parsed {len(nl.instances)} instances from {path}")
from collections import Counter
counts = Counter(inst.base for inst in nl.instances.values())
for base, n in counts.most_common():
print(f" {base:12s} x{n}")
print(f"Detected {len(nl.clk_alias_nets)} clock-tree alias nets -> 'clk'")
unknown = {inst.base for inst in nl.instances.values()
if inst.base not in FF_CELLS
and inst.base not in PASSIVE_CELLS
and inst.base != "conb"}
from sky130_cells import COMB_CELLS
unknown = {b for b in unknown if b not in COMB_CELLS}
if unknown:
print("WARNING: no behavioral model for these cell types:", unknown)
else:
print("All cell types have behavioral models. Good to simulate.")And it just said:
......
o32ai x1
a22oi x1
o2bb2a x1
a2111oi x1
buf x1
o211ai x1
o21bai x1
Detected 16 clock-tree alias nets -> 'clk'
All cell types have behavioral models. Good to simulate.Thank god. Now I only needed to turn all these gates into boolean expressions.
"and2": (["A", "B"], ["X"], lambda p: {"X": f"({p['A']} & {p['B']})"}),
"and3": (["A", "B", "C"], ["X"], lambda p: {"X": f"({p['A']} & {p['B']} & {p['C']})"}),
"and4": (["A", "B", "C", "D"], ["X"], lambda p: {"X": f"({p['A']} & {p['B']} & {p['C']} & {p['D']})"}),
"or2": (["A", "B"], ["X"], lambda p: {"X": f"({p['A']} | {p['B']})"}),
"or3": (["A", "B", "C"], ["X"], lambda p: {"X": f"({p['A']} | {p['B']} | {p['C']})"}),........Then iterate over the netlist with plain Verilog assign statements, after declaring a hell of a lot of wires.
#!/usr/bin/env python3
import argparse
import re
import sys
from collections import defaultdict
from netlist_parser import parse_netlist
from sky130_cells import FF_CELLS, PASSIVE_CELLS
from sky130_cells_verilog import COMB_CELLS_SV
FORCE_INPUTS = {"clk", "rst_n", "I", "enable"}
FORCE_OUTPUTS = {"success"}
BUS_RE = re.compile(r"^([A-Za-z_]\w*)\[(\d+)\]$")
def sanitize(net):
if BUS_RE.match(net):
return net
return net.replace(".", "_")
def classify_ports(nl):
driven = set(nl.net_driver.keys())
all_nets = set()
for inst in nl.instances.values():
all_nets.update(inst.pins.values())
all_nets -= {"VPWR", "VGND", "VPB", "VNB", "FLOAT"}
inputs, outputs = set(), set()
buses = defaultdict(dict)
for net in all_nets:
if net in nl.clk_alias_nets:
continue # internal, not clk itself
m = BUS_RE.match(net)
is_driven = net in driven
if net in FORCE_INPUTS or (not is_driven and not m and _looks_like_port(net)):
inputs.add(net)
elif net in FORCE_OUTPUTS or (is_driven and (m or _looks_like_port(net))):
if m:
prefix, idx = m.group(1), int(m.group(2))
buses[prefix][idx] = net
else:
outputs.add(net)
inputs |= FORCE_INPUTS # e.g. 'clk' never appears literally in netlist.txt
outputs |= (FORCE_OUTPUTS - inputs)
return inputs, outputs, buses
def _looks_like_port(net):
"""Heuristic: internal auto-generated names are 'U<digits>.<pin>' or
'net_<digits>'. Anything else was a real layout label -> a port."""
if re.match(r"^U\d+\.", net):
return False
if re.match(r"^net_\d+$", net):
return False
return True
def generate(nl, module_name="puzzle"):
inputs, outputs, buses = classify_ports(nl)
lines = []
lines.append(f"// Auto-generated from netlist.txt by netlist_to_sv.py")
lines.append(f"// {len(nl.instances)} cell instances -> boolean-logic assigns/always_ff blocks.")
lines.append(f"// No dependency on the sky130 cell library - pure behavioral SystemVerilog.")
lines.append(f"module {module_name} (")
port_lines = []
for net in sorted(inputs):
port_lines.append(f" input logic {sanitize(net)}")
for bus, members in sorted(buses.items()):
width = max(members) + 1
port_lines.append(f" output logic [{width-1}:0] {bus}")
for net in sorted(outputs):
port_lines.append(f" output logic {sanitize(net)}")
lines.append(",\n".join(port_lines))
lines.append(");")
lines.append("")
# --- internal wire declarations -----------------------------------
port_nets = set(inputs) | set(outputs)
for members in buses.values():
port_nets.update(members.values())
internal_nets = set()
for inst in nl.instances.values():
if inst.base in PASSIVE_CELLS:
continue
for pin, net in inst.pins.items():
if pin in ("VPWR", "VGND", "VPB", "VNB"):
continue
if net in ("VPWR", "VGND", "FLOAT"):
continue
if net in port_nets:
continue
resolved = nl.resolve_clk(net) if net in nl.clk_alias_nets else net
if resolved in port_nets:
continue
if net in nl.clk_alias_nets:
continue # aliased directly to clk, no wire needed
internal_nets.add(net)
lines.append(" // internal nets")
for net in sorted(internal_nets):
lines.append(f" logic {sanitize(net)};")
lines.append("")
def ref(net):
"""Verilog expression to *read* a net's current value."""
if net in nl.clk_alias_nets:
return "clk"
if net in ("VPWR",):
return "1'b1"
if net in ("VGND", "FLOAT"):
return "1'b0"
return sanitize(net)
# --- combinational cells -> assign ----------------------------------
lines.append(" // combinational logic")
for inst in sorted(nl.instances.values(), key=lambda i: i.name):
if inst.base in FF_CELLS or inst.base in PASSIVE_CELLS:
continue
if inst.base == "conb":
for pin, val in (("HI", "1'b1"), ("LO", "1'b0")):
if pin in inst.pins:
net = inst.pins[pin]
if net in ("FLOAT", "VPWR", "VGND"):
continue # unused tie - nothing meaningful to drive
lines.append(f" assign {ref(net)} = {val}; // {inst.name}")
continue
model = COMB_CELLS_SV.get(inst.base)
if model is None:
lines.append(f" // WARNING: no model for {inst.name} ({inst.cell_type}) - skipped")
continue
in_pins, out_pins, fn = model
args = {p: ref(inst.pins[p]) for p in in_pins if p in inst.pins}
if len(args) != len(in_pins):
lines.append(f" // WARNING: {inst.name} ({inst.base}) missing pin(s) - skipped")
continue
outs = fn(args)
for op, expr in outs.items():
onet = inst.pins.get(op)
if onet is None:
continue
if onet in ("FLOAT", "VPWR", "VGND"):
continue # driving a tie/no-connect net, nothing to do
lines.append(f" assign {ref(onet)} = {expr}; // {inst.name}")
lines.append("")
# --- flip-flops -> always_ff -----------------------------------------
lines.append(" // flip-flops")
for inst in sorted(nl.instances.values(), key=lambda i: i.name):
if inst.base not in FF_CELLS:
continue
clk_net = inst.pins.get("CLK")
clk_expr = ref(clk_net) if clk_net else "clk"
q_expr = ref(inst.pins["Q"])
d_expr = ref(inst.pins["D"]) if "D" in inst.pins else "1'b0"
if inst.base == "dfrtp":
rb_expr = ref(inst.pins["RESET_B"])
lines.append(f" always_ff @(posedge {clk_expr} or negedge {rb_expr}) begin // {inst.name}")
lines.append(f" if (!{rb_expr}) {q_expr} <= 1'b0;")
lines.append(f" else {q_expr} <= {d_expr};")
lines.append(" end")
# NB: if a testbench ever *declares* rst_n already at 0 (rather
# than driving a real 1->0 transition after t=0), this always_ff
# never gets edge-triggered and Q stays X forever - the classic
# "reset never seen as an edge" gotcha. Force the same power-on
# default as simulator.py regardless of testbench sequencing.
lines.append(f" initial {q_expr} = 1'b0;")
elif inst.base == "dfstp":
sb_expr = ref(inst.pins["SET_B"])
lines.append(f" always_ff @(posedge {clk_expr} or negedge {sb_expr}) begin // {inst.name}")
lines.append(f" if (!{sb_expr}) {q_expr} <= 1'b1;")
lines.append(f" else {q_expr} <= {d_expr};")
lines.append(" end")
lines.append(f" initial {q_expr} = 1'b1;")
else: # dfxtp
lines.append(f" always_ff @(posedge {clk_expr}) begin // {inst.name}")
lines.append(f" {q_expr} <= {d_expr};")
lines.append(" end")
# dfxtp has no reset pin, so real silicon (and Verilog sim) would
# start it at X forever, poisoning everything downstream. Match
# simulator.py's Circuit._init_nets(), which defines "power-on"
# as Q=0 for every flop including these, so the two simulators
# agree instead of one being permanently X.
lines.append(f" initial {q_expr} = 1'b0;")
lines.append("")
# --- bus assembly (O[7:0] etc, in case any bit wasn't already the
# bus-vector identifier itself) -------------------------------
for bus, members in sorted(buses.items()):
for idx, net in sorted(members.items()):
if net != f"{bus}[{idx}]":
lines.append(f" assign {bus}[{idx}] = {ref(net)};")
lines.append("")
lines.append("endmodule")
return "\n".join(lines)
def main():
ap = argparse.ArgumentParser()
ap.add_argument("netlist", nargs="?", default="netlist.txt")
ap.add_argument("output", nargs="?", default="puzzle.sv")
ap.add_argument("--module-name", default="puzzle")
args = ap.parse_args()
nl = parse_netlist(args.netlist)
sv = generate(nl, args.module_name)
with open(args.output, "w") as f:
f.write(sv)
print(f"Wrote {args.output}: {sv.count(chr(10))} lines, "
f"{len(nl.instances)} instances translated.")
if __name__ == "__main__":
main()And there you go. We have the Verilog file. Just a small matter of 1000+ lines.
// Auto-generated from netlist.txt by netlist_to_sv.py
// 706 cell instances -> boolean-logic assigns/always_ff blocks.
// No dependency on the sky130 cell library - pure behavioral SystemVerilog.
module puzzle (
input logic I,
input logic clk,
input logic enable,
input logic rst_n,
output logic [7:0] O,
output logic success
);
// internal nets
logic U1_X;
logic U10_Y;
logic U100_Q;
logic U101_Q;
logic U102_Q;
logic U103_Y;
logic U104_Q;.........
............
assign U81_X = ((U298_X & U8_Q) | (U703_Y & U341_Y) | U673_Y); // U81
assign U82_X = ((U298_X & U6_Q) | (U168_Q & U673_Y) | U683_Y); // U82
assign U83_X = ((U271_X & U167_Q) | (net_1618 & U152_Q) | U267_X); // U83
assign U84_X = ((U298_X & U118_Q) | (U317_Q & U673_Y) | U694_Y); // U84
assign U85_X = ((U298_X & U139_Q) | (U673_Y & U120_Q) | U516_X); // U85
assign U86_Y = (~(U3_Q | U4_Q | U5_Q | (~U451_Q))); // U86
assign U87_X = ((U550_Y | U315_Y | U701_Y) & (U282_X | U629_Y)); // U87
assign U88_X = ((U386_X | U642_X | U691_Y) & (U659_Y | U252_Y)); // U88
assign U89_X = ((U286_X | U24_X | U193_X) & (U651_X | U8_Q)); // U89
assign U9_Y = (~((U71_Y & U332_Y) | (~U155_Q))); // U9.................
......
initial U98_Q = 1'b0;
always_ff @(posedge clk or negedge rst_n) begin // U99
if (!rst_n) U99_Q <= 1'b0;
else U99_Q <= U501_X;
end
initial U99_Q = 1'b0;
endmoduleWhich left exactly one thing: which sequence of input bits pushes that lovely success pin high.
All paths lead to THE TWO STARS
Back when I was still trying to solve the warmup GDS, a doubt crept in. If you were implementing an adder, nonetheless, then why use a shift register? A comparator?
So I suspected the real puzzle had to be built the same way, just nastier. Both the warmup and the puzzle took a single bit in, but the puzzle had a strict 8-bit output. Which made step one obvious: find out when the output actually starts churning.
`timescale 1ns / 1ps
//////////////////////////////////////////////////////////////////////////////////
// Company:
// Engineer:
//
// Create Date: 08/23/2026 01:56:25 PM
// Design Name:
// Module Name: tb_puzzle_replay
// Project Name:
// Target Devices:
// Tool Versions:
// Description:
//
// Dependencies:
//
// Revision:
// Revision 0.01 - File Created
// Additional Comments:
//
//////////////////////////////////////////////////////////////////////////////////
module tb_puzzle_replay;
// ---------------------------------------------------------------
// DUT hookup
// ---------------------------------------------------------------
logic clk;
logic rst_n;
logic enable;
logic I;
logic [7:0] O;
logic success;
puzzle dut (
.clk (clk),
.rst_n (rst_n),
.enable (enable),
.I (I),
.O (O),
.success (success)
);
// ---------------------------------------------------------------
// Clock: free-running, 10 ns period (period is arbitrary for a
// purely synchronous netlist like this one)
// ---------------------------------------------------------------
initial clk = 1'b0;
always #5 clk = ~clk;
// ---------------------------------------------------------------
// Reset / enable
// - rst_n low only for the very first cycle
// - enable held high the whole run
// ---------------------------------------------------------------
initial begin
rst_n = 1'b0;
enable = 1'b1;
#2 rst_n = 1'b1; // released well before the first posedge at t=5
end
// ---------------------------------------------------------------
// Exact 125-bit input sequence recovered from trace.vcd
// (cycle 1 .. cycle 125, left to right == in time order)
// ---------------------------------------------------------------
localparam int SEQ_LEN = 125;
logic [0:SEQ_LEN-1] seq_I =
{125{1'b0}};
int idx;
// Drive I on the falling edge so it is already stable and
// glitch-free by the time the following rising edge samples it
initial begin
idx = 0;
I = seq_I[0]; // valid for the very first rising edge (cycle 1)
idx = 1;
forever begin
@(negedge clk);
if (idx < SEQ_LEN) begin
I = seq_I[idx];
idx++;
end else begin
I = 1'b0; // sequence exhausted - keep the input quiet
end
end
end
int cyc;
initial cyc = 0;
always @(posedge clk) begin
cyc <= cyc + 1;
$display("[cyc=%0d t=%0t] rst_n=%0b enable=%0b I=%0b success=%0b O=0x%02h",
cyc + 1, $time, rst_n, enable, I, success, O);
end
string decoded_string = "";
bit decode_done = 1'b0;
initial begin
// Wait for exactly 122 rising clock edges
repeat (123) @(posedge clk);
while (!decode_done) begin
if (O === 8'h00) begin
$display("\n================================================================");
$display(" [t=%0t] O bus = 0x00 -> end of string", $time);
$display(" DECODED STRING: \"%s\"", decoded_string);
$display("================================================================\n");
decode_done = 1'b1;
end else begin
$display("[t=%0t] O = 0x%02h ('%c') running string so far: \"%s\"",
$time, O, O, decoded_string);
decoded_string = {decoded_string, string'(O)};
@(posedge clk); // sample every cycle
end
end
#20 $finish;
end
// ---------------------------------------------------------------
// Safety watchdog in case O never hits 0x00
// (adjust the multiplier if you extend SEQ_LEN / expect a longer string)
// ---------------------------------------------------------------
initial begin
#((SEQ_LEN + 200) * 10);
$display("\n*** WATCHDOG TIMEOUT at t=%0t - success=%0b, O=0x%02h, decoded so far: \"%s\" ***\n",
$time, success, O, decoded_string);
$finish;
end
// ---------------------------------------------------------------
// VCD dump for the waveform viewer
// ---------------------------------------------------------------
initial begin
$dumpfile("tb_puzzle_replay.vcd");
$dumpvars(0, tb_puzzle_replay);
end
endmodule
After more beating around the bush, I realised the output actually starts showing up somewhere around cycle 121 to 124. I wrote the testbench to decode on any decoding and stop immediately. Then, being an FPGA guy, I tested it with just all zeroes. Guess what?
This is the output I got:
run 1000ns
[cyc=1 t=5000] rst_n=1 enable=1 I=0 success=0 O=0x00
[cyc=2 t=15000] rst_n=1 enable=1 I=0 success=0 O=0x00
[cyc=3 t=25000] rst_n=1 enable=1 I=0 success=0 O=0x00
........
[cyc=119 t=1185000] rst_n=1 enable=1 I=0 success=0 O=0x00
[cyc=120 t=1195000] rst_n=1 enable=1 I=0 success=0 O=0x00
[cyc=121 t=1205000] rst_n=1 enable=1 I=0 success=0 O=0x00
[cyc=122 t=1215000] rst_n=1 enable=1 I=0 success=0 O=0x00
[cyc=123 t=1225000] rst_n=1 enable=1 I=0 success=0 O=0x45
[t=1225000] O = 0x45 ('E') running string so far: ""
[cyc=124 t=1235000] rst_n=1 enable=1 I=0 success=0 O=0x4d
[t=1235000] O = 0x4d ('M') running string so far: "E"
[cyc=125 t=1245000] rst_n=1 enable=1 I=0 success=0 O=0x50
[t=1245000] O = 0x50 ('P') running string so far: "EM"
[cyc=126 t=1255000] rst_n=1 enable=1 I=0 success=0 O=0x54
[t=1255000] O = 0x54 ('T') running string so far: "EMP"
[cyc=127 t=1265000] rst_n=1 enable=1 I=0 success=0 O=0x59
[t=1265000] O = 0x59 ('Y') running string so far: "EMPT"
[cyc=128 t=1275000] rst_n=1 enable=1 I=0 success=0 O=0x20
[t=1275000] O = 0x20 (' ') running string so far: "EMPTY"
[cyc=129 t=1285000] rst_n=1 enable=1 I=0 success=0 O=0x53
[t=1285000] O = 0x53 ('S') running string so far: "EMPTY "
[cyc=130 t=1295000] rst_n=1 enable=1 I=0 success=0 O=0x4b
[t=1295000] O = 0x4b ('K') running string so far: "EMPTY S"
[cyc=131 t=1305000] rst_n=1 enable=1 I=0 success=0 O=0x59
[t=1305000] O = 0x59 ('Y') running string so far: "EMPTY SK"
[cyc=132 t=1315000] rst_n=1 enable=1 I=0 success=0 O=0x00
================================================================
[t=1315000] O bus = 0x00 -> end of string
DECODED STRING: "EMPTY SKY"
================================================================
EMPTY SKY, it said.
Is this the way to go? Success pin obviously wasn't high. So what does it mean?
Maybe the puzzle's answer was as simple as all ones then? Well. For that, the console showed me this:
.......
[cyc=122 t=1215000] rst_n=1 enable=1 I=1 success=0 O=0x00
[cyc=123 t=1225000] rst_n=1 enable=1 I=1 success=0 O=0x42
[t=1225000] O = 0x42 ('B') running string so far: ""
[cyc=124 t=1235000] rst_n=1 enable=1 I=1 success=0 O=0x49
[t=1235000] O = 0x49 ('I') running string so far: "B"
[cyc=125 t=1245000] rst_n=1 enable=1 I=1 success=0 O=0x47
[t=1245000] O = 0x47 ('G') running string so far: "BI"
[cyc=126 t=1255000] rst_n=1 enable=1 I=0 success=0 O=0x20
[t=1255000] O = 0x20 (' ') running string so far: "BIG"
[cyc=127 t=1265000] rst_n=1 enable=1 I=0 success=0 O=0x42
[t=1265000] O = 0x42 ('B') running string so far: "BIG "
[cyc=128 t=1275000] rst_n=1 enable=1 I=0 success=0 O=0x41
[t=1275000] O = 0x41 ('A') running string so far: "BIG B"
[cyc=129 t=1285000] rst_n=1 enable=1 I=0 success=0 O=0x4e
[t=1285000] O = 0x4e ('N') running string so far: "BIG BA"
[cyc=130 t=1295000] rst_n=1 enable=1 I=0 success=0 O=0x47
[t=1295000] O = 0x47 ('G') running string so far: "BIG BAN"
[cyc=131 t=1305000] rst_n=1 enable=1 I=0 success=0 O=0x00
================================================================
[t=1305000] O bus = 0x00 -> end of string
DECODED STRING: "BIG BANG"
================================================================
[cyc=132 t=1315000] rst_n=1 enable=1 I=0 success=0 O=0x00Nope. Success still low. But it said BIG BANG.
All zeroes = EMPTY SKY. All ones = BIG BANG.
Well, one thing was sure. All zeroes created an empty sky. All ones blew everything up into a big bang. The cycle count starts at 1 and the output starts showing at cycle 123, so 122 - 1 = 121 bit shifts before anything comes out. That 121-bit input sequence is talking about a cosmic event.
Now all that was left was finding which 121 bits made the success pin go high.
I didn't know what BMC was. Didn't know what a SAT solver was. But I did know SYSTEMVERILOG ASSERTIONS.
It's a chip designer's way of proving his chip works right, for the properties he defined it for. And here we had exactly one property: the success pin must go high after a 121 bit input sequence.
So: a simple sysver assertion testbench, run through Yosys. We prove our property by asking yosys bmc (just discovered it had bmc) to disprove it. Classic maths proof. Assert that success must never go high, and when it does, use a python tool to pull out the 121 bit input sequence that did it.
`timescale 1ns/1ps
module tb_puzzle;
logic clk;
logic rst_n;
logic enable;
logic I;
logic [7:0] O;
logic success;
// Instantiate the reverse-engineered puzzle
puzzle dut (
.clk(clk),
.rst_n(rst_n),
.enable(enable),
.I(I),
.O(O),
.success(success)
);
// Formal-friendly clocking block
default clocking cb @(posedge clk);
endclocking
// Static array to store the history of the 'I' input (up to 200 cycles)
logic [0:199] seq_history;
integer seq_idx = 0;
// Capture the 'I' input at every clock edge when out of reset
always @(posedge clk) begin
if (rst_n) begin
seq_history[seq_idx] = I;
seq_idx = seq_idx + 1;
end
end
// ==========================================
// SYSTEMVERILOG ASSUMPTIONS (Constraints)
// ==========================================
// 1. Constrain Reset
initial assume(!rst_n);
assume_rst_high: assume property (##1 rst_n == 1'b1);
// 2. Constrain Enable
assume_enable_high: assume property (enable == 1'b1);
// ==========================================
// SYSTEMVERILOG ASSERTIONS
// ==========================================
// The "Failure" Assertion
assert_success_never_high: assert property (
success == 1'b0
) else begin
$display("\n========================================================");
$display("SUCCESS TRIGGERED! Formal solver found the sequence.");
$display("Sequence Length: %0d bits", seq_idx);
$write("Sequence: ");
for (int i = 0; i < seq_idx; i++) begin
$write("%b", seq_history[i]);
end
$write("\n");
$display("========================================================\n");
$fatal(1, "Assertion failed.");
end
endmoduleRun the BMC solver, you get the following:
...........
SBY 11:30:48 [puzzle_bmc] engine_0: ## 0:00:22 Checking assertions in step 123..
SBY 11:30:48 [puzzle_bmc] engine_0: ## 0:00:22 Checking assumptions in step 124..
SBY 11:30:48 [puzzle_bmc] engine_0: ## 0:00:22 Checking assertions in step 124..
SBY 11:30:49 [puzzle_bmc] engine_0: ## 0:00:22 BMC failed!
SBY 11:30:49 [puzzle_bmc] engine_0: ## 0:00:22 Assert failed in tb_puzzle: assert_success_never_high
SBY 11:30:49 [puzzle_bmc] engine_0: ## 0:00:22 Writing trace to VCD file: engine_0/trace.vcd
SBY 11:30:54 [puzzle_bmc] engine_0: ## 0:00:28 Writing trace to Verilog testbench: engine_0/trace_tb.v
SBY 11:30:54 [puzzle_bmc] engine_0: ## 0:00:28 Writing trace to constraints file: engine_0/trace.smtc
SBY 11:30:54 [puzzle_bmc] engine_0: ## 0:00:28 Writing trace to Yosys witness file: engine_0/trace.yw
SBY 11:30:55 [puzzle_bmc] engine_0: ## 0:00:29 Status: failedSBY 11:30:55 [puzzle_bmc] engine_0: finished (returncode=1)
SBY 11:30:55 [puzzle_bmc] engine_0: Status returned by engine: FAIL
SBY 11:30:55 [puzzle_bmc] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:29 (29)
SBY 11:30:55 [puzzle_bmc] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:29 (29)
SBY 11:30:55 [puzzle_bmc] summary: engine_0 (smtbmc z3) returned FAIL
SBY 11:30:55 [puzzle_bmc] summary: counterexample trace: puzzle_bmc/engine_0/trace.vcd
SBY 11:30:55 [puzzle_bmc] summary: failed assertion tb_puzzle.assert_success_never_high at tb_puzzle.sv:54.32-67.8 step 124
SBY 11:30:55 [puzzle_bmc] DONE (FAIL, rc=2)SBY 11:30:55 The following tasks failed: ['bmc']And now to extract where exactly the pin went high, through some AI-generated python code. We get this.
⦗Tabby CAD Suite⦘ kal-thir@kitanoken:~/bmc$ python3 extract_witness.py puzzle_bmc/engine_0/trace.vcd --clk clk --signals rst_n,enable,I,success
NOTE: 'clk' matched multiple ids ['n2', 'n773'], using first
NOTE: 'rst_n' matched multiple ids ['n782', 'n785'], using first
NOTE: 'enable' matched multiple ids ['n774', 'n784'], using first
NOTE: 'I' matched multiple ids ['n0', 'n3'], using first
NOTE: 'success' matched multiple ids ['n783', 'n786'], using first
cycle | time | rst_n | enable | I | success
-------+--------+--------+--------+--------+--------
1 | 10 | 1 | 1 | 0 | 0
2 | 20 | 1 | 1 | 0 | 0
3 | 30 | 1 | 1 | 0 | 0
4 | 40 | 1 | 1 | 0 | 0
5 | 50 | 1 | 1 | 0 | 0
6 | 60 | 1 | 1 | 0 | 0
7 | 70 | 1 | 1 | 0 | 0
............
120 | 1200 | 1 | 1 | 0 | 0
121 | 1210 | 1 | 1 | 0 | 0
122 | 1220 | 1 | 1 | 0 | 0
123 | 1230 | 1 | 1 | 0 | 1
124 | 1240 | 1 | 1 | 1 | 1
125 | 1250 | 1 | 1 | 1 | 1
rst_n bit-sequence (125 cycles): 11111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111
enable bit-sequence (125 cycles): 11111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111111
I bit-sequence (125 cycles): 00000001010100001000000000000101010100000000000010100000010000010000001000001010000100000001000000100000100100010100000000011
success bit-sequence (125 cycles): 00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000111
⦗Tabby CAD Suite⦘ kal-thir@kitanoken:~/bmc$
And there's our input sequence. Feed that back into our original testbench and we get the final answer to the puzzle.
cyc=122 t=1215000] rst_n=1 enable=1 I=0 success=0 O=0x00
[cyc=123 t=1225000] rst_n=1 enable=1 I=0 success=1 O=0x28
[t=1225000] O = 0x28 ('(') running string so far: ""
[cyc=124 t=1235000] rst_n=1 enable=1 I=1 success=1 O=0x2a
[t=1235000] O = 0x2a ('*') running string so far: "("
[cyc=125 t=1245000] rst_n=1 enable=1 I=1 success=1 O=0x20
[t=1245000] O = 0x20 (' ') running string so far: "(*"
[cyc=126 t=1255000] rst_n=1 enable=1 I=0 success=1 O=0x54
[t=1255000] O = 0x54 ('T') running string so far: "(* "
[cyc=127 t=1265000] rst_n=1 enable=1 I=0 success=1 O=0x57
[t=1265000] O = 0x57 ('W') running string so far: "(* T"
[cyc=128 t=1275000] rst_n=1 enable=1 I=0 success=1 O=0x4f
[t=1275000] O = 0x4f ('O') running string so far: "(* TW"
[cyc=129 t=1285000] rst_n=1 enable=1 I=0 success=1 O=0x20
[t=1285000] O = 0x20 (' ') running string so far: "(* TWO"
[cyc=130 t=1295000] rst_n=1 enable=1 I=0 success=1 O=0x53
[t=1295000] O = 0x53 ('S') running string so far: "(* TWO "
[cyc=131 t=1305000] rst_n=1 enable=1 I=0 success=1 O=0x54
[t=1305000] O = 0x54 ('T') running string so far: "(* TWO S"
[cyc=132 t=1315000] rst_n=1 enable=1 I=0 success=1 O=0x41
[t=1315000] O = 0x41 ('A') running string so far: "(* TWO ST"
[cyc=133 t=1325000] rst_n=1 enable=1 I=0 success=1 O=0x52
[t=1325000] O = 0x52 ('R') running string so far: "(* TWO STA"
[cyc=134 t=1335000] rst_n=1 enable=1 I=0 success=1 O=0x53
[t=1335000] O = 0x53 ('S') running string so far: "(* TWO STAR"
[cyc=135 t=1345000] rst_n=1 enable=1 I=0 success=1 O=0x20
[t=1345000] O = 0x20 (' ') running string so far: "(* TWO STARS"
[cyc=136 t=1355000] rst_n=1 enable=1 I=0 success=1 O=0x2a
[t=1355000] O = 0x2a ('*') running string so far: "(* TWO STARS "
[cyc=137 t=1365000] rst_n=1 enable=1 I=0 success=1 O=0x29
[t=1365000] O = 0x29 (')') running string so far: "(* TWO STARS *"
[cyc=138 t=1375000] rst_n=1 enable=1 I=0 success=1 O=0x00
================================================================
[t=1375000] O bus = 0x00 -> end of string
DECODED STRING: "(* TWO STARS *)"
================================================================
And folks. That's our answer.
(* TWO STARS *)
And it's quite easy to see why THIS was the answer. Also the fact that they used (* *) tells you it was Jane Street's own OCaml language, HardCaml, that probably built this hardware design.
Now look at the two deductions above and the input bit sequence that gets you the answer. Stare at it for a little over a week, like I did, and you notice 121 is 11². Lay the sequence out in an 11 by 11 matrix and you get:
0 0 0 0 0 0 0 1 0 1 0
1 0 0 0 0 1 0 0 0 0 0
0 0 0 0 0 0 0 1 0 1 0
1 0 1 0 0 0 0 0 0 0 0
0 0 0 0 1 0 1 0 0 0 0
0 0 1 0 0 0 0 0 1 0 0
0 0 0 0 1 0 0 0 0 0 1
0 1 0 0 0 0 1 0 0 0 0
0 0 0 1 0 0 0 0 0 0 1
0 0 0 0 0 1 0 0 1 0 0
0 1 0 1 0 0 0 0 0 0 0None of the ones touch each other. Not even diagonally. And there are two ones in every row and column.
Because if they do touch, they're gonna blow up. In other words, a big bang. And if they aren't there at all, we would be staring at an empty night sky. That was what it meant.
EASTER EGGS IN THE REPO?
Well, the one I could find was this. Whenever I gave a wrong input bit sequence, the chip exclaimed:
================================================================
[t=1315000] O bus = 0x00 -> end of string
DECODED STRING: "TRY AGAIN"
================================================================But then I never found any use for the vcd input file. Except for one line sitting in it: $date Sat Dec 31 23:59:60 2016 $end. That's the most recent real leap second, every second accounted for as our beloved Earth's rotation keeps slowing.
And a few others, like the version field reading "Leave no Stone Unturned".
And obviously, as I mentioned before, the likely use of HardCaml for creating this hardware design.