← The Elemental Codices · Artifacts
TEMPO · lane-parallel co-simulation · writeup

Scaling Out Lane Parallelism

~18,000 programs/s · 65 M/hour (Mac mini)

A lane-parallel harness for TEMPO, our Tiny Tapeout ASIC, runs thousands of random programs at once on the chip's gate-level netlist, one program per bit-sliced lane, on a CPU or a GPU, and compares each with an independent reference model. It found four confirmed gaps between that model and the chip (since resolved in the model, along with eight more that reviews and audits turned up) and went from about 1,000 programs a second (the first end-to-end harness, on an M5 Max) to about 18,000 on a Mac mini, with every speed-up proven identical to what it replaced before it counted.

~18,000programs/s peak, one Mac mini, as of 2026-09-22 (from ~1,000 on an M5 Max at the first end-to-end harness)
12ISS-vs-chip divergences (4 from the sweeps, 8 from later reviews and audits), all on the model side: 11 fixed, 1 documented
33 of 45netlist-changing RTL mutants killed at lane scale (was 7 of 46)
8,000,000seeds in the largest single sweep, every mismatch a known cause
0mismatches in 5,500,000 seeds swept since the fixes of 2026-09-25
1,200,000programs identical on the generic-gate netlist, the signoff netlist and the GDS built for submission, as RETRACE reads it
Every change, measured the same way. Each row is one change, timed as a pair of million-seed sweeps on the Mac mini: the same seeds (2,000,001–3,000,000), classification included, and results identical block by block in every run. From the second row on, each pair is an interleaved A/B measured in one session; the first compares the streamed sweep with the per-block sweep it replaced. Hollow dots are the runs before the change, solid dots the runs after; the labels are their means and the speed-up is the ratio of the means. The axis is logarithmic, so equal speed-ups have equal length, and faster is to the right. The rows do not chain exactly: the mini's baseline drifted between sessions (the run before fastgen took 187 s where the row above, measured a few hours earlier, ended at 168 s), and smaller changes landed between rows (the 1-in-256 generator check and one ISS run per classification variant before the vector-classification row). The last row compares the two ends on the same machine and seeds, measured on different days: 458 s per million seeds with the per-block sweep, 55.6 s with fastiss, about 18,000 programs a second.

Lane-parallel co-simulation of TEMPO, a Tiny Tapeout ASIC: running thousands of random programs at once against a synthesized gate-level netlist, and proving every speed-up exact along the way

Result. lanes/ runs TEMPO's synthesized gate-level netlist next to an independent, vectorised instruction-set model, one random program per bit-sliced lane, at up to about 18,000 programs a second on a single Mac mini; the first end-to-end harness managed about 1,000 programs a second, on an M5 Max. At that scale it found four real places where the reference model disagreed with the chip (findings 15–18), confirmed them by re-running seeds on the RTL under Icarus (same diffs), and used the same harness to lift a mutation campaign's kill rate from 7 of 46 RTL mutants to 33 of 45. Since publication all four have been fixed in the reference model, reviews and audits of those fixes turned up eight more (seven fixed the same way, one documented as a reserved setting), and the generator gap A1 has been fixed, so sweeps that used to end in about a thousand explained mismatches per million seeds now match on every seed; and the GDS built for submission, read back by RETRACE, runs through the same harness identically to the signoff netlist (section 8).

How we know. Every mismatch the harness reported was re-run against the known causes of the time and, where the cause was new, confirmed by replaying the same seed through the pre-existing test_cosim harness on the RTL under Icarus; since every known cause has been fixed (2026-09-25), any mismatch now counts as new. Every speed-up along the way — a faster assembler, a C port of the program generator, a C port of the instruction-set simulator, a rewritten GPU kernel, a cheaper way to classify a mismatch — was proven bit- or word-identical to what it replaced before it was allowed to run, usually across hundreds of thousands to millions of seeds, and several of the larger changes were checked further by a separate adversarial review pass before merge.

Project writeup, 2026-09-22; revised 2026-09-27 (see the revision log). Repository: tempo, branch main (the lanes branch was merged on 2026-09-24; not yet public; citations are given as plain text until it is released). Work described: 2026-09-18 through 2026-09-22, and in section 8 through 2026-09-26.

The problem: one program at a time

TEMPO already had a co-simulation harness (test/cosim/) that runs random programs against the RTL under Icarus and compares the result, instruction by instruction, with tools/tempo/iss.py, a golden model that is architecturally exact and cycle-exact for TIME-related behaviour. That harness compares registers and halt codes of both hardware threads, POUT, PINCFG, the 256 data words, the C2H FIFO, FLAGS, STATUS, and every pad edge — TIME, pin and level — including the IRQ line. It is thorough, and it is also the standard against which everything below has to agree, because lanes/ changes none of it: not the RTL, not tools/tempo/iss.py, not test/cosim/ itself. (The fixes its findings later led to went into iss.py and test/cosim/gen.py openly, one recorded finding at a time, after each was confirmed on the RTL; see section 8.) What that harness cannot do cheaply is run at scale: one program under Icarus, seed by seed, is slow enough that a wide random sweep is an overnight job, and the class of bug most worth finding — a rare corner where a per-cycle model quietly disagrees with real silicon — needs a lot of random seeds to surface at all.

This piece is a sequel to Retracing Two Stars, which built an independent LVS check for TEMPO's sign-off GDS. Where that piece asked whether the manufactured layout matches the design, this one asks whether the design's own reference model matches the design — at a scale the existing harness could never reach on its own.

Thesis: run the same comparison thousands of times at once, and prove every shortcut exact first

The idea behind lanes/ is to keep test_cosim's comparison exactly as it is, but run it bit-sliced: one random program per lane, thousands of lanes at once, on the CPU with numpy or on the Apple GPU as one Metal kernel generated straight from the netlist. Nothing about what is compared changes; only how many comparisons run in parallel, and how cheaply each one can be produced. Every one of the five pieces below has its own oracle, and the later throughput work never counted until it matched the piece before it.

StageOutputOracle
Program generationa random TEMPO assembly program per seedword-identical to test/cosim/gen.py plus tools/tempo/asm.py (fastasm: 170,000 + 1.3 million fuzzed programs; fastgen: 7.1 million seeds, 25 configurations)
Stimulus schedulethe per-seed schedule of random pin togglesbit-identical to stimulus.make_schedule (248,001 seeds, including edge cases around 231–264 and negative seeds)
Vectorised ISSthe reference model's state, run in laneslockstep-identical to tools/tempo/iss.py every cycle (335,447 lane-cycles for the first port; ~79,000 lockstep programs and 1,250,000+ harness seeds for the C port, fastiss)
Netlist evaluatorthe gate-level chip's state, bit-slicedCPU (numpy) and GPU (Metal) evaluators checked bit-identical every 16–32 cycles; a rewritten GPU kernel checked against an earlier kernel's digests over a million seeds
Mismatch classifiera cause label for every mismatching seedre-run against known-cause model variants, with the causes confirmed on the RTL under Icarus (28 seeds re-run with test_cosim: 20 of the 92 two-thread mismatches, 8 of the 28 single-thread new-cause seeds); a cheaper classification path proven identical to the original on 7,549 mismatches (since the fixes of 2026-09-24/25 no known cause is left: any mismatch is new)

1. What the harness is

A lane loads with every flop and the SRAM read register at zero and the program image written into SRAM directly. It then boots exactly as the RTL test harness does — reset low for 5 cycles, high for 5, then IRQ_MASK, PUSH and CTRL written over the real SPI host port with the same bit timing the RTL testbench uses, each transaction padded to an even cycle count so every lane starts at the same slot phase as align_start(0). It runs with the seed's own stimulus schedule on ui_in[7:3], halt read from u_top.u_core.halted_r, and 64 more cycles recorded after the last HALT — the same window the RTL harness keeps polling STATUS for. The pad model resolves uio pins the way the real pins do (the chip's output-enable wins, else the external pull-up), and every pad edge is folded into a per-lane splitmix64 rolling hash (lanes/events.py) rather than stored edge by edge, so thousands of lanes' full edge histories cost almost nothing to compare.

The netlist itself runs bit-sliced two ways: 64 lanes packed into a uint64 word on the CPU with numpy, or 32 lanes packed into a uint32 word on the Apple GPU, as one Metal kernel generated directly from the synthesized netlist and run through MLX — 131,072 lanes reachable in one launch on an M5 Max. Two netlists are used throughout: the generic-gate netlist Yosys synthesizes straight from the RTL (22,894 primitive gates, 2,764 flops), and the sg13cmos5l sign-off netlist, test/gate_level_netlist.v (30,734 primitive gates, 2,832 flops); both carry the SRAM macro as a per-lane array. That sign-off netlist was the v0.2-signoff layout; the file has held v0.3-signoff (30,736 gates, 2,832 flops) since, and a third netlist is now built from the GDS itself (section 8).

ModuleWhat it does
lanes/netlist.pyYosys JSON → a flat, levelised program; folds constants, removes buffers, keeps RTL net names, recognises mux cells by truth table instead of flattening them to primitive gates; since 2026-09-24 ties each compiled program to the SHA-256 of the files it was made from.
lanes/sim_cpu.py / sim_mlx.pythe bit-sliced CPU evaluator and its GPU twin — the same lane machinery (boot, stimulus, pad model, halt detection), checked bit-identical to each other.
lanes/iss_vec.py / fastiss.pytools/tempo/iss.py ported to run L lanes at once, first in numpy, later as a C port; lockstep-identical to the scalar Machine.
lanes/pipeline.pythe program supply: long-lived worker processes that keep the netlist lanes full and hand the main process packets as programs finish.
lanes/whatif.pyclassifies a mismatching seed against known causes (findings 15–18 and generator artefact A1, until their fixes of 2026-09-24/25 left only the base model); anything else is new and stops the sweep for a human to look at.
lanes/sweep.py / fleet.pya long unattended run, or the same run spread across this Mac and the mini over ssh, streamed through one program supply and one netlist loop.
lanes/mutation.py / faults.pythe RTL mutation catalogue and gate-level stuck-at faults, run at lane-parallel scale.
lanes/retrace_netlist.pysince 2026-09-26: a netlist of the GDS built for submission, extracted by RETRACE, with connectivity from the GDS alone (section 8).

2. What it found

Six acceptance milestones (M1–M6) built the harness up piece by piece, each one an independent check against the existing reference before the next piece was trusted.

MilestoneCheckResult
M1CPU evaluator vs. cosim.common.iss_runseeds 1–8 (one lane each) and 64 seeds in 64 lanes: all match, every key including every pad edge
M2vectorised ISS vs. scalar Machine, whole state every cycle256 two-thread + 64 one-thread seeds (335,447 lane-cycles): identical; three independent adversarial reviews (every handler diffed, 7.5 million lane-cycles of directed lockstep) found nothing
M310,000 seeds, 4,096 CPU lanes, on the mini9,992 match; the 8 mismatches (5 generator artefacts, 3 finding 15) all reproduce with identical diffs under test_cosim on the RTL
M4Metal (GPU) evaluator vs. CPU evaluator, bit-identical every 16 cycles; 100,000 seeds in one run97.6 s: 99,908 match; the 92 mismatches (57 A1, 23 finding 15, 12 finding 16) all explained; 20 of them re-run on the RTL with test_cosim, identical diffs
M5sign-off netlist vs. generic-gate netlist, same 100,000 seedsidentical compared state for every seed, and the same 92 mismatches with the same diffs
M6RTL mutation catalogue and gate-level stuck-at faults, at scale33 of 45 netlist-changing mutants killed (was 7 of 46); 74.7% / 75.8% of sampled stuck-at faults detected — see below

Checked

M5's result — that the sign-off netlist and the generic-gate netlist agree, seed for seed — is not a spot check: it is every compared field, plus the pad-edge hash, over the same 100,000 seeds, digest by digest. The two netlists come from different Yosys flows and use different cells; there is no reason they would agree by construction if either had a real discrepancy the comparison could see.

Four findings, one generator artefact (all since resolved)

Across the 100,000-seed run and a follow-up 50,000-seed single-thread run, every mismatch reduced to one of four confirmed ISS-vs-chip divergences or one generator artefact. lanes/ changes neither the ISS, the generator, nor ISA.md — each finding below was recorded (here, in docs/spec/VERIFICATION.md §8 and as a variant in lanes/whatif.py) and confirmed on the RTL before anyone touched the reference, and none was fixed by silently editing it. All five have since been fixed openly, in the model or the generator and never in the RTL: the dated notes below say when, and section 8 of this page how.

  1. Finding 15 — a receive word dropped one cycle too late by the ISS (23 of 100,000 seeds). A SIN that pops the serializer's result register in the same cycle a new word completes should see that register as full: the RTL tests the registered rx_result_valid_q (src/tempo_ser.v:468), which is still 1 in the pop cycle, so the new word is dropped and overrun is set (tempo_ser.v:472-473). The ISS instead clears rx_valid inside the SIN handler's own execute phase, so the same cycle's incoming word finds the register free and is kept without an overrun. The RTL follows ISA.md 4.7's own rule ("if free, else dropped and overrun set"); the ISS is the side to fix.
    Confirmed by test_cosim on the RTL under Icarus, seeds 4656, 7212 and 9294 among them; each matches on every key once the ISS records the cycle of the last pop.
    li r3, 0x10060
    scfg 0, r3
    li r3, 0x480        ; SPER 4.5
    sper 0, r3
    rdtime r3
    addi r3, r3, 4
    sstart 0, r3
    sin r1, 0, 1        ; arm, pop word 1
    sin r2, 0, 1        ; pop word 2
    nop
    nop
    nop
    sin r6, 0, 1        ; pops the waiting word in the cycle the next word completes
    sstat r4, 0         ; RTL 0x10012 (overrun), ISS 0x10011
    halt 1
    Resolved 2026-09-24 iss.py, VecISS and fastiss.c now let the pop take effect a cycle later, as the RTL does (053b1a3); ISA.md 4.7 states the rule.
  2. Finding 16 — a mid-word bit-order change leaves stale bits in place on the RTL (12 of 100,000 seeds). An SCFG that flips msb_first while a receiver is armed mid-word: the RTL writes each bit at a fixed index, rx_widx = msb_first ? (rx_nbits_q - rx_pos_q) : rx_pos_q (src/tempo_ser.v:249-251), clearing the register only when SIN arms it (tempo_ser.v:459-463). The ISS instead shifts bits in as they arrive, so a mid-word flip makes the two models diverge (seed 74307: RTL 0x7ff8000, ISS 0). The RTL implements its own documented design; ISA.md 4.7 should say what a bit-order change mid-word does, and the ISS should write each bit at the RTL's fixed index instead of shifting.
    Resolved 2026-09-24 the ISS writes each received bit at the RTL's fixed index and sends each transmitted bit at the live msb_first ? nbits-1-k : k (that transmit half, which no generated program reaches, was found afterwards with directed programs); ISA.md 4.7 says what a mid-word change does.
  3. Finding 17 — the ISS starts with a cold pad synchronizer the RTL never resets (20 of 50,000 single-thread seeds). The RTL's pad synchronizers (src/tempo_tio.v:109-139) run continuously from reset through the whole SPI boot and are cleared only by rst, not by run or time_rst (tempo_tio.v:98-107), so at TIME 0 the netlist already reads the settled pad vector. The co-simulation instead starts the ISS's synchronizer state at zero, so an INP or a rising-edge WATCH issued by a thread's very first instruction can disagree with the RTL (10 seeds each symptom). The fix belongs in the harness's start state, not the ISS's per-cycle rules: align_start should preload the synchronizer with the settled pad vector.
    Resolved 2026-09-24 Machine.align_start now starts the co-simulation with the synchronizers settled; ISA.md 1.4 states the rule.
  4. Finding 18 — the RTL's 5-bit transmit counter wraps after a 32-bit word's last bit (8 of 50,000 single-thread seeds). The RTL's transmit position counter is 5 bits (src/tempo_ser.v:78) with no upper bound in clocked serializer modes (tempo_ser.v:436-437), so the drive edge after a 32-bit word's last bit wraps it past 31 and SSTAT's tx_bits_left reads 32, then 31, and so on, where the ISS's unbounded counter reads 0. Only 32-bit words in clocked (SPI-like) modes reach the wrap.
    Confirmed by test_cosim on the RTL under Icarus, among the 8 of the single-thread run's 28 new-cause mismatches (findings 17 and 18 combined) re-run there; the fix masks the ISS's transmit-position counter to 5 bits in the clocked tick.
    li r1, 176226        ; out_pin 2 | in_pin 3 | clk_pin 12 | tx_en | clk_src
    scfg 0, r1
    sstart 0, r0
    li r2, 0x89ABCDEF
    sout 0, r2, 32
    nop
    nop
    li r4, 31
    L1:
      setp 0x1000          ; leading edge: sample
      clrp 0x1000          ; trailing edge: drive the next bit
      djnz r4, L1
    nop
    nop
    sstat r3, 0          ; RTL 0x2014 (tx_bits_left 32), ISS 0x14 (0)
    halt 0
    Resolved 2026-09-24 the ISS's clocked transmit counter now wraps at 5 bits, as the RTL's does.

A1 (57 of the first 100,000 seeds; not a model difference). The generator, test/cosim/gen.py, is supposed to drain any pending timed output with a final WAITT before HALT — but it only decides to emit that drain from whether the main body used a timed output (gen.py:719), and subroutines are generated after the halt line (gen.py:724-730). A thread whose only timed outputs live in subroutines can halt with an output still queued, which the RTL harness (and the netlist lane) later fire but the ISS's fixed halt-plus-2 window (test/cosim/common.py:166) misses. Running the unmodified ISS 64 cycles past halt instead of 2 matches on every key in all 57 cases — this is a generator gap, not a disagreement about the chip.

Resolved 2026-09-25 fixed in the generator itself (e7bc8f6), not by widening the ISS's window: a called subroutine's queued timed output now gets the drain too, and the sweeps that used to show A1 match on every seed (section 8).

Every one of these causes was confirmed independently: 20 of the two-thread run's 92 mismatches and 8 of the single-thread run's 28 new-cause mismatches were re-run through test_cosim on the RTL under Icarus, and every one failed there with the identical diff the netlist lane had found. As the project's own notes put it: every checked mismatch so far comes from the ISS or the generator, never the RTL — the netlist lanes agree with the RTL on all 28 seeds re-run so far across both sweeps (20 from the two-thread run, 8 from the single-thread one).

3. How fast

The first end-to-end version of the harness — 16 worker processes each building a chunk of programs and running it on a fresh vectorised ISS — ran the same 20,000 seeds on both backends: 752 programs/s on the GPU, 266 on the CPU, identical 21 mismatches on each. On M4’s separate 100,000-seed run, the same first-version harness checked about 1,000 programs a second (97.6 s, 3.7 million an hour). The netlist simulation itself was already 26 times faster on the GPU at those lane counts, and up to 96 times faster at 131,072 lanes, but the GPU sat idle 70–92% of the time: building each program in Python (mostly the assembler) plus running its ISS cost about 5 ms of CPU per seed, and that set the pace, not the simulator. Several further rewrites, each proven exact before it counted, closed that gap; the chart at the top shows what each one bought on the Mac mini.

StepMachineBeforeAfter
Streaming program supply (pipeline.py, fastasm.py)M5 Max, M4's 100,000 seeds97.6 s (1,024/s)26.6 s (3,759/s); same 92 mismatches
— same supply, 1M seedsMac mini—215 s (4,651/s, 16.7 M/hour); all 1,095 mismatches known causes
Batched classification + streamed sweepMac mini, 1M seeds458 s (per-block sweep)236 s including classification; identical block by block
Batched lane loading, cheaper worker buildsMac mini, 1M seeds237.5 / 238.7 s196.7 / 196.7 s; identical results
— same speed-upsM5 Max, M4's 100,000 seeds (re-measured 2026-09-19)26.1 s20.8 s; identical results
Fleet across two machinesM5 Max + mini, 4M seeds474 s (8,440/s)389 s (10,293/s, 37 M/hour); all 4,333 mismatches known causes
Metal kernel rework + vectorised-ISS reworkMac mini, 1M seeds196.9 / 197.6 s (5,079/s)173.3 / 174.0 s (5,771/s); identical block by block
Program generator in C (fastgen.c)Mac mini, 1M seeds188.5 / 186.0 s (5,305–5,376/s)117.7 / 118.1 s (8,468–8,493/s); every program built by fastgen
Classification from the lane's own readout vectorMac mini, 1M seeds89.7 / 91.5 s80.5 / 80.3 s (~15% less CPU); 1,120 vector verdicts, 80 sampled checks, 0 disagreements
ISS in C (fastiss.c)Mac mini, 1M seeds80.6 / 79.2 s55.7 / 55.5 s (17,950–18,031/s, ~65 M/hour); same coverage counts

The largest single run to date is a two-machine fleet sweep of 8,000,000 further seeds (3,000,001–11,000,000, split into two 4-million-seed segments), the second run after the host-side speed-ups landing at 10,293 programs/s: every one of the 8,716 mismatches across both segments reduced to a known cause. The harness's overall arc, per STATUS.md, runs from about 1,000 programs a second on the first end-to-end harness (M5 Max, before the streaming supply) to about 18,000 on a Mac mini after every optimization above — with every step along the way proven bit-exact first. (Since the fixes of 2026-09-25 a clean million takes 44.2 s on the mini, because nothing is left to classify; see section 8.)

4. How we kept every speed-up exact

Every rewrite in the table above is a C port, a rewritten kernel, or a cheaper code path standing in for something slower and already trusted. The rule that held throughout: a speed-up is not "fast," it is "fast and lockstep-identical, word-identical, or bit-identical" — and it stays that way even after the model it mirrors changes.

Fingerprint gates. Both C ports, fastgen.c (the program generator) and fastiss.c (the instruction-set simulator), record a sha256-prefix fingerprint of every Python source they mirror — gen.py, asm.py, isa.py and make_program for fastgen; iss.py, isa.py, VecISS's harness semantics and the readout layout for fastiss — and make themselves unavailable, falling back to the slower Python path, the moment the checkout's fingerprint differs from what they were verified against. The gate exists because of a concrete near miss: an early version of fastgen tied its availability only to a build hash of its own C source. A one-line edit to gen.py (removing its last undefined SUB encoding) left fastgen available and building the old generator's programs — 200 of 3,000 harness programs differed from what the edited generator would have produced, and the in-run 1-in-64 spot check caught only 6 of them.

Near miss, closed

Without the fingerprint, a routine edit to the reference model could have left the fast path silently building stale programs, with only a 1-in-N sample standing between that and a mismatch being misreported. A follow-up recheck found the same shape of gap one layer deeper: the fingerprinted "reference" fastgen compared itself against was itself a hand copy of make_program's construction, not make_program itself — an edit to make_program would have been compared against the stale copy and could still have passed (500 of 500 seeds differed from the edited function in the experiment that showed this). Both fixes point the fingerprint and the in-run check at the live reference, not a copy of it.

What each speed-up actually proved. The vectorised ISS was checked lockstep-identical to the scalar model on 335,447 lane-cycles and then reviewed three times independently (every handler diffed by hand, 7.5 million lane-cycles of directed lockstep, the paths random programs never reach exercised by directed programs); nothing was found. fastasm.py matched the reference assembler word for word on 170,000 generated programs and 1.3 million fuzzed ones. fastgen.c matched the reference generator and assembler together on 7.1 million seeds across 25 configurations — every workers' spot-check now rebuilds 1 program in 256 through the full reference path (it was 1 in 64 until 2026-09-21), which cost about 16% of a worker's build time and now costs about 4%. fastiss.c matched iss.py in every state field after every cycle on roughly 79,000 lockstep programs, and matched the ISS it replaces (VecISS) on the same readout vectors, status, cycles and coverage counters across 1,250,000 harness seeds; its own load-time self-test runs a further lockstep and cross-check in about 0.16 seconds every time a worker process starts. Both C ports were also adversarially reviewed: no case of either building a wrong program or computing a wrong result survived review, in either case — what the reviews found and fixed were plumbing issues around the ports (header and argument checks the C side lacked, a schedule read from the caller's array instead of copied, a load interrupted mid-way that could leave a lane reading a stale schedule, checks that defaulted to the wrong start phase), not wrong simulated behaviour.

Fail-safe by construction. Both ASan and UBSan builds of fastiss.c were exercised on thousands of lockstep programs and tens of thousands of harness seeds and found nothing; more usefully, builds with a deliberately planted fault — an ADD computing SUB, an inverted Manchester-decode check, a dropped coverage counter, swapped readout bits, a post-halt window cut one cycle short — all fail the load-time self-test, and each is caught by the specific check meant for it (the lockstep sees the state faults, the comparison with VecISS sees the coverage fault, the result check the readout fault). One planted-fault case only shows up reliably across a batch of programs, not a single one, which is why the self-test runs a mix of generated and random programs rather than a lone directed case.

Proving a cheaper classifier exact. Classifying a mismatch used to mean re-running the seed on a scalar netlist lane; a cheaper path classifies straight from the readout vector the GPU already harvested when the lane finished. That is only safe because nothing compared changes once a lane is marked DONE: the core is halted, the host port idle, the last queued timed output fires within about 49 cycles of the last HALT, well inside the 64-cycle recording window. That invariant was measured, not assumed — zero changes from DONE to DONE+300 across 44,865 lanes, and zero more at DONE+63 and DONE+255 across 50,000 further lanes — and a 2,048-seed regression guard now fails automatically if a future change lets compared state move after DONE. Before vector classification became the default, it ran for 7,000,000 seeds (5 million on the M5 Max, 2 million on the mini) in "both" mode, comparing the vector verdict against a full CPU re-run on every one of the 7,549 mismatches that came up. It disagreed zero times.

Checked

Vector classification kept a running honesty check even after becoming the default: 1 seed in 16 (chosen by a hash of the seed) is still re-run on the CPU as a spot check, and any disagreement, digest mismatch, or vector-path failure exits the sweep with a nonzero status rather than reporting a clean result. On the largest runs measured this way, that check has never once disagreed with the vector verdict. Since the fixes of 2026-09-25 it has had nothing to check: the sweeps end with no mismatches, and with no known cause left to trust, any mismatch would get the full CPU re-run anyway.

5. Case study: the M4 Pro's shader compiler

The 2026-09-21 rework of the Metal kernel split each 32-lane word's logic across 16 SIMD groups instead of one thread doing all the work, deriving each thread's SIMD group from Metal's own simdgroup_index_in_threadgroup attribute rather than computing it from the thread's linear position — a change made specifically so the kernel's ballot bit order would hold portably on any GPU. On the mini's M4 Pro GPU, that version made test_sim_mlx fail deterministically, always at cycle 464: lane 65's u_top.u_ser.u_ser0.rx_shreg_q received a bit at index 1546 instead of the correct 1544. The identical kernel source ran exactly on the M5 Max.

The state and inputs going into the failing cycle matched the CPU model exactly, and no single flipped input bit reproduced the GPU's wrong result. Replaying the relevant block of combinational logic in Python, using the CPU model's own inputs, reproduced the GPU's stored values only if one specific gate — v3914 = Q501.z | ~Q197.w, or the quad component feeding its only partner — was evaluated wrongly; that single wrong value explained all 265 flops the block stores. An extra barrier per cycle, forcing a fixed thread count, and using a fresh working buffer every launch all failed the same way; adding unrelated code that checked every SIMD ballot's active mask made the failure disappear. That pattern — unrelated code changing the result, no data race or bad input identifiable, one machine affected and not another — points at the shader compiler itself, not the kernel's logic.

The fix was to keep the kernel's original, thread-position-derived SIMD indexing, which computes the same values as the attribute-derived form on both GPUs but does not trigger the miscompile on the M4 Pro. Twenty-four kernel-related tests passed on the mini and the full 136-test suite passed on the M5 Max afterward, and a run of seeds 5,000,001–6,000,000 on the mini gave every per-seed readout digest identical to the pre-rework kernel's, with the same 1,118 mismatches and diffs. The tests that exercise the generic-gate netlist had been silently skipping on the mini before this (it has no local Yosys), which is part of why the miscompile went unnoticed until a change specifically targeted at portability triggered it; they now also run wherever a compiled netlist file already exists.

Fix cfb124f (2026-09-21): reverts to position-derived SIMD indices, exact on both GPUs.

The house rule that came out of this is stated plainly in the kernel's own notes: a kernel change is checked on both GPUs, against the numpy evaluator (the unit tests), and against an earlier kernel's digests over many seeds — before its results count, on either machine.

6. Mutation and fault coverage

TEMPO's mutation catalogue (test/mutation/campaign.py) plants one representative fault at a time — 46 in all: off-by-one timestamp compares, inverted watcher and branch conditions, swapped operands and lanes, dropped guards and flags, wrong reset values, a bypassed synchronizer — and runs the project's test suites against each mutated copy. The first, module-level campaign (2026-09-16) killed 44 of the 45 non-equivalent mutants (98%): unit tests alone caught 93%, formal properties 100% of the modules they cover, but firmware, system and co-simulation each caught under a third (29%, 16%, 16%) because those suites simply don't run enough distinct programs to hit most mutated behaviour. The original co-simulation campaign, at 6 seeds, killed only 7 of the 46 mutants.

Run through lanes/mutation.py at lane-parallel scale instead — each mutant synthesized to its own netlist and run against roughly 4,094 random two-thread programs on the GPU — the co-simulation kill rate rose to 33 of the 45 mutants that actually change the netlist (one mutant, mem_lane1_src, mutates the generic RAM model that lanes/ replaces with the SRAM macro, so it can't be retested this way at all, hence 45 rather than 46). The number of programs needed to catch a killed mutant ranged from 17 of 4,094 up to every single one. The 12 survivors are what this style of comparison cannot see by construction, not undetected bugs: host activity during a run (the harness only pre-loads FIFOs and reads state by name, so it never exercises the mutants that only matter while the host is actively pushing or popping), writes to register r0 that no program reads back, reset-release timing, one mutant Yosys proves equivalent to the original, and two generator gaps — a byte load of a word the same program just wrote (rare, because loads read data at random addresses) and an instruction appearing between a TO-setting op and BTO/BNTO (the generator never emits that ordering).

A separate campaign (lanes/faults.py) plants 4,096 gate-level stuck-at faults — stuck-at-0 and stuck-at-1 on 2,048 randomly sampled gate outputs, one fault per 32-lane group, every group running the same programs as fault-free groups (131,200 lanes at once). With 256 programs per fault, 74.7% are detected on the generic-gate netlist and 75.8% on the sign-off netlist of the time, v0.2 (76.4% on v0.3-signoff and, field for field the same, on the netlist extracted from its GDS; section 8). About 900 of the detections are simply because the faulted program stops halting. The detection curve is nearly flat past 128 programs — 67% are already caught after just 32 — which suggests the remaining faults are out of this harness's reach entirely, rather than merely needing more random programs. Grouped by the registers their same-cycle fan-out reaches, most of the undetected faults on the generic run sit in the host port (431 of them — its read paths surface only on MISO, which no lane compares), the serializers (306), top-level glue registers (150), the timed-I/O unit (127) and the core itself (125).

7. What limits it now

After the Metal kernel's rework to 16 SIMD groups per word (section 5) and with fastgen already in place, the GPU itself was rarely the bottleneck: at one measured point (2026-09-21) its lane-cycles were only 18–20% useful, spending most of its time waiting on the workers to hand it more programs, with the main loop's own host-side work under 25% of an iteration and the rest one GPU step. On that same million-program sweep, the machine's 12 cores (8 performance, 4 efficiency) spent about 1,040 CPU-seconds in total: roughly 0.75 ms per program in the supply workers (about 0.34 ms of that in the ISS, measured slightly differently elsewhere in the docs as 0.30 ms; about 0.25 ms building the program — of which the stimulus schedule alone was 61% and the in-run reference spot-check was 16%, since cut to about 4% by moving from a 1-in-64 to a 1-in-256 sample), roughly 0.2 ms per program in classification, and a negligible 0.04 ms per program in the main process itself. The workers, not the GPU or the main loop, were setting the pace.

The C ISS, fastiss.c, changed that balance again: cutting a worker's ISS cost from about 0.30 to about 0.06 ms per program on the mini pushed the GPU's useful lane-cycle share from 34% up to 82%, and the project's own notes on it say plainly that "the netlist is near its limit again." In other words, the bottleneck has moved back and forth between the workers (building programs and running the reference model) and the GPU (running the netlist) several times over the course of this project, and each time one side got cheap enough, the other became the new limit. As of the 2026-09-22 source, the workers' own program-build cost — still dominated by the stimulus schedule — was the largest single remaining piece of a million-program sweep's CPU time. Since the fixes of 2026-09-25 a clean sweep also spends nothing on classification: there are no mismatches to classify.

8. Since publication: the model fixed, the layout checked

Added 2026-09-27; covers 2026-09-23 through 2026-09-26. The sections above describe the harness and its results as of 2026-09-22, with dated notes where a statement has changed.

The four findings, fixed in the reference model — and eight more

On 2026-09-24 tools/tempo/iss.py and its two lane ports, VecISS and fastiss.c, took the fixes of findings 15–18 (053b1a3), each the change the RTL's behaviour called for above: the pop takes effect a cycle later (15), each received bit is written at the RTL's fixed index and each transmitted bit at the live one (16), align_start starts the co-simulation with the pad synchronizers settled (17), and the clocked transmit counter wraps at 5 bits (18). Reviewing those fixes found more differences of the same kind, none of which a generated program reaches: the transmitter keeps running whatever tx_en says, which gates only the pins and a master's clock (19); one transmit word register serves every mode (20); a receive-only master's clock follows the registered arm (21); the slave clock's previous level is recorded every cycle (22); and out_pin values 16–31 wrap to a pin the RTL drives, now documented as reserved rather than modelled (23). An audit of every power-on default found the serializers starting MSB first where the RTL resets to LSB first (24, 2026-09-25); the CRC unit's corners gave three more (25: the polynomial aligned at the width in force when it is written, the CRCFEED count clamped to 1–8, the f bit ignored); and reviewing that fix gave the last (26: f = 1 on the 55 mnemonics defined only with f = 0 runs the op, and a unit op without a destination writes the unit's read data to rd).

All twelve were differences in the reference model, never the chip: the RTL did not change, ISA.md's changelog records the rules as v0.1.3 ("clarifications; hardware unchanged"), and 55 directed programs, the reproducers and their controls, give the RTL's values on the ISS, on the netlist and on the RTL under Icarus (tools/tempo/tests/cosim_findings.py, test/cosim/test_findings_probe.py). Every fix was also checked at the harness's own scale before it counted: fastiss 0 divergent on 35,000 generated programs and 15,000 random images and 0 differences on 1,400,000 harness seeds, VecISS 0 divergent, and the sweeps below.

A1, fixed in the generator

A1 was fixed where it lived, in test/cosim/gen.py and its C port, on 2026-09-25 (e7bc8f6): the generator now tracks each subroutine's own use of a timed output, and when a called one queued an output the main body did not already drain, it inserts rdtime r1; waitt r1, 64 in front of HALT. It draws no extra random numbers, so only the programs that needed the drain change (1.2% of one-thread and 3.6% of two-thread programs, and only by those two lines). With the findings and A1 fixed, the sweeps that used to end in explained mismatches now end in none:

Sweep (Mac mini)Fixed ISS, old generatorFixed ISS and generator
Benchmark million, 2,000,001–3,000,000, every verdict re-run on the CPU999,209 match; 791 A11,000,000 of 1,000,000 match
3,000,001–7,000,0003,055 A14,000,000 of 4,000,000 match
500,000 single-thread seeds, 100,001–600,000253 A1500,000 of 500,000 match

The fifteen seeds that used to show A1 match on the RTL under Icarus too. lanes/whatif.py now knows one cause, the base model: with nothing left to forgive, any mismatch is new, and the vector classifier's trusted shortcut (section 4) has no known cause to trust, so every mismatch would get a full CPU re-run. A clean million now takes 44.2 s on the mini, about 22,600 programs a second. That is not a new speed-up: the 55.6 s run in the chart still classified 1,120 mismatches, and this one has none to classify.

Programs tied to their sources

Preparing the re-run on the new sign-off netlist exposed a gap: a compiled netlist in lanes/build was reused whenever it existed, so a program built from one routed netlist could still be simulated after the file changed. Since 2026-09-24 (1a0eba5) every compiled program carries the SHA-256 of the files it was made from and of its own JSON, a stale one is rebuilt or refused, the Mac mini (which has no Yosys) accepts only programs whose record matches its tree, and every report names the netlist it simulated. The results above were not affected: the v0.2-signoff runs were reproduced exactly as the control of the re-run below.

The chip's current sign-off netlist

TEMPO's layout moved to v0.3-signoff on 2026-09-21 (30,736 gates and 2,832 flops once compiled). On 2026-09-24 the harness repeated M5 and M6 on it, with the v0.2-signoff netlist above as the control: every compared field and the pad-edge hash equal to the generic netlist's for 1,200,000 programs (seeds 1–100,000 with two threads and with one, and 2,000,001–3,000,000), with the same mismatching seeds and diffs as before; 3,131 of the 4,096 stuck-at faults detected (76.4%), against 3,106 (75.8%) on v0.2, within a standard error. The same six flops lose their names in layout on both (POUT[15:10]), and trace matching recovers them.

The layout built for submission, read back by RETRACE

Retracing Two Stars built RETRACE, an extractor that reads a GDS with nothing but its polygons, its labels and the cell library, and pointed it at TEMPO's sign-off GDS as an independent LVS. On 2026-09-26 lanes/ gained a third netlist from it (f57e311): lanes/retrace_netlist.py extracts the v0.3 GDS that goes to Tiny Tapeout, refuses it unless RETRACE's own electrical check passes (one driver per net, no undriven load, the supplies separate), and writes a netlist whose connectivity comes only from the GDS; the DEF supplies names alone, each instance by its placement and each net by the DEF net on its driver pin. Yosys proves that netlist equivalent to the v0.3-signoff netlist at all 3,046 compare points, and it compiles to the same lanes program, gate for gate. Run through the harness, every one of 1,200,000 programs gives the same readout digest on the generic, sign-off and GDS-extracted netlists, all matching the ISS; the classified benchmark million matches on every seed; and the 4,096 stuck-at faults give the same report on the extracted and sign-off netlists, field for field (3,131 detected, 915 of them because the faulted program stops halting, and 965 undetected). Planted faults show the checks can fail: a Metal2 bridge drawn into a copy of the GDS stops the generator (a net with two drivers), and a moved flop input in a copy of the netlist fails the equivalence check at exactly that flop.

Checked

Retracing Two Stars asked whether the layout matches the design; this piece asked whether the design's reference model matches the design. The two now meet: the GDS that goes to the foundry, read back by an extractor that knows nothing of how it was made, gives the same result as the netlist synthesized straight from the RTL, and as the reference model, on every one of the 1,200,000 programs run on it.

Limits and what we did not check

Open / caveat

This harness simulates the netlists functionally: two-valued, zero-delay, single clock. The sign-off netlist's actual timing is a separate signoff step's business, not this harness's; async resets would be modelled as synchronous if any were used (none are — every sign-off flop's reset pin is tied high, checked). A finished lane's compared state is read up to 255 cycles later on the GPU (63 on the CPU) rather than the instant it finishes; that is safe only because nothing compared changes after a lane is marked DONE, which was measured directly rather than assumed (see above), not because the harness watches every cycle. Most of the timings in this piece are single runs on a Mac mini also used for other work (lanes/README.md notes this can shift a benchmark); treat each before/after pair as a real but noisy reading, not an averaged result.

Every confirmed mismatch cause found across every sweep run so far sits in the ISS or the generator, never in the RTL: the netlist lanes agree with the RTL under Icarus on all 28 seeds re-run (20 from the two-thread run, 8 from the single-thread run). That is a strong result for the seeds actually run, not a proof that no RTL divergence exists outside what tens of millions of random programs have hit so far. It still holds after the fixes of 2026-09-24/25: all twelve findings and A1 were on the model or generator side, and the finding seeds, the fifteen former A1 seeds and the 55 directed programs all match the RTL under Icarus. But eight of the twelve (19–26), and the transmit half of 16, are corners no generated program reaches, so a clean sweep says nothing about them; what guards them is the directed suite, run against the ISS in the tools tests and against the RTL by test/cosim/test_findings_probe.py. Two known generator gaps (the byte-load and TO-ordering cases above) mean those specific code paths in the RTL have essentially never been exercised by this generator at all, at any scale. The default boot sequence also runs SPI faster than the host protocol's own documented limit — SCK at clk/2 against HOST.md's stated clk/6 ceiling for write-only traffic, checked functionally rather than against the letter of the timing spec (--half 3 gives a rate inside the documented limit).

STATUS.md's own next open item for this work is host activity during a run: nothing here models the host pushing to or popping from the FIFOs, or reading CSRs, while a program executes, so the blocking FIFO operations never actually block in any of these sweeps — only the pre-load-then-drain pattern is exercised. The 12 surviving mutants, of the 45 that change the netlist, are what this co-simulation cannot see by construction: host activity during a run (the host only pre-loads, and the state is read by name), writes to r0 that no program reads back, reset-release timing, one proven-equivalent mutant, and two generator gaps (docs/spec/VERIFICATION.md §4b). Most of the undetected stuck-at faults sit in the host port, whose read paths show only on MISO, which no lane compares, then the serializers and the top-level glue registers; the detection curve is nearly flat after 128 programs, so the rest is out of reach of this harness rather than of more programs (same section).

Every citation above is a repository path, line number or commit hash in the TEMPO repository, given as plain text until the repository is public.

What this project developed, and where it applies

Most of what follows is a new combination of established techniques — bit-slicing, bulk mutation and fault campaigns, and fingerprint-gated native ports are none of them new ideas in isolation. No prior-art search was done, so nothing here should be read as a novelty or patentability claim; it is a record of what this project built and where else it might be useful.

#Technique or findingCode pathWhat is new hereFuture applications
1Bit-sliced lane-parallel gate simulation: thousands of independent random programs against the same synthesized netlist at once, on CPU or GPUlanes/sim_cpu.py, sim_mlx.pyscales an existing per-program co-simulation harness to lane-parallel scale without changing what it comparesany cycle-accurate netlist verification effort bottlenecked on wall-clock seeds per hour
2Fingerprint-gated native ports of a Python reference model, unavailable while the checkout differs from what they were verified againstlanes/fastgen.py, fastiss.pya performance port that refuses to silently run stale after its reference changes, closing a near-miss found by direct experimentany performance port of a model used elsewhere as ground truth
3Verify-then-trust classification: promoting a cheap approximation (a GPU-harvested vector) to production only after proving it identical to the expensive path at real scalelanes/whatif.py0 disagreements demonstrated on 7,549 real mismatches before the cheap path became the default, with a permanent 1-in-16 spot check kept afterward (since 2026-09-25 no known cause is left for the shortcut to trust)any pipeline stage with an expensive "ground truth" recomputation and a cheaper proxy for it
4A GPU kernel generated directly from a gate-level netlist, partitioned into SIMD-group blocks by shared logic coneslanes/netlist.py, sim_mlx.pya Metal kernel compiled from Yosys JSON rather than hand-written, checked bit-identical to a CPU evaluator of the same netlistfast randomized or property-based testing of any small-to-medium ASIC's gate-level model
5Mutation and fault campaigns run at co-simulation scale instead of a handful of directed seedslanes/mutation.py, faults.pythousands of programs per mutant or fault instead of single digits, turning "did we test this?" into a measured detection rateany RTL-plus-reference-model verification project with spare compute to spend on breadth
6A functional check of the layout built for submission: the GDS read back by an independent extractor and run through the same harness as the generic-gate and signoff netlists (added 2026-09-26)lanes/retrace_netlist.pyconnectivity from the GDS alone, refused unless the extractor's electrical check passes; equivalent at every compare point and identical on 1,200,000 programsany tapeout with an independent extractor and a fast functional harness: closes the loop from the file sent to the foundry back to the RTL

Lessons that transfer

  1. A cheap sampling check can hide exactly the failure it exists to catch. An early fastgen build's 1-in-64 spot check flagged only 6 of 200 programs that a single generator edit silently made wrong; the fix was tying the fast path's availability to a fingerprint of its reference, not a bigger sample.
  2. Batching for speed changes what "identical" has to mean, and that has to be reproven, not assumed. Both batched classification and vector-mode classification were run at real scale (1,095 and then 7,549 real mismatches) and compared word for word against the slow path before either became the default; a demonstration of a few dozen mismatches could easily have found zero disagreements and still hidden a real, rarer one.
  3. A kernel that compiles correctly on one GPU is a claim about that specific compiler, not about the source. The M4 Pro's shader compiler miscompiled a form of the Metal kernel the M5 Max compiled correctly; the house rule that came out of it is to test every kernel change on both machines, not to assume a portable-looking construct is actually portable.
  4. An operating-system default can silently steal a measured speed-up. zsh backgrounds jobs at a lower scheduling priority by default (its BG_NICE option), which starved a sweep of CPU on a busy machine and looked exactly like a code regression until someone checked top.
  5. Every entry point should distrust its own arguments, even in hand-written, in-process C. An unchecked out-of-range write in an early version of fastiss.c moved one lane's program counter into unrelated lane state without any entry point reporting an error; the fix was header and argument validation on every call, not only at the public API boundary.
  6. Reviewing a fix is where the next bug is. The four findings the sweeps surfaced led to twelve (added 2026-09-27): reviews of the fixes found six more (19–23 and 26) and audits of the power-on defaults and the CRC unit found two (24, 25), none of them reachable by a generated program. The same fact sets a limit on what a clean sweep proves: those eight are guarded by 55 directed programs, not by random seeds.

How this was built

The lanes/ engineering described above (2026-09-18 through 2026-09-22) was run by Claude Opus 5 (the co-author on every lanes/ commit) orchestrating a series of subagents, several working in separate branches as implementers with a separate agent reviewing each substantial change adversarially before merge — three independent reviews for the vectorised ISS (M2), a six-lens review each for the C program generator and the C instruction-set simulator, and two rounds of thirteen and then ten reviewing agents (23 in total) for the streamed-sweep and batched-classification work, which found eleven liveness and reporting defects (a shared pipe that froze every worker if it died mid-send, orphaned worker processes, one failing classification chunk that could abort an entire sweep) and zero differences in any recorded result. Every reviewed change either passed unchanged or was fixed and re-verified before it was allowed to affect a reported number.

This write-up itself is, per the session's own working notes (not something the TEMPO repository records), the second stage of a two-stage process. A research-and-ledger stage first had Sonnet 5 agents extract every checkable figure from lanes/README.md, docs/spec/VERIFICATION.md and docs/STATUS.md, then had separate Sonnet 5 "skeptics" adversarially validate each one against the repository's own docs and commit history, the orchestrator's session reporting, and the project's Hindsight memory bank — the three ledgers this write-up was written from. A handful of figures the skeptics could not independently confirm (an uncorroborated total from one adversarial review's chat summary; a couple of A/B timing pairs that exist only in the session transcript, not in any committed document) were marked unverifiable and are described here qualitatively rather than as numbers; a few others were corrected outright (a stray-process-inflated timing figure; an arithmetic total that didn't add up). The write-up itself then had every figure and narrative claim re-checked by further skeptic passes against the same sources, and the corrections they found were applied.

The work since publication (2026-09-23 through 2026-09-26, section 8) was run the same way by Claude Opus 5.5, the co-author on those commits, with each fix reviewed adversarially before merge; per the session's working notes (not something the repository records), from the A1 fix on, its subagents ran on Sonnet 5 while Opus 5.5 orchestrated and assembled. The 2026-09-27 revision of this page was made the way the page was: Sonnet 5 agents built ledgers of every change since 2026-09-22 and audited the page, passage by passage, against the current repository; separate Sonnet 5 skeptics validated each ledger; Opus 5.5 wrote the revision; and further skeptics checked every changed statement.

Stack: Python (numpy for the CPU evaluator and the vectorised ISS), C (the two native ports, built with the system compiler on first use and cached), Metal via MLX for the GPU kernel, cocotb and Icarus Verilog for the pre-existing RTL co-simulation this work never touches, Yosys for netlist synthesis.

Reproduce

The repository is private while the Tiny Tapeout submission is pending, so a reader outside the project cannot run these commands without it — they are given here verbatim, as what actually produced the numbers above, not a paraphrase.

source scripts/env.sh
python -m lanes.run --seeds 1-10000 --lanes 4096                                # CPU (numpy)
python -m lanes.run --seeds 1-100000 --lanes 16384 --backend mlx --workers 16   # GPU (M5 Max; 11 workers on the mini)
python -m lanes.run ... --netlist signoff                                       # the signoff netlist
python -m lanes.retrace_netlist GDS DEF                                         # under RETRACE's Python: the GDS-extracted netlist
python -m lanes.run ... --netlist retrace                                       # the GDS built for submission, as RETRACE extracts it
python -m lanes.whatif --json run.json                                          # classify its mismatches
python -m lanes.sweep --start 2000001 --blocks 10 --workers 10                  # 1M seeds, classified (mini: ~4 min)
python -m lanes.fleet --start 3000001 --blocks 40                               # 4M seeds on this Mac and the mini (~7 min)
python -m lanes.trace --seed 4656 --from 380 --to 400 --signals u_top.pout_q    # one seed, side by side
lanes/remote.sh sync && lanes/remote.sh run m3 --seeds 1-10000 --lanes 4096   # on the mini
python -m pytest lanes/tests                                                    # ~6 min
python -m lanes.fastgen --check SEEDS                                           # fastgen vs. the reference generator
python -m lanes.fastiss --lockstep SEEDS --harness SEEDS                        # fastiss vs. iss.py and VecISS

Details: lanes/README.md, docs/spec/VERIFICATION.md sections 3, 4b and 8, docs/STATUS.md, docs/spec/CHANGELOG.md.

Revision log

This page is revised in place when the work it describes changes. A statement that was true when written stays where it is history, with a dated note beside it; one that is no longer true is corrected; and every revision is listed here.

DateRevision
2026-09-22First published.
2026-09-22The hero's small bar chart replaced by the full-width before-and-after chart of the speed-ups; every value re-checked against the validated ledgers.
2026-09-27Revised for the work of 2026-09-23 through 2026-09-26. Findings 15–18 fixed in the reference model and eight more found (seven fixed, one documented); A1 fixed in the generator, so the sweeps now end with no mismatches; compiled programs tied to their sources; the harness run on the v0.3-signoff netlist and on the GDS built for submission, as RETRACE extracts it. New section 8 and one lesson; dated notes where earlier statements changed; the description, hero, facts, dateline, tables, Limits, How this was built, Reproduce, footer and listing blurb updated to match.