3. Evidence and Projections🔗

Every accelerator quotes a peak number: the multiply rate if every multiplier ran every cycle. Tilessa's target is narrower and stricter: sustained int8/BFP TOPS/mm² on inference workloads after the memory and BFP placement costs are counted. This chapter separates claim types:

proved: machine-checked Lean facts.
measured: numbers from checked-in RTL and OpenLane/OpenROAD logs.
modeled: workload and BFP-placement estimates from the previous chapter.
projected: scaled 16FFC numbers; no 16FFC result is claimed as measured.

3.1. Nano systolic utilization — proved🔗

The deeper fix is organisational. Wire the MAC elements into a systolic array — weights held, activations flowing one axis, partial sums the other — and in steady state every element does a MAC every cycle. We simulate the wavefront cycle-accurately (counting active elements per cycle, not asserting the textbook formula), then fold in the element's real per-cycle issue overhead.

namespace Perf

/-- Elements doing a MAC at cycle `t`: element (i,j) is active while
`i+j ≤ t < i+j+K`. -/
def activePEs (N K t : Nat) : Nat :=
  (List.range N).foldl (fun acc i =>
    acc + ((List.range N).filter (fun j => i + j ≤ t ∧ t < i + j + K)).length) 0

/-- Measured useful MAC-cycles over the whole run (sum over cycles). -/
def macCycles (N K : Nat) : Nat :=
  (List.range (K + 2 * N + 2)).foldl (fun acc t => acc + activePEs N K t) 0

/-- Measured wall-clock: cycles for which the array is busy. -/
def wall (N K : Nat) : Nat :=
  ((List.range (K + 2 * N + 2)).filter (fun t => activePEs N K t > 0)).length

/-- Array utilization, per-mille, straight from the simulation. -/
def arrayUtil (N K : Nat) : Nat := macCycles N K * 1000 / (N * N * wall N K)

/-- Sustained, folding in the element's mac-loop overhead (U MACs per U+1
cycles): a programmable element gives up almost nothing. -/
def sustained (N K U : Nat) : Nat := arrayUtil N K * U / (U + 1)

The simulation really does the full $N^2K$ useful MACs, and the sustained figures are machine-checked facts, not claims:

theorem sim_exact : macCycles 8 64 = 8 * 8 * 64 := by⊢ macCycles 8 64 = 8 * 8 * 64 native_decideAll goals completed! 🐙

theorem util_8x8   : sustained 8 256 16 = 892 := by⊢ sustained 8 256 16 = 892 native_decideAll goals completed! 🐙   -- 89.2%
theorem util_16x16 : sustained 16 1024 16 = 913 := by⊢ sustained 16 1024 16 = 913 native_decideAll goals completed! 🐙 -- 91.3%

end Perf

So a systolic tile of Nano elements sustains ~89–91% on long GEMMs. This is a proof-backed upper bound for compute-heavy phases, not a claim about full FlashAttention; the workload model adds SRAM, fabric, scale, softmax, and reduction pressure separately.

3.2. Routed Nano evidence — measured🔗

The measured OpenLane/OpenROAD sweep is now Nano-first:

| design | role | status | |---|---|---| | nano_i8 | int8 DP4A compute baseline | routed with detailed-route DRC 0; timing/setup still reported separately | | nano_mem | fixed memory-rich SRAM tile baseline | routed far enough to expose SRAM macro/Magic issues; not a clean signoff result | | nano_tile2 | two PE / two SRAM bank candidate | routed with detailed-route DRC violations; not clean | | nano_tile4 | four PE / four SRAM bank candidate | 20 ns run reaches post-route/post-PnR artifacts; not clean; estimated setup-limited Fmax is ~46.8 MHz | | nano_tile4_bfp | nano_tile4 plus boundary BFP assist stub | 20 ns run reaches post-route/post-PnR artifacts; not clean; measured as the conservative boundary-placement delta | | sys8 | fixed-function 64-MAC comparison | full signoff artifacts exist; DRC/LVS pass but antenna/timing violations remain |

A physical result is never called "clean" unless detailed-route DRC, Magic DRC, KLayout DRC, LVS, and timing status are all reported separately. The generated evidence table in docs/physical-evidence-generated.md is produced from the checked-in run logs instead of hand-copied numbers. It also reports the configured clock period and an estimated setup-limited Fmax: period + max(0, -setup_slack) is treated as the next lower-bound sweep point, not as signoff.

Two measured facts drive the architecture:

measured: nano_i8 adds DP4A-style int8 packing for a small area increment over the stripped Nano core, so the integer PE remains the default throughput path.
measured: SRAM macros dominate memory-rich tiles; banking and macro integration, not the Nano proof, are the first physical risks.
measured/model-calibrated: the current 20 ns nano_tile4 sky130 run gives a routed-but-not-clean 0.8782 mm² cell-area point, 14 detailed-route DRC errors, and an estimated 46.8 MHz setup-limited point. The matched nano_tile4_bfp run reports 0.8988 mm² cell area, 18 route DRC errors, and 45.1 MHz estimated setup-limited Fmax, so the rounded observed boundary-BFP area delta is 0.0206 mm². The workload model names the base calibration separately as nanoTile4ObservedSky130.

3.3. Workload placement — modeled🔗

The model in the previous chapter compares edge-only, tile-boundary, per-bank, and PE-local BFP scale handling. The default remains conservative: integer-only Nano PEs, scales in tile SRAM/fabric, and conversion/requantization at the tile boundary or mesh edge. PE-local scale logic is modeled, but it places BFP on the MAC path and breaks the simple "integer Nano PE" proof story until a real workload win justifies that cost.

3.4. 16FFC density — projected🔗

Scaling the measured sky130 runs to 16FFC remains a projection, not evidence. The working range is area divided by roughly 10–15 and clock multiplied by roughly 8–15. Until a real 16FFC run exists, those numbers are only planning inputs for tile sizing and MPW conversations.

The claim this book can defend today is therefore precise: the Nano core and its MAC semantics are proved; representative Nano RTL and routed sky130 artifacts are measured; BFP placement is modeled against real inference traffic; 16FFC TOPS/mm² is projected and labeled as such.