# proposal/10-fpga-loop.md · versecafe/strata [View on GitCafe](https://git.cafe/versecafe/strata/blob/06a4f98bcf687ad2c86b99aa7d0d12ecbd5a2bb9/proposal/10-fpga-loop.md) Repository: [versecafe/strata](https://git.cafe/versecafe/strata) Visibility: public Requested revision: 06a4f98bcf687ad2c86b99aa7d0d12ecbd5a2bb9 Requested commit: 06a4f98bcf687ad2c86b99aa7d0d12ecbd5a2bb9 Commit: 06a4f98bcf687ad2c86b99aa7d0d12ecbd5a2bb9 Blob: 44b4d4b90f380c0418a22711ef0cbac5b47a1970 Size: 8124 bytes [Immutable source](https://git.cafe/versecafe/strata/blob/06a4f98bcf687ad2c86b99aa7d0d12ecbd5a2bb9/proposal/10-fpga-loop.md?format=markdown) ``` # Synthesis Feedback and the FPGA Loop The physical-evidence layer: how implementation reality feeds back into the semantic substrate. Principles in force: P-2 (cost visible), P-7 (physical facts are evidence, never types), D-005 (FPGA-first, ASIC-clean). ## Committed design ### 1. Pre-synthesis estimation Components carry structure reports (comparator counts, reduction depth, register counts, estimated LUTs/delay) computed from architectural nodes before any vendor tool runs — these are `Estimated` evidence, explicitly weaker than `Measured`. Budgets (`#[budget(max_latency, max_luts, max_fanout)]`) check against estimates early and against measurements late. Candidate open estimation backend: circt-synth's AIG + longest-path timing analysis over our emitted structural IR ([07 §2](07-compiler-architecture.md)) — giving a vendor-independent delay/area signal cheap enough to run in CI. ### 2. Structured synthesis feedback Vendor tool output is parsed into structured diagnostics anchored to provenance: critical path reported as a chain of _source-level_ structures (via the [ledger](07-compiler-architecture.md)), with candidate improvements stated in architectural vocabulary (hierarchical priority encoder, added pipeline stage, split allocation groups, fanout reduction) — consumable by the [synthesis agent](09-agent-system.md). Objectives/constraints (`#[optimize(objectives, constraints)]`) define the optimizer's contract-shaped problem ([07 §4](07-compiler-architecture.md)). ### 3. Hardware-in-the-loop experiments `experiment` declarations (comptime-generated variant sweeps × workloads × measurements) drive: automated bitstream builds, deployment, execution, trace/counter capture, fault injection, randomized I/O timing, and simulation-vs-hardware comparison. Every run is reproducible (P-6 determinism extends to experiment definitions) and lands in the [experiment database](09-agent-system.md) as `Measured` evidence attached to the design hash. Captured per-branch and occupancy counters double as the **hardware-PGO source** (D-071): they land as `Measured` likelihood facts on stable node identities, and the contract-shaped search re-runs against them ([07 §5](07-compiler-architecture.md)) — profile-guided cost ranking with the profile attached to the design by node identity, not by fragile source location. ### 4. Evidence discipline Frequency, area, power, and fanout claims in any summary or agent report must cite their evidence tag. A design promoted through a release gate needs measurement on the gate's named target; simulation IPC and estimated frequency never silently substitute (P-7). Divergence between simulation and FPGA measurement is itself a first-class result (it indicts either the model or the design) and is retained in the experiment database. Physical and lifecycle evidence is invalidation-sensitive. Retiming, cloning, clock/mode changes, DVFS points, power intent, scan insertion, reconfiguration, netlist revision, vendor-tool version, target, or seed invalidate exactly the certificates whose dependency manifests name those facts. Reuse requires re-binding and re-checking, not filename equality. ### 5. Physical information: four channels in, one door closed (D-075) Physical information genuinely enters the language through four channels — as **evidence** (`Measured<842MHz, vu19p, tool>` ledger facts ranking candidates and gating releases, D-017), as **coeffect obligations** (`placement_distance(rf) <= D`, fanout/depth budgets — stated in source, discharged at implementation), as **search inputs** (D-071 `Measured` counters on stable node identities re-running the contract-shaped search), and as **budgets vs estimates** (P-2, circt-synth-class early signals). The single closed door: **physical facts never participate in type equality or judgment soundness.** The precise form (verification-hardened, 2026-07-17): post-P&R timing is a function of _(design, context, target, tool, seed)_, not of the design term — any judgment sound for the term alone must either quantify over all contexts, yielding bounds too loose to bear load, or freeze the context, at which point it is a measured fact about an _artifact_, which is exactly what the evidence lattice stores. And composition offers no frame rule: adding neighbors invalidates a physical-timing judgment on an untouched subterm (congestion, routing), so tight bounds aren't compositional and compositional bounds aren't tight. The boundary case that proves the rule: RapidWright-style pre-implemented modules — placed-and-locked macros with carried timing — are supported _as `Measured` evidence on a reusable artifact_, never as a type. (Cycle-level timing, by contrast, _is_ a function of the design and _is_ typed — [03](03-time-and-resources.md); the door closes exactly at the physical layer.) ## North star - ASIC flow adapters: same evidence schema, `Measured` from signoff tools; CDC/timing signoff reports imported as evidence artifacts. - Fleet-scale HIL: many boards, scheduled like CI, with the corpus manager targeting hardware-only behaviors (I/O timing races) simulation can't reach. - Learned cost models trained on the experiment database's estimate-vs-measured pairs, tightening §1 estimates per target. Industrial precedent exists and is acknowledged rather than ignored: Synopsys DSO.ai and Cadence Cerebrus run learned search over opaque flows (reported ~20% PPA), Google's RL placement (AlphaChip) the same for macros — **the delta is that Strata's candidates pass deterministic legality checks under declared contracts before ranking; backend and physical claims still require downstream evidence** (D-076). - Netlist-custody adapters that resolve intended false/multicycle/generated-clock constraints to exact nonempty post-synthesis path manifests and check lineage, precedence, setup/hold pairing, mode, and clocks before admission. Source semantics creates a candidate certificate; only the bound artifact earns evidence (D-086). - Power/DFT/reconfiguration adapters: import IEEE 1801-class power intent and vendor reports as external artifacts; validate isolation/retention/test/reconfiguration contracts against the emitted and implemented design; preserve the boundary between digital guarantees and characterized electrical assumptions. - Fault-injection HIL across transient/permanent campaigns, with injected model, physical mechanism, coverage, target, and recovery observation attached to each result. FPGA fault injection validates declared campaigns, not radiation/environmental equivalence without separate evidence. - **Release-full spatial optimization (D-076)** — composes from existing machinery, no new semantics: on vendor flows Strata drives the search _around_ the placer (regions, constraints, restructuring per D-041 + the Exit-2 bundle, [07 §2b](07-compiler-architecture.md)) — the prior art is direct (RapidLayout's evolutionary placement DSE via RapidWright beat manual Vivado constraints 5–6×; AutoBridge's floorplan-coupled pipelining took 43 designs from 147→297 MHz average), with direct-placement ownership scoped honestly to AMD/Xilinx (RapidWright has no Intel-side equivalent) and the open RTLIL→nextpnr flow as where deeper ownership arrives. P-7 makes it structurally a measured search loop, never a closed-form solve: legality from the semantic substrate, ranking from this loop, cost models learned from the experiment DB. And because placement is NP-hard, "release-full" is an objective profile (D-070) plus a compute budget — **under a keep-the-best policy over contract-legal candidates against a pinned measurement protocol, additional compute is monotone in best-measured QoR; it does not strengthen the contracts or physical evidence**. ## Open problems touching this doc None owned. Feeds the [evidence lattice](06-refinements-and-evidence.md); consumes ledger provenance ([OP-6](open-problems.md) erosion would degrade §2's source-anchored feedback — a concrete consumer to test against). ```