Verification
Every claim on this site is checked by a test in the repository. The golden model is the reference: a Python program with the same integer formats, which the RTL is compared against on every run.
What is checked
| Layer | What it checks | How it runs |
|---|---|---|
| Unit blocks | Each arithmetic block against the golden model, including exhaustive sweeps of the exp2 and reciprocal inputs, and the DMA burst timing cycle by cycle. | bash sim/run_unit.sh (cocotb with Verilator) |
| Tile core | One tile against the golden trace, including causal masking and multi-group blocks. | sim/test_attn_tile.py |
| Engine, end to end | Output bit for bit; HBM read and write bytes; tile count; K/V loads; busy cycles against the closed-form model. Every sequence length 4 to 32, causal and not, all block sizes, both schedules, overlap on and off, and random HBM latency. Random seeds on top. | SEEDS=200 bash sim/run_e2e.sh |
| Golden model | Quantization, exp2 and reciprocal, both schedules against float attention, traffic formulas, presets, and that the committed LUT table matches its generator. | pytest sim/golden |
| Lint | Verilator with all warnings on, for every module and the full design. | bash sim/lint.sh |
| WebAssembly | The compiled module, on golden fixtures for each schedule: output, bytes, tiles, cycles, the last tile's state, probabilities, and the K/V buffer in use. | node wasm/test.mjs |
| Web app | Quantization and tile order against the shared fixtures, the visualizer and each docs page in a real browser, at phone width and in both colour schemes. | pnpm test, pnpm test:e2e |
All of these run in GitHub Actions on every pull request. The workflows are rtl.yml, wasm.yml and web.yml.
Output error
Maximum error of the engine's output against float attention, per preset, in float units. These numbers come from the golden model, which the RTL matches bit for bit.
| Preset | N | Causal | Max error |
|---|---|---|---|
| toy_sentence | 12 | yes | 0.0049 |
| previous_token | 16 | yes | 0.0105 |
| attention_sink | 16 | yes | 0.0254 |
| uniform | 16 | no | 0.0028 |
| self | 16 | no | 0.0260 |
| random | 16 | no | 0.0163 |
Accuracy study
The recorded study (sim/golden/study_results_1000seeds.txt), in V units (one int8 step of V). dp is the datapath
error on the INT8 inputs. tot is the error against float attention on the original inputs.
| N | Causal | dp max | dp mean | tot max | tot mean |
|---|---|---|---|---|---|
| 4 | no | 0.624 | 0.0665 | 6.431 | 0.3839 |
| 4 | yes | 0.591 | 0.0418 | 8.085 | 0.3209 |
| 8 | no | 0.849 | 0.0640 | 10.942 | 0.4172 |
| 8 | yes | 0.849 | 0.0486 | 8.855 | 0.3728 |
| 16 | no | 1.061 | 0.0661 | 9.016 | 0.4541 |
| 16 | yes | 0.981 | 0.0529 | 9.383 | 0.4065 |
| 32 | no | 1.260 | 0.0691 | 11.904 | 0.4722 |
| 32 | yes | 1.023 | 0.0563 | 13.076 | 0.4403 |
Cycles at N = 32
Busy cycles at N = 32, non-causal, with 10 cycles of HBM latency. The sequential FLASH rows match the closed-form schedule exactly. The overlap and NAIVE rows are pinned baselines from the RTL, and the test fails if they change.
| Configuration | Busy cycles |
|---|---|
| FLASH, Q block 4 rows, no overlap | 4113 |
| FLASH, Q block 4 rows, overlap | 2937 |
| FLASH, Q block 16 rows, no overlap | 2133 |
| FLASH, Q block 16 rows, overlap | 1657 |
| NAIVE | 10961 |
FPGA
The engine behind a UART synthesizes for an ECP5 (LFE5U-85F) with no latches. The UART protocol is simulated: the
results read back over the serial line match the golden model, and the cycle and byte counts match the models
(bash sim/run_fpga.sh). Synthesis runs in CI (fpga.yml).
Not verified yet
- Timing at the board clock. The fmax estimate is 11.5 MHz against 25 MHz, and the estimate has no pin constraints.
- Real hardware. The board has not been used. Everything else runs in simulation or in WebAssembly.