Mirage: a 6-layer, 512-wide INT8
transformer encoder
on a $99 FPGA
An autonomous loop was handed a 19-task plan for this design and closed all 19, finding four real defects in the RTL on the way — but every claim it made was a projection. Then it went on a board: 2,352 jobs replayed on the fabric, 61,632 values matched byte-for-byte, zero mismatched, with a negative control proving the check could fail.
=== Mirage vector replay === ID : 0x4d495247 OK <- "MIRG" out of the AXI4-Lite ID register cmd tape : 0x00400000 res tape : 0x00600000 board verdict: VECTOR REPLAY PASS -- silicon matches the reference bit-exactly. 5. BIT-EXACT RECHECK (host-side, independent of the board's own) 61,632 values compared across 138 tensors PASS: every byte the board produced matches the model --- and with one activation byte flipped, 05 -> 06 --- 112 MISMATCHES -- the silicon and the model differ NEGATIVE CONTROL PASSED -- one flipped byte was caught.
01 What was attempted
A deliberately unforgiving target, chosen so that a mistake could not hide.
The subject is Mirage, an open-source, ultra-small FPGA transformer accelerator for EN→AR translation. What is documented here is not the accelerator but the experiment wrapped around it: a planner–designer–verifier loop given the 19 tasks, with every one gated on evidence rather than on the agent's own confidence.
The part is a Digilent Cora Z7-07S carrying an XC7Z007S: 14,400 LUTs, 66 DSP48E1 slices, 50 RAMB36 blocks. The spec demanded end-to-end INT8, no floating-point, 30% slack left over. A part this small leaves no room to be sloppy — which is the point.
Most agent demos are single-shot: one prompt, one file, one plausible answer. A chip is the opposite — a long chain of decisions where an error in week three quietly poisons week nine. The question was whether a loop could hold a multi-week engineering program together.
Board map of the Cora Z7-07S — press to open
02 The harness that built it
The agent occupies exactly one box. The only path from "I think I'm done" to "task closed" reads the disk, not the transcript.
An agent will declare victory on a vague instruction, so the first step had
nothing to do with hardware. 6 phases, 19 tasks, each with a numeric acceptance
criterion, the artifacts it must produce, and a risk note. "Verify the softmax" is not a
task. smx_core passes end-to-end SMX test for 8 heads × 1 layer × 4 tokens
is, because it can fail.
The model is a swappable part. The 19-task run was Kimi K2; the v2 rebuild, the board bring-up and this write-up are Claude; a little of the early scaffolding was Codex. Across the whole project that is roughly 60 / 30 / 10 Claude / Kimi / Codex — an operator's estimate, not a measured split. The harness never asked which: it hands out one brief at a time and reads the disk to decide whether a task closed. That is the point of gating on artifacts rather than on a transcript — the gate does not care who wrote the file.
The agent harness, end to end — press to open
complete
is the one that matters: it is the reason nothing on this page is the agent's own
opinion of its work.
The gate, in two commands
complete exits 2 and refuses to close a task unless the
artifacts the plan declared actually exist on disk. There is a --force
flag, and it is human-only.
# 1. Ask the harness what's next — never the agent's memory $ python -m workflow.cli next p1/w3 taylor_exp_approx # 2. Try to close a task with no artifacts on disk $ python -m workflow.cli complete p1/w3 refusing: declared artifact missing — reports/w3-exp-error-histogram.md $ echo $? 2
03 What the agent found
Write the bit-accurate model from the spec first, then audit the RTL against it. That ordering is the whole method — the model has no knowledge of how the RTL cheats.
This is where the project stopped being a workflow demo and became engineering. The audits kept finding real defects, and four of them were the kind a human reviewer skims past:
| Week | Module | What the golden model exposed | Resolution |
|---|---|---|---|
| W3 | Taylor exp | The 3rd-order core was supposed to hold under 1% relative error. It met that bar at exactly one point — x = 0 — and 64 of 64 sampled points came back 100% or more off, because an implicit clamp of 0 swallowed the input. Root cause: Q-format. |
Move to Q9 (scale 512), clamp |x| ≤ 0.5352. Max relative error 0.9683%. |
| W5 | Softmax e2e | End-to-end attention came back 87–107 int8 LSB from golden. The exp input scaling was wrong by a factor of about 218. | Shift z << 6, range-reduced exp, no divider. Worst case 2.99 LSB, RMS 0.52, exactly 0.00 one-hot. |
| W7 | FFN | Failed all 10 random trials at 100% relative error — and ghdl confirmed it could not even compile: no declaration for "mac_array". Its weight BRAMs alone came to ~278 KB against a device total of ~225 KB. |
Not a fix — a redesign spec. 16-bit activations, per-layer power-of-two scales. |
| W9 | Layer cascade | With int8 inter-stage activations, drift blew past 1 LN unit by layer 1. Softmax is chaotic under coarse quantisation: a small perturbation does not stay small. | int16 between layers, int8 weights kept. 3-layer chain: worst drift 0.0062 LN units, RMS 0.0019. |
The release gate is one command
Nine bit-accurate golden checks with numeric criteria, plus a self-checking
ghdl bench. This is the independent re-run recorded for the v1.0 freeze:
$ bash outputs/run_regression.sh == model-level golden checks == PASS taylor_exp_model.py PASS smx_e2e_model.py (2.99 < 4.0) PASS ffn_model.py PASS encoder_e2e_model.py (0.0296 < 0.05) PASS multilayer_e2e_model.py (0.0047 < 0.01) PASS greedy_decode_model.py PASS bidirectional_demo.py PASS beam_search_model.py (13 >= 13) PASS robustness_model.py == RTL (ghdl) checks == PASS ghdl:gemm_latency_tb == REGRESSION: ALL GREEN exit=0
Fault injection went further: saturated inputs, single-bit upsets, patterns
built to maximise accumulator growth. Every scenario passed — but under an all-max input
the FFN hidden accumulator can hit 4.0× int32 overflow. That
became outputs/rc2_hardening.vhd, drafted and ghdl-analysed,
not a footnote.
04 The three domains
Weights and activations go down; computed tensors come back up. The fabric never sees a sentence.
"An FPGA that translates" is the wrong model. The fabric runs a transformer encoder's matmul chain — about 99.8% of the arithmetic — and nothing else. The ARM is a courier; an x86 host stitches the layers and runs the decoder. Being exact about that split is what makes this page checkable.
The three domains: host, ARM, fabric — press to open
The split, to scale
Drawn proportionally, the host's share of the arithmetic is the amber sliver.
On the fabric
99.8%Every multiply-accumulate in all six encoder layers — including the 512→2048→512 FFN, 91% of a layer by itself.
On the host
~0.2%FP.layer_norm(x1 + yf, …) — cheap in FLOPs, indispensable to the result, and it runs between every pass.
05 Inside the fabric
Every multiply forced into a DSP, every array into a BRAM. The memory budget is the architecture.
Inside the fabric, lane by lane — press to open
build_cora/mirage_cora_wrapper.bit, and it is the one the recording below
loads.06 How the Arabic is produced
The part most easily overclaimed. Follow which box the tokens come out of.
Where the Arabic tokens come from — press to open
enc_hw is the
host's own computation, so the decode check runs on the model's state. The
board's 61,632 values match it bit-exactly, so decoding the board's numbers must give the
same Arabic — but "must" is an inference, not a demonstration.07 Bring-up, on one cable
One unbroken session against the board. Nothing was re-run between clips.
Eight clips, one take, in order. Long waits are compressed, but the elapsed clock counts true seconds, so a cut shows as the clock jumping, never as time that did not happen. The terminal is 145 columns: go full-screen, landscape on a phone.
./demo.sh --check./demo.sh./demo.sh --negative
demo.sh drives for you.JTAG and console, one cable
00:10Both channels into the board arrive on one micro-USB.
/dev/ttyUSB1 has a tty node, and that is correct — openocd claims interface 0
over libusb, so the kernel drops the other. Nothing else may hold the port: a tty gives
each byte to one reader.
- FT2232H
- /dev/ttyUSB1
uname -sr; echo; lsusb -d 0403:6010ls -l /dev/ttyUSB*fuser -v /dev/ttyUSB1 2>&1 || echo 'no reader holds /dev/ttyUSB1'
Scanning the JTAG chain
00:07ID codes burned into the die, not printed by the host.
0x13723093 is the XC7Z007S fabric, 0x4ba00477 the ARM core
beside it. Neither can be faked from this machine.
- openocd
- scan_chain
openocd -f cora.cfg -c 'init' -c 'scan_chain' -c 'targets' -c 'shutdown' 2>&1 | grep -vE 'Warn|deprecated|srst|Info : (clock|Listening|starting)'
grep only quiets openocd’s startup noise; drop it and the ID codes read the same.Opening the console at 115200
00:10115200 8N1 — chosen by the block design, not by this terminal.
PCW_UART0_BAUD_RATE in the XSA and the host has
to match it. picocom then attaches to a board that says nothing: no boot flash,
no SD card, nothing running on the processor yet. Code arrives over JTAG.
- 115200 8N1
- picocom
stty -F /dev/ttyUSB1 115200 raw -echo -crtscts; stty -F /dev/ttyUSB1 -a | head -3picocom -b 115200 /dev/ttyUSB1
ctrl-a ctrl-x detaches when stage 05 needs the port.Bitstream load and smoke test
00:11Bitstream and smoke test, both over the same JTAG cable.
0x4d495247 is “MIRG” out of the AXI4-Lite ID register. The loopback
returns 0 of 64 bytes wrong and the gemm the expected 64 in all 32 lanes.
That output came out of the chip, not out of this machine — it is the
mac_array from section 05 answering for the first time.
- 0x4d495247
- 32 lanes
make load
load is openocd: halt, pld load the bitstream, load_image the smoke test, resume. Replies come back on the console from stage 03.08 Why the tape was taken apart
64.3 MB against an on-chip ceiling of ~64 KB per tape. Counting it changed the problem.
The tape, and the 98.6% that never changes — press to open
Splitting the recorded run
00:1064.3 MB of recorded simulator run, cut in two.
- 1,152 window loads
- 786,432 rows
./ddr_replay.sh ../../../sim/xlate_cmd.txt ../../../sim/xlate_res.txt
Loading 25 MB over JTAG
00:1125,165,824 bytes of weights, at about 132 KiB/s.
main() so ps7_init
finishes and DDR is initialised before anything is written to it. 25,165,824 bytes of
weights go to 0x01000000, the command stream to 0x00400000, at
about 132 KiB/s. The elapsed clock runs 00:32 to 04:18 in eleven seconds of video — that
is the cable, not the array.
- 132 KiB/s
- 0x01000000
09 Chain of custody
Four representations of one computation, each required to agree with the last at zero tolerance.
Chain of custody: float32 to silicon — press to open
Comparing 61,632 values on chip
00:17The board grades itself; the host only reads the tally.
VECTOR REPLAY PASS. The rightmost arrow in the diagram above,
happening.
- 2,352 jobs
- 61,632 values
Negative control: one byte flipped
00:17One activation byte flipped, 05 to 06 — 112 mismatches.
05 to
06: 112 of 61,632 values wrong, and it prints VECTOR REPLAY FAIL.
The pass is a result, not a default. Note what does not happen — the Arabic still
comes out right. An int8 activation off by one almost never moves an argmax, which is
exactly why the byte comparison is the verdict and the translation only the presentation.
- 05 → 06
- 112 wrong
grep -E 'records|values|VECTOR REPLAY' build/ddr_console.negctl-2026-08-13.log | sed 's/\r$//'
./demo.sh --negative; the date in the name is the run’s.0x4d495247). Its GEMM passes a known-answer test. It ran 2,352
jobs and returned 61,632 values over MMIO matching simulation exactly — and one changed
input byte breaks that match in 112 places.Nothing was re-recorded and nothing dropped between the clips. The take is here in one piece — mirage-board-demo.mp4 · 1:34 · 4.9 MB — the same eight clips this page plays a stage at a time.
10 Projection vs measurement
The honest way to read this project is to ask which claims moved tier, and which did not.
The evidence ladder, five rungs — press to open
What the v1.0 freeze claimed, and where each claim stands now
| Claim at v1.0 | Then | Now |
|---|---|---|
| Bitstream exists | Not fabricated — human + Vivado step | build_cora/mirage_cora_wrapper.bit, timing closed 2026-08-01 |
| Board bring-up | Planned future work | Run, recorded, and reproducible from demo.sh |
| DSP budget | 65 / 66 · 98% pre-synthesis — fails the <90% bar | 34 / 66 · 51.5% measured in context |
| BRAM budget | ≈84% projected | 36.5 / 50 · 73% measured |
| Timing at clock | Assumed, no Vivado run | WNS +0.214 ns · 0 of 8,803 paths failing |
| Datapath correctness | Bit-accurate Python models only | 61,632 values from silicon, 0 mismatched, negative control caught |
| Latency ≈16.74 ms | Cycle model @ 200 MHz | Unchanged — still a cycle model |
| ≈360 tok/s, ≈1,700× CPU | Estimate vs unoptimised Python | Unchanged — and the project's own report narrows it to 10–20× against a competent int8 baseline |
| Translation quality | Toy-scale random weights, no BLEU | Real MarianMT weights now drive the tape; still no BLEU evaluation |
11 What is not proven
Stated plainly, because a page that only lists wins is not evidence of anything.
Speed
This run says nothing about it. Weights reach the board over JTAG at ~132 KiB/s, which makes the whole session bandwidth-bound by a wide margin. The wall clock describes the cable.
Translation quality
The tape comes from real MarianMT weights and the decode is token-identical to the float32 reference, but no BLEU evaluation exists. "Correct Arabic on one word" is not a quality claim.
The last decode hop
enc_hw is the host's own
computation, so the check decodes the model's encoder state. The board's values
match it bit-exactly, so the same Arabic must follow — but that is an inference, not a
demonstration.
Power
No rail was ever measured. The 5–10 mJ/sentence figure is a projection and has not moved.
Sustained operation
One sentence, replayed twice. Nothing here speaks to thermals, long runs, or a second sentence without a reload.
The FFN overflow
The adversarial all-max input that reaches
4.0× int32 overflow is a modelled result. rc2_hardening.vhd is drafted and
analysed, not integrated upstream.
12 Where it goes next
In rough order of impact, now that the biggest gap on the old page is closed.
| Next | Why it is the next one |
|---|---|
| Load weights over something other than JTAG | SD or Ethernet turns a 3-minute load into a fraction of a second, and it is the only thing standing between this run and a timing measurement worth reporting. |
| DDR bandwidth tuning | After the optimisation pass the pipeline is memory-bound, not compute-bound — crossover at roughly 192 MB/s against 100 MB/s of streaming bandwidth. That is where the next real speedup lives. |
| Decode from the board's own state | Closes the one inference left in section 06 and turns "must give the same Arabic" into a demonstration. |
| int4 FFN weight compression | Relieves BRAM pressure and stream time at once — the FFN is 91% of a layer. |
| Integrate RC2 saturating readback | Plus ECC or scrubbing for multi-bit upsets. Single-bit upsets already absorb at the noise floor, at most 0.051 LN drift. |
| Real BLEU | Quantise the trained checkpoints through the model scripts and run a proper evaluation, so translation quality stops being an open box. |