|
1 | | -# FPGA Loop Cooperation Variants — 2026-07-06 (for W397) |
| 1 | +# FPGA Loop Cooperation Variants — W404 (2026-07-06) |
2 | 2 |
|
3 | | -**Basis:** W396 closed as honest diagnostic gathering. H2 (bitstream config), H3 (round-trip mismatch), and H4 (package chipdb) are ruled out. H1 (cold-POR mode-pin sampling) is the only remaining high-priority hypothesis. W397 must either confirm H1 or expand the diagnostic set. |
| 3 | +> Proposed follow-up to Wave Loop 403 ([#1307](https://github.com/t27/t27/issues/1307)). |
| 4 | +> Each variant is independently valuable; choose based on available hardware and |
| 5 | +> reviewer bandwidth. |
4 | 6 |
|
5 | 7 | --- |
6 | 8 |
|
7 | | -## Variant A — Confirm and fix cold-POR mode sampling (default) |
| 9 | +## Variant A — Capture the actual CCLK frequency on P12 |
8 | 10 |
|
9 | | -Execute the user-assisted cold-POR experiment that W396 could not complete autonomously: |
| 11 | +**Goal:** close the deferred physical AC by measuring the real CCLK frequency |
| 12 | +and duty cycle produced by the canonical `OSCFSEL=0` bitstream. |
10 | 13 |
|
11 | | -1. Power off the QMTech Wukong V1 board completely (all rails) for ≥10 s. |
12 | | -2. Power on. |
13 | | -3. Within seconds, run `tri fpga stat --pre-jtag-reset` and capture `MODE`, `BUS Width`, `INIT_B`, `DONE`. |
14 | | -4. Then run `tri fpga stat` (JTAG reset path) and capture again. |
| 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. |
15 | 24 |
|
16 | | -If cold-POR `MODE` differs from post-reset `MODE=0x1`, H1 is confirmed. Root-cause fixes depend on the observed value: |
17 | | - |
18 | | -- If cold-POR samples `MODE=0x0` (JTAG) or another value, inspect the board's M0/M1/M2 pull resistor network and `CFGBVS`/`PUDC_B` strapping. A stronger pull-up/down or a dedicated strapping resistor may be needed. |
19 | | -- If cold-POR samples the same `MODE=0x1` but boot still fails, the issue is not mode sampling; move to Variant B or C. |
20 | | - |
21 | | -**Deliverables:** evidence log, board schematic note, `fpga/HARDWARE_SSOT.md` update, and (if a fix is found) a working flash-boot end-to-end. |
22 | | - |
23 | | -**IGLA impact:** +0 generic ∀ in W397 unless a quick fix leaves cycles; keep the 125-wave no-regression streak. |
| 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. |
24 | 29 |
|
25 | 30 | --- |
26 | 31 |
|
27 | | -## Variant B — Bitstream-generation / SPI-startup fix |
28 | | - |
29 | | -If Variant A shows the same correct `MODE=0x1` at cold-POR and boot still fails, the problem lies deeper than mode sampling. Candidate causes: |
| 32 | +## Variant B — Extend the Lean 4 model to `OSCFSEL` variants and CCLK bounds (no hardware) |
30 | 33 |
|
31 | | -- `COR0` CCLK frequency field is `0` (default decode). Some Artix-7 speed grades interpret this as a frequency the N25Q128 cannot satisfy in the specific board environment, or the openXC7 `fasm2frames`/`xc7frames2bit` path omits a required SPI-startup timing detail. |
32 | | -- The openXC7-generated bitstream works in JTAG/SRAM loading but is missing a frame or command needed for autonomous SPI boot. Compare a Vivado-generated `.bin` of the same design byte-by-byte with the OpenXC7 output. |
33 | | -- The `bscan_spi` bridge loaded during openFPGALoader flash access leaves the FPGA in a state that interferes with the next boot sequence. |
| 34 | +**Goal:** strengthen the formal FPGA-boot story by making the model speak about |
| 35 | +the `OSCFSEL` field and the derived CCLK frequency bounds, without requiring a |
| 36 | +physical measurement. |
34 | 37 |
|
35 | | -**Actions:** |
36 | | -- Regenerate a minimal GF16 bitstream with explicit `BITSTREAM.CONFIG.CONFIGRATE` and `SPI_BUSWIDTH` constraints and test flash boot. |
37 | | -- Use `bitread`/FASM diff to compare OpenXC7 vs Vivado bitstreams for the same design. |
38 | | -- Try a different, simpler design (e.g., `fpga/openxc7-synth/blink_j26.bit` rebuilt for XC7A200T) to see if the failure is design-specific. |
| 38 | +**Steps:** |
| 39 | +1. Add constants for the documented `OSCFSEL` values and the corresponding |
| 40 | + nominal CCLK ranges to `TernaryFPGABoot.lean`. |
| 41 | +2. Define a predicate `cclk_within_flash_spec` that states the configured CCLK |
| 42 | + is compatible with the N25Q128 read timing. |
| 43 | +3. Prove that `canonical` + `OSCFSEL=0` implies `cclk_within_flash_spec` under |
| 44 | + the published Artix-7 startup clock tables. |
| 45 | +4. Link the result to `fpga/HARDWARE_SSOT.md` §3.3 (H2 decision tree) as a |
| 46 | + formal justification for why the default bitstream is timing-safe. |
39 | 47 |
|
40 | | -**Deliverables:** root cause in the generation flow, a patched wrapper or `.fasm` pre-processing step, and a booting bitstream. |
| 48 | +**Effort:** ~4–6 hours; no hardware. |
| 49 | +**Dependencies:** Lean 4 toolchain + Xilinx UG470 tables. |
| 50 | +**Impact:** turns the W400 empirical result into a provable timing claim, |
| 51 | +adding another formal barrier for competitors to match. |
41 | 52 |
|
42 | 53 | --- |
43 | 54 |
|
44 | | -## Variant C — Vivado-in-Docker fallback |
| 55 | +## Variant C — Cable-connected end-to-end smoke verification |
45 | 56 |
|
46 | | -If both Variant A and Variant B fail to yield a bootable OpenXC7 bitstream, accept that the open-source 7-series toolchain may have a fundamental gap for XC7A200T FGG676 autonomous SPI boot. Switch to the Vivado-in-Docker path. |
| 57 | +**Goal:** extend `tri fpga smoke-gate` so that, when a Digilent cable is |
| 58 | +detected, it also loads the GF16 matrix into SRAM and asserts `DONE=HIGH`. |
47 | 59 |
|
48 | | -**Prerequisites (require user action outside the agent):** |
49 | | -- Restore/install Vivado 2025.2 or later Linux installer. |
50 | | -- Provide a valid `wi_authentication_key` or offline entitlement. |
51 | | -- Build the `t27/vivado:webpack` Docker image or supply a multi-arch image. |
| 60 | +**Steps:** |
| 61 | +1. Detect cable presence with `openFPGALoader --detect -c digilent_hs2`. |
| 62 | +2. If the cable is present, run: |
| 63 | + ```bash |
| 64 | + openFPGALoader -c digilent_hs2 fpga/verilog/ternary_mac_demo_top_200t.bit |
| 65 | + ``` |
| 66 | + and then `tri fpga stat` to read `DONE`. |
| 67 | +3. Keep the board-less assertions as the mandatory path and make the physical |
| 68 | + SRAM load an optional bonus check that is skipped gracefully when no cable is |
| 69 | + connected. |
| 70 | +4. Add a `--require-cable` flag for CI runners that expect hardware. |
52 | 71 |
|
53 | | -**Actions:** |
54 | | -- Build `gf16_matmul4x4_top.bit` through Vivado for `xc7a200tfgg676-1`. |
55 | | -- Program flash with `tri fpga program-flash` and test cold boot. |
56 | | -- If Vivado-generated bitstream boots from flash, bisect the OpenXC7 differences and file actionable upstream issues or patches. |
57 | | - |
58 | | -**Deliverables:** boot-from-flash working via Vivado, documented OpenXC7 gap, and a decision on whether to maintain dual-toolchain support. |
| 72 | +**Effort:** ~3–5 hours; needs the board for final verification. |
| 73 | +**Dependencies:** Digilent FTDI cable + board. |
| 74 | +**Impact:** turns `smoke-gate` from a static bitstream audit into a true |
| 75 | +hardware smoke test, without breaking board-less CI. |
59 | 76 |
|
60 | 77 | --- |
61 | 78 |
|
62 | 79 | ## Recommendation |
63 | 80 |
|
64 | | -Start with **Variant A**. It is the only hypothesis that survived W396 and requires only a user-assisted power-cycle plus CLI capture. If H1 is disproven, proceed to **Variant B** before escalating to **Variant C**, because Vivado-in-Docker has unresolved entitlement/container blockers. |
| 81 | +If hardware is available, start with **Variant A** (it directly closes the |
| 82 | +physical AC and produces numeric evidence). If hardware is not available, |
| 83 | +**Variant B** is the highest-leverage no-hardware path. **Variant C** is best as |
| 84 | +a stretch goal once A is done. |
| 85 | + |
| 86 | +--- |
65 | 87 |
|
66 | | -*phi^2 + phi^-2 = 3 | TRINITY* |
| 88 | +*φ² + 1/φ² = 3 | TRINITY* |
0 commit comments