Fixed-Point Streaming Attention Engine
SystemVerilog attention accelerator, verified to sky130 gate level
View repositoryDatapath
Q1.6 activations, 8-bit
Head dim
D = 16 · 1/sqrt(D) is a shift
Sequence
N ≤ 64 · N_MAX 256
Flow
Yosys → sky130 → OpenSTA
01Overview
A streaming attention engine in synthesizable SystemVerilog. A tiled Q·Kᵀ matmul in the lineage of the TPU paper feeds an online softmax in the lineage of the FlashAttention paper, integrated end to end behind BRAM-inferable memories so the design maps to real block RAM rather than inferred flop arrays.
The interesting part is not the RTL, it is the evidence. Every result is backed by a row in an append-only ledger that the build writes on success, and the repository refuses to make a hardware claim it cannot support: nothing is running on an FPGA and nothing is fabricated. Every timing and power figure below is a tool estimate at a single sky130 corner.
02Problem Statement
Attention is memory-bound and numerically awkward in fixed point. A naive implementation materializes the full score matrix and then normalizes it, which costs both storage proportional to sequence length and a second pass over the data.
The online-softmax formulation avoids that by carrying a running maximum and a running denominator and rescaling the accumulator as new scores arrive, so scores stream through in one pass. Doing that in fixed point means every width, rounding site, and saturation site has to be derived and then proven, not guessed.
03Architecture
Numeric contract: activations are Q1.6 in 8 bits, the Q·Kᵀ accumulator is Q11.12 in 24 bits, scores are Q5.10 in 16 bits, softmax weights are UQ1.15, the denominator accumulator is UQ9.15 in 24 bits, and the weighted-V accumulator is Q10.21 in 32 bits. Each width is derived from the range of the expression it holds rather than rounded up to a convenient size, and a spec document is the normative source of truth: where the code and the spec disagree, the code is the bug.
Head dimension D is fixed at 16 so that the 1/√D score scale is an exact right shift by 2 and the score path needs no scaling multiplier. The exponential is a direct 1024-entry lookup table in UQ1.15, generated from a normative hex interchange file that both golden models read, so the hardware and the models cannot silently disagree about the table.
Modules: mac_unit is the multiply-accumulate primitive, matmul_tile is the tiled dot-product engine, online_softmax carries the running maximum and denominator with a parameterizable ROM pipeline stage, and attention_top integrates them behind BRAM-pattern memories.
Verification is a dual golden model. A Python implementation is normative and an independent C++ reimplementation exists to catch a bug that lives in one author's head, and a cross-check proves the two are bit-identical before either is used as a reference for the RTL.
04Technical Challenges
Proving the golden model before trusting it
A reference model is only useful if it is right. The Python model is normative and the C++ model is an independent reimplementation; a cross-check proves the two produce bit-identical output across the test space, and the exponential lookup table is emitted to a shared hex file that both read. Only after that gate passes does either model get used to judge the RTL.
Deriving every fixed-point width
Each accumulator width is derived from the range of the expression it holds, including the exact saturation edges. The score path is provably free of saturation at D = 16, and the models assert the derived bounds at runtime so a width mistake fails loudly rather than silently clipping.
Closing functional coverage rather than declaring it closed
Phase 3 closed 52 of 52 reachable coverage bins and added an exact-max formal property for the running maximum, so the corner the coverage model cares about most is proven rather than sampled.
The timing limiter is the softmax, and it is documented as such
online_softmax is the design's critical path. In OpenSTA at the sky130 typical corner it closes at 38.5 MHz naive and 76.9 MHz with the ROM pipeline stage; neither configuration meets the 10 ns target period, while mac_unit and matmul_tile do. That gap is recorded rather than rounded away.
05Implementation Details
Per-module verification gate
Every module passes the same gate before it is considered done: Verilator lint, cocotb simulation against the golden model, a coverage threshold, a latch-free synthesis check, and a bounded formal proof in SymbiYosys. The gate appends a row to the evidence ledger on success, so a claim without a row is not a claim.
sky130 synthesis, timing, and gate-level simulation
Yosys synthesizes to a sky130 gate-level netlist, OpenSTA reports timing at the typical corner, and both the naive and pipelined netlists are re-simulated at gate level with spec-derived vectors, passing with zero errors. Gate-level simulation is what catches the synthesis-versus-simulation mismatches that RTL testing cannot.
Switching-activity power proxy
Toggle counts are extracted from the two gate-level VCD traces and fed through an OpenSTA power script to compare the naive and pipelined configurations. It is a proxy, calibrated and documented with its biases, not a measurement.
A build that refuses unbacked claims
The technical guide is audited mechanically: a build target fails if a hardware or silicon claim appears without a supporting evidence row. Phase 6 (FPGA) and Phase 7 (silicon) are marked pending-hardware and stay that way until a bring-up log or a measured clock sweep exists.
06Key Engineering Decisions
Online softmax over a two-pass normalization
Carrying a running maximum and denominator and rescaling the accumulator lets scores stream through in a single pass, which removes the need to store the full score matrix. It costs a rescale multiply per step and a more delicate numeric argument, which is the trade this project was built to make and then prove.
D fixed at 16 rather than parameterized
Fixing the head dimension at 16 makes 1/√D an exact shift and removes a multiplier from the score path. It is documented as a spec decision rather than a parameter, because changing it moves saturation boundaries: at D = 64 a single all-extreme input pattern lands exactly on the score saturation edge.
A direct lookup table for exp()
A 1024-entry UQ1.15 table indexed by 10 bits of the clamped score keeps the exponential exact-by-construction against the model, and makes the approximation error a documented table property rather than an emergent one. The score quantization sits an order below the table index error, so score width is deliberately not the accuracy bottleneck.
Stating the sandbox/silicon wall explicitly
RTL correctness, coverage, formal proof, synthesis, timing, gate-level simulation, and estimated power are all provable in a sandbox and are claimed. FPGA and silicon results are not, so they are marked pending-hardware. Saying so plainly is more useful to a reader than a claim that does not survive scrutiny.
07Future Improvements
- Bring the design up on an FPGA and replace the pending-hardware rows with a real bring-up log and a measured clock sweep.
- Close the timing gap on online_softmax so the pipelined configuration meets the 10 ns target period rather than 76.9 MHz.
- Extend the benchmark beyond cycle counts once a real clock frequency is measured rather than estimated.
- Push the design through a physical-design flow to GDS as the Phase 7 guide describes.
08Media & Documentation
Visual documentation for this project. Placeholders below are reserved for assets exported from the verification and synthesis flow.
Open to opportunities
Looking for a Summer 2027 internship.
If you're hiring for embedded, firmware, or hardware roles, I'd be glad to talk through my projects and how I work. The fastest way to reach me is email.
