|
1 | | -# Wave Loop 400 — Cooperation Variants |
| 1 | +# FPGA Loop Cooperation Variants — W403 (2026-07-05) |
2 | 2 |
|
3 | | -**Context:** W399 automated the W398 CCLK-sweep workflow. The physical cold-POR |
4 | | -CCLK sweep has not yet been run; W400 should close that loop on the QMTech |
5 | | -Wukong V1 / XC7A200T-FGG676-1. |
6 | | - |
7 | | -**Constraint:** A true cold power-cycle still requires a user-assisted physical |
8 | | -step. Any W400 variant should either (a) perform that step or (b) make fallback |
9 | | -progress if board access is unavailable. |
| 3 | +> Proposed follow-up to Wave Loop 402 ([#1305](https://github.com/t27/t27/issues/1305)). |
| 4 | +> Each variant is independently valuable; choose based on available hardware and |
| 5 | +> reviewer bandwidth. |
10 | 6 |
|
11 | 7 | --- |
12 | 8 |
|
13 | | -## Variant A — Run the automated cold-POR CCLK sweep and commit a working default (default, root-cause driven) |
| 9 | +## Variant A — Capture the actual CCLK frequency on P12 |
14 | 10 |
|
15 | | -**Goal:** definitively identify a raw `OSCFSEL` value that boots the board from |
16 | | -flash, measure its actual CCLK frequency, and make that the default bitstream. |
| 11 | +**Goal:** close the deferred physical AC by measuring the real CCLK frequency |
| 12 | +and duty cycle produced by the canonical `OSCFSEL=0` bitstream. |
17 | 13 |
|
18 | | -**Work** |
19 | | -1. Run `tri fpga cclk-sweep fpga/verilog/ternary_mac_demo_top_200t.bit`. |
20 | | -2. For each variant the command will program flash, prompt for the cable-disconnect |
21 | | - + power-cycle, capture STAT, and write a JSON log. |
22 | | -3. Run `tri fpga sweep-report --out build/fpga/sweep-report.md` to identify the first |
23 | | - working variant. |
24 | | -4. Measure actual CCLK for the working variant with a logic analyser / oscilloscope |
25 | | - (see `tri fpga measure-cclk`). |
26 | | -5. Optionally parse the DSView CSV with `tri fpga measure-cclk --csv <file>`. |
27 | | -6. Rename the working variant to the canonical default and update |
28 | | - `fpga/HARDWARE_SSOT.md` §3.5 and §9 with the measured frequency. |
| 14 | +**Steps:** |
| 15 | +1. Attach a logic analyzer / oscilloscope to pin **P12** (CFGCLK / CCLK_0). |
| 16 | +2. Trigger on board power-on; capture the first ~100 µs. |
| 17 | +3. Export CSV and run: |
| 18 | + ```bash |
| 19 | + tri fpga measure-cclk --csv build/fpga/p12_cclk.csv |
| 20 | + ``` |
| 21 | +4. Record the frequency and duty cycle in `fpga/HARDWARE_SSOT.md` §3.5. |
| 22 | +5. Optionally sweep `OSCFSEL=0..5` and measure each variant to map raw field |
| 23 | + value to MHz. |
29 | 24 |
|
30 | | -**Acceptance** |
31 | | -- AC-A1: cold-POR `DONE=1` for at least one CCLK variant. |
32 | | -- AC-A2: The working `OSCFSEL` value and measured CCLK frequency are documented. |
33 | | -- AC-A3: The default bitstream committed to the repo boots from flash. |
| 25 | +**Effort:** ~2–4 hours bench time. |
| 26 | +**Dependencies:** physical board + DSLogic/oscilloscope. |
| 27 | +**Impact:** turns the default bitstream choice from empirical to quantitative; |
| 28 | +unblocks future frequency-limited flash devices. |
34 | 29 |
|
35 | 30 | --- |
36 | 31 |
|
37 | | -## Variant B — Board-less CI and reproducible toolchain recipe (fallback if no board) |
38 | | - |
39 | | -**Goal:** make the FPGA evidence path reproducible without a physical board by |
40 | | -hardening the board-less smoke gate and removing dependencies on opaque upstream |
41 | | -artifacts. |
42 | | - |
43 | | -**Work** |
44 | | -1. Extend `tri fpga smoke-gate` to also run `tri fpga synth-gf16` end-to-end when |
45 | | - the openXC7 tools are on PATH, so CI exercises the full spec-to-bitstream |
46 | | - path. |
47 | | -2. Add a CI target that runs `tri fpga bit-config --assert-idcode 0x03636093 |
48 | | - --assert-spi-x1 --assert-cclk-startup` on every committed demo bitstream. |
49 | | -3. Document the exact openXC7/nextpnr/prjxray versions and build flags in |
50 | | - `fpga/HARDWARE_SSOT.md` so the toolchain can be rebuilt deterministically. |
51 | | -4. Investigate building or locating a 200T-compatible JTAG-to-SPI proxy without |
52 | | - Vivado, or document the upstream openFPGALoader `spiOverJtag` source so the |
53 | | - dependency is not entirely opaque. |
54 | | - |
55 | | -**Acceptance** |
56 | | -- AC-B1: `tri fpga smoke-gate` runs green in CI with no physical board and covers |
57 | | - bit-config, synthesis, and (optionally) the openXC7 GF16 flow. |
58 | | -- AC-B2: The FPGA path has a version-locked, reproducible toolchain recipe. |
| 32 | +## Variant B — Extend the Lean 4 model to configuration timing (no hardware) |
| 33 | + |
| 34 | +**Goal:** strengthen the formal FPGA-boot story by adding `STARTUPCLK` / |
| 35 | +`OSCFSEL` / `SPI_BUSWIDTH` predicates and proving that the canonical bitstream |
| 36 | +configuration implies `boot_success` under the cold-POR protocol. |
| 37 | + |
| 38 | +**Steps:** |
| 39 | +1. Add a `BitstreamConfig` structure to `TernaryFPGABoot.lean` with fields |
| 40 | + `idcode`, `spi_buswidth`, `startupclk`, `oscfsel`. |
| 41 | +2. Define a relation `config_implies_boot_pred` that states: when the |
| 42 | + bitstream is configured for `IDCODE=0x03636093`, SPI x1, CCLK startup, and |
| 43 | + `OSCFSEL=0`, then any cold-POR that samples mode correctly satisfies the |
| 44 | + preconditions for `boot_success` (modulo the physical CCLK timing question). |
| 45 | +3. Prove lemmas such as: |
| 46 | + - `mode_master_spi_x1_and_done_implies_boot_success` |
| 47 | + - `config_canonical : canonical_config → ...` |
| 48 | +4. Link the lemmas to `fpga/HARDWARE_SSOT.md` §3.3 (H2 decision tree). |
| 49 | + |
| 50 | +**Effort:** ~4–6 hours; no hardware. |
| 51 | +**Dependencies:** Lean 4 toolchain. |
| 52 | +**Impact:** gives t27 a publishable formal traceability claim for the entire |
| 53 | +FPGA boot path, not just the STAT decode. |
59 | 54 |
|
60 | 55 | --- |
61 | 56 |
|
62 | | -## Variant C — Vivado-in-Docker controlled comparison (long-leverage insurance) |
| 57 | +## Variant C — Cable-connected end-to-end smoke verification |
63 | 58 |
|
64 | | -**Goal:** produce a Vivado-generated XC7A200T SPI bitstream and compare its |
65 | | -behavior against the openXC7 bitstream, isolating whether the boot failure is an |
66 | | -openXC7 generation artifact. |
| 59 | +**Goal:** extend `tri fpga smoke-gate` so that, when a Digilent cable is |
| 60 | +detected, it also loads the GF16 matrix into SRAM and asserts `DONE=HIGH`. |
67 | 61 |
|
68 | | -**Work** |
69 | | -1. Resolve the Xilinx auth token / disk-space blockers documented in |
70 | | - `fpga/HARDWARE_SSOT.md` §4 and `docs/fpga/DOCKER_VIVADO_STATUS.md`. |
71 | | -2. Build a minimal 200T demo wrapper (or reuse `fpga/vivado/build_gf16_matmul4x4.tcl`) |
72 | | - inside a `t27/vivado:webpack` container with explicit `BITSTREAM.CONFIG.CONFIGRATE`. |
73 | | -3. Program the Vivado bitstream to flash and run the same cold-POR / JTAG-reset |
74 | | - STAT sequence. |
75 | | -4. Compare COR0/COR1 register values and CCLK timing between openXC7 and |
76 | | - Vivado outputs. |
| 62 | +**Steps:** |
| 63 | +1. Detect cable presence with `openFPGALoader --detect -c digilent_hs2`. |
| 64 | +2. If the cable is present, run: |
| 65 | + ```bash |
| 66 | + openFPGALoader -c digilent_hs2 fpga/verilog/ternary_mac_demo_top_200t.bit |
| 67 | + ``` |
| 68 | + and then `tri fpga stat` to read `DONE`. |
| 69 | +3. Keep the board-less assertions as the mandatory path and make the physical |
| 70 | + SRAM load an optional bonus check that is skipped gracefully when no cable is |
| 71 | + connected. |
| 72 | +4. Add a `--require-cable` flag for CI runners that expect hardware. |
77 | 73 |
|
78 | | -**Acceptance** |
79 | | -- AC-C1: A Vivado-generated 200T bitstream exists and is documented. |
80 | | -- AC-C2: The comparison identifies whether the boot failure is openXC7-specific |
81 | | - or board/flash-specific. |
| 74 | +**Effort:** ~3–5 hours; needs the board for final verification. |
| 75 | +**Dependencies:** Digilent FTDI cable + board. |
| 76 | +**Impact:** turns `smoke-gate` from a static bitstream audit into a true |
| 77 | +hardware smoke test, without breaking board-less CI. |
82 | 78 |
|
83 | 79 | --- |
84 | 80 |
|
85 | | -## Recommended choice |
86 | | - |
87 | | -**Variant A** is the default because W399 built the exact tooling needed for an |
88 | | -automated cold-POR CCLK sweep. A single user-assisted session with a logic |
89 | | -analyser is the shortest path to a booting board. |
90 | | - |
91 | | -If board access is unavailable, fall back to **Variant B** to keep the toolchain |
92 | | -reproducible and CI-enforced. |
| 81 | +## Recommendation |
93 | 82 |
|
94 | | -**Variant C** remains the long-leverage insurance policy: it resolves the |
95 | | -open-source-vs-vendor question but requires the most external setup (Xilinx |
96 | | -entitlement, disk space, Docker image). |
| 83 | +If hardware is available, start with **Variant A** (it directly closes the |
| 84 | +physical AC and produces numeric evidence). If hardware is not available, |
| 85 | +**Variant B** is the highest-leverage no-hardware path. **Variant C** is best as |
| 86 | +a stretch goal once A is done. |
97 | 87 |
|
98 | 88 | --- |
99 | 89 |
|
100 | | -*phi^2 + 1/phi^2 = 3 | TRINITY* |
| 90 | +*φ² + 1/φ² = 3 | TRINITY* |
0 commit comments