Tilessa

2. Workload-Tuned BFP Placement🔗

The Nano reset changes the question. The core is now small enough that the important design choice is no longer "can the processor route?" but "where do the BFP/MX scales live while real inference kernels run?" This chapter keeps that question executable: tiles, workloads, and BFP placements are ordinary Lean values, and the representative cases are checked when the book builds.

2.1. The model surface🔗

The units are deliberately simple. Area is square micrometres. Bandwidths are bytes per cycle. Counts are integer MACs unless a field says bytes or cycles.

namespace Tilessa namespace Workload inductive DataMode where | int8 | bfp8 | mx deriving DecidableEq, Repr /-- Nano core parameters that affect throughput scheduling. -/ structure NanoConfig where registerCount : Nat dataMode : DataMode macsPerInstruction : Nat loadLatency : Nat deriving DecidableEq, Repr /-- Physical tile parameters used by the workload model. -/ structure TileConfig where peCount : Nat sramBytes : Nat bankCount : Nat sramPortsPerBank : Nat fabricEdgeBytesPerCycle : Nat clockMHz : Nat computeAreaUm2 : Nat sramAreaUm2 : Nat fabricAreaUm2 : Nat boundaryBfpAreaUm2 : Nat perBankBfpAreaUm2 : Nat peLocalBfpAreaUm2 : Nat deriving DecidableEq, Repr inductive BfpPlacement where | edgeOnly | tileBoundary | perBank | peLocal deriving DecidableEq, Repr inductive WorkloadKind where | flashPrefill | flashDecode | denseGemm | mlpGelu | kvCache | scaledDot deriving DecidableEq, Repr /-- Workload accounting. `opCount` is useful integer MACs. -/ structure Workload where kind : WorkloadKind opCount : Nat sramTrafficBytes : Nat fabricTrafficBytes : Nat scaleTrafficBytes : Nat softmaxCycles : Nat reductionCycles : Nat deriving DecidableEq, Repr def ceilDiv (n d : Nat) : Nat := if d = 0 then 0 else (n + d - 1) / d def max3 (a b c : Nat) : Nat := Nat.max (Nat.max a b) c

The default is intentionally conservative: integer-only Nano PEs, scale metadata held in tile SRAM/fabric, and conversion at the tile boundary or mesh edge until measurements justify bringing more BFP logic inward.

def nanoI8 : NanoConfig where registerCount := 4 dataMode := .int8 macsPerInstruction := 4 loadLatency := 1 def nanoBfpBoundary : NanoConfig where registerCount := 4 dataMode := .bfp8 macsPerInstruction := 4 loadLatency := 1 def nanoMemTile : TileConfig where peCount := 2 sramBytes := 2 * 1024 bankCount := 2 sramPortsPerBank := 1 fabricEdgeBytesPerCycle := 32 clockMHz := 95 computeAreaUm2 := 2 * 29038 sramAreaUm2 := 2 * 191444 fabricAreaUm2 := 32000 boundaryBfpAreaUm2 := 12000 perBankBfpAreaUm2 := 5000 peLocalBfpAreaUm2 := 3000 def nanoTile4 : TileConfig where peCount := 4 sramBytes := 4 * 1024 bankCount := 4 sramPortsPerBank := 1 fabricEdgeBytesPerCycle := 64 clockMHz := 95 computeAreaUm2 := 4 * 29038 sramAreaUm2 := 4 * 191444 fabricAreaUm2 := 52000 boundaryBfpAreaUm2 := 16000 perBankBfpAreaUm2 := 5000 peLocalBfpAreaUm2 := 3000 /-- Current routed-but-not-clean sky130 `nano_tile4` observation. The area and clock are calibration inputs from `docs/physical-evidence-generated.md`: the 20 ns run reports 0.8782 mm² cell area and an estimated 46.8 MHz setup-limited point. This is not a signoff-clean frequency claim; it is the conservative point used to tune the next sweep. -/ def nanoTile4ObservedSky130 : TileConfig where peCount := 4 sramBytes := 4 * 1024 bankCount := 4 sramPortsPerBank := 1 fabricEdgeBytesPerCycle := 64 clockMHz := 47 computeAreaUm2 := 115350 sramAreaUm2 := 762850 fabricAreaUm2 := 0 boundaryBfpAreaUm2 := 20600 perBankBfpAreaUm2 := 5000 peLocalBfpAreaUm2 := 3000

2.2. Workloads🔗

The core set is small and aimed at the first tuning target: sustained TOPS/mm² on inference, especially FlashAttention. The formulas are not accuracy models; they are traffic and cycle-pressure models that say where the tile will stall.

def blockScales (values blockSize : Nat) : Nat := ceilDiv values blockSize /-- FlashAttention prefill for one head: QK and P·V, with K/V resident. -/ def flashPrefill (tokens dim blockSize : Nat) : Workload where kind := .flashPrefill opCount := 2 * tokens * tokens * dim sramTrafficBytes := 3 * tokens * dim fabricTrafficBytes := tokens * tokens + tokens * dim scaleTrafficBytes := 2 * blockScales (tokens * dim) blockSize softmaxCycles := tokens * ceilDiv tokens 16 reductionCycles := 2 * tokens * ceilDiv dim 32 /-- FlashAttention decode for one new token against an existing KV cache. -/ def flashDecode (cacheTokens dim blockSize : Nat) : Workload where kind := .flashDecode opCount := 2 * cacheTokens * dim sramTrafficBytes := 2 * cacheTokens * dim fabricTrafficBytes := cacheTokens + dim scaleTrafficBytes := 2 * blockScales (cacheTokens * dim) blockSize softmaxCycles := ceilDiv cacheTokens 16 reductionCycles := 2 * ceilDiv dim 32 def denseGemm (m n k blockSize : Nat) : Workload where kind := .denseGemm opCount := m * n * k sramTrafficBytes := m * k + k * n + 4 * m * n fabricTrafficBytes := m * n scaleTrafficBytes := blockScales (m * k) blockSize + blockScales (k * n) blockSize softmaxCycles := 0 reductionCycles := m * n * ceilDiv k 32 def mlpGelu (tokens hidden expansion blockSize : Nat) : Workload where kind := .mlpGelu opCount := 2 * tokens * hidden * expansion sramTrafficBytes := tokens * hidden + hidden * expansion + expansion * hidden fabricTrafficBytes := tokens * expansion scaleTrafficBytes := blockScales (hidden * expansion) blockSize + blockScales (expansion * hidden) blockSize softmaxCycles := 0 reductionCycles := tokens * ceilDiv expansion 16 def kvCacheTraffic (tokens dim blockSize : Nat) : Workload where kind := .kvCache opCount := 0 sramTrafficBytes := 2 * tokens * dim fabricTrafficBytes := 2 * tokens * dim scaleTrafficBytes := 2 * blockScales (tokens * dim) blockSize softmaxCycles := 0 reductionCycles := 0

2.3. Placement reports🔗

Every BFP placement report carries the fields the architecture decision needs: extra tile area, scale bytes, conversion/requantization cycles, fabric impact, SRAM bank pressure, critical-path risk, and whether the PE proof remains the integer Nano proof.

structure BfpReport where placement : BfpPlacement extraAreaUm2PerTile : Nat scaleMetadataBytes : Nat conversionRequantCycles : Nat fabricBandwidthBytes : Nat sramBankPressurePermille : Nat criticalPath : Bool preservesSimplePeProof : Bool deriving DecidableEq, Repr def baseTileAreaUm2 (t : TileConfig) : Nat := t.computeAreaUm2 + t.sramAreaUm2 + t.fabricAreaUm2 def bfpExtraAreaUm2 (t : TileConfig) : BfpPlacement → Nat | .edgeOnly => 0 | .tileBoundary => t.boundaryBfpAreaUm2 | .perBank => t.bankCount * t.perBankBfpAreaUm2 | .peLocal => t.peCount * t.peLocalBfpAreaUm2 def placementScaleBytes (t : TileConfig) (w : Workload) : BfpPlacement → Nat | .edgeOnly => w.scaleTrafficBytes | .tileBoundary => w.scaleTrafficBytes | .perBank => w.scaleTrafficBytes + t.bankCount | .peLocal => w.scaleTrafficBytes * t.peCount def conversionCycles (t : TileConfig) (w : Workload) : BfpPlacement → Nat | .edgeOnly => 2 * ceilDiv w.scaleTrafficBytes 2 + w.softmaxCycles | .tileBoundary => ceilDiv w.scaleTrafficBytes 2 + ceilDiv w.reductionCycles 4 | .perBank => ceilDiv w.scaleTrafficBytes (Nat.max 1 t.bankCount) | .peLocal => 0 def fabricBytesWithScales (t : TileConfig) (w : Workload) (p : BfpPlacement) : Nat := match p with | .edgeOnly => w.fabricTrafficBytes + w.scaleTrafficBytes | .tileBoundary => w.fabricTrafficBytes + ceilDiv w.scaleTrafficBytes 2 | .perBank => w.fabricTrafficBytes + placementScaleBytes t w p | .peLocal => w.fabricTrafficBytes + placementScaleBytes t w p def bankPressurePermille (t : TileConfig) (w : Workload) (p : BfpPlacement) : Nat := (w.sramTrafficBytes + placementScaleBytes t w p) * 1000 / Nat.max 1 w.sramTrafficBytes def onCriticalPath : BfpPlacement → Bool | .edgeOnly => false | .tileBoundary => false | .perBank => false | .peLocal => true def simplePeProof : BfpPlacement → Bool | .edgeOnly => true | .tileBoundary => true | .perBank => true | .peLocal => false def bfpReport (t : TileConfig) (w : Workload) (p : BfpPlacement) : BfpReport where placement := p extraAreaUm2PerTile := bfpExtraAreaUm2 t p scaleMetadataBytes := placementScaleBytes t w p conversionRequantCycles := conversionCycles t w p fabricBandwidthBytes := fabricBytesWithScales t w p sramBankPressurePermille := bankPressurePermille t w p criticalPath := onCriticalPath p preservesSimplePeProof := simplePeProof p

The model also gives a conservative sustained-density estimate. It takes the maximum of compute, SRAM, and fabric pressure, then adds the non-MAC softmax, reduction, and conversion cycles.

def macCycles (n : NanoConfig) (t : TileConfig) (w : Workload) : Nat := ceilDiv w.opCount (Nat.max 1 (t.peCount * n.macsPerInstruction)) def sramCycles (t : TileConfig) (w : Workload) : Nat := ceilDiv w.sramTrafficBytes (Nat.max 1 (t.bankCount * t.sramPortsPerBank * 4)) def fabricCycles (t : TileConfig) (r : BfpReport) : Nat := ceilDiv r.fabricBandwidthBytes (Nat.max 1 t.fabricEdgeBytesPerCycle) def workloadCycles (n : NanoConfig) (t : TileConfig) (w : Workload) (p : BfpPlacement) : Nat := let r := bfpReport t w p max3 (macCycles n t w) (sramCycles t w) (fabricCycles t r) + w.softmaxCycles + w.reductionCycles + r.conversionRequantCycles /-- Milli-TOPS/mm², counting one MAC as one operation for conservative ranking. -/ def sustainedMilliTopsPerMm2 (n : NanoConfig) (t : TileConfig) (w : Workload) (p : BfpPlacement) : Nat := let cycles := workloadCycles n t w p let area := baseTileAreaUm2 t + bfpExtraAreaUm2 t p w.opCount * t.clockMHz * 1000 / Nat.max 1 (cycles * area)

2.4. Checked cases🔗

The examples below are intentionally small enough to audit by eye, but they exercise the same formulas as the larger tuning sweeps.

def prefill4x8 : Workload := flashPrefill 4 8 32 def decode16x8 : Workload := flashDecode 16 8 32 def gemm4x4x8 : Workload := denseGemm 4 4 8 32 def prefill64x64 : Workload := flashPrefill 64 64 32 theorem prefill_case_checked : prefill4x8.opCount = 256 ∧ prefill4x8.sramTrafficBytes = 96 ∧ (bfpReport nanoMemTile prefill4x8 .tileBoundary).scaleMetadataBytes = 2 ∧ workloadCycles nanoBfpBoundary nanoMemTile prefill4x8 .tileBoundary = 47 := ⊢ prefill4x8.opCount = 256 ∧ prefill4x8.sramTrafficBytes = 96 ∧ (bfpReport nanoMemTile prefill4x8 BfpPlacement.tileBoundary).scaleMetadataBytes = 2 ∧ workloadCycles nanoBfpBoundary nanoMemTile prefill4x8 BfpPlacement.tileBoundary = 47 All goals completed! 🐙 theorem decode_case_checked : decode16x8.opCount = 256 ∧ decode16x8.sramTrafficBytes = 256 ∧ (bfpReport nanoMemTile decode16x8 .tileBoundary).fabricBandwidthBytes = 28 ∧ workloadCycles nanoBfpBoundary nanoMemTile decode16x8 .tileBoundary = 40 := ⊢ decode16x8.opCount = 256 ∧ decode16x8.sramTrafficBytes = 256 ∧ (bfpReport nanoMemTile decode16x8 BfpPlacement.tileBoundary).fabricBandwidthBytes = 28 ∧ workloadCycles nanoBfpBoundary nanoMemTile decode16x8 BfpPlacement.tileBoundary = 40 All goals completed! 🐙 theorem gemm_case_checked : gemm4x4x8.opCount = 128 ∧ gemm4x4x8.scaleTrafficBytes = 2 ∧ workloadCycles nanoBfpBoundary nanoMemTile gemm4x4x8 .tileBoundary = 37 := ⊢ gemm4x4x8.opCount = 128 ∧ gemm4x4x8.scaleTrafficBytes = 2 ∧ workloadCycles nanoBfpBoundary nanoMemTile gemm4x4x8 BfpPlacement.tileBoundary = 37 All goals completed! 🐙 theorem default_placement_keeps_integer_pe_story : (bfpReport nanoMemTile prefill4x8 .tileBoundary).criticalPath = false ∧ (bfpReport nanoMemTile prefill4x8 .tileBoundary).preservesSimplePeProof = true ∧ (bfpReport nanoMemTile prefill4x8 .peLocal).criticalPath = true ∧ (bfpReport nanoMemTile prefill4x8 .peLocal).preservesSimplePeProof = false := ⊢ (bfpReport nanoMemTile prefill4x8 BfpPlacement.tileBoundary).criticalPath = false ∧ (bfpReport nanoMemTile prefill4x8 BfpPlacement.tileBoundary).preservesSimplePeProof = true ∧ (bfpReport nanoMemTile prefill4x8 BfpPlacement.peLocal).criticalPath = true ∧ (bfpReport nanoMemTile prefill4x8 BfpPlacement.peLocal).preservesSimplePeProof = false All goals completed! 🐙 theorem nano_tile4_observed_calibration : nanoTile4ObservedSky130.clockMHz = 47 ∧ baseTileAreaUm2 nanoTile4ObservedSky130 = 878200 ∧ workloadCycles nanoBfpBoundary nanoTile4ObservedSky130 prefill64x64 .tileBoundary = 33472 ∧ (bfpReport nanoTile4ObservedSky130 prefill64x64 .tileBoundary).extraAreaUm2PerTile = 20600 := ⊢ nanoTile4ObservedSky130.clockMHz = 47 ∧ baseTileAreaUm2 nanoTile4ObservedSky130 = 878200 ∧ workloadCycles nanoBfpBoundary nanoTile4ObservedSky130 prefill64x64 BfpPlacement.tileBoundary = 33472 ∧ (bfpReport nanoTile4ObservedSky130 prefill64x64 BfpPlacement.tileBoundary).extraAreaUm2PerTile = 20600 All goals completed! 🐙

The BFP arithmetic connection is the existing scaled_dot theorem from the edge chapter, reused directly by this placement model. Scale handling can move around the tile; the PE still computes the integer dot that theorem factors.

def sampleA (i : Nat) : Int := (i % 5 : Nat) - 2 def sampleB (i : Nat) : Int := (i % 7 : Nat) - 3 theorem bfp_scaled_dot_matches_boundary : isum 32 (fun i => (2 * sampleA i) * (3 * sampleB i)) = (2 * 3) * isum 32 (fun i => sampleA i * sampleB i) := ⊢ (isum 32 fun i => 2 * sampleA i * (3 * sampleB i)) = 2 * 3 * isum 32 fun i => sampleA i * sampleB i All goals completed! 🐙 end Workload end Tilessa

The conservative result is therefore explicit: tile-boundary BFP carries a small area and cycle tax, keeps scale metadata out of the PE, keeps BFP off the MAC critical path, and preserves the simple Nano proof story. Edge-only remains the lowest-area baseline; PE-local BFP is reserved for evidence that the workload benefit outweighs the verification and timing cost.