Skip to content

Commit 82c7df6

Browse files
Dmitrii Vasilevclaude
Dmitrii Vasilev
and
claude
committed
feat(igla): Wave Loop 404 — hardware smoke-gate --require-cable for FPGA SRAM load (Closes #1309)
- Add --require-cable, --cable, --part to tri fpga smoke-gate. - Detect Digilent FTDI cable/board via openFPGALoader --detect. - Load canonical bitstream into FPGA SRAM and assert boot_success conditions (DONE=1, MODE=0b001, no CRC/ID/DEC errors) using capture_stat. - Keep board-less bit-config audit, dry-run CCLK sweep, and yosys synthesis as the default mandatory path. - Update fpga/HARDWARE_SSOT.md §3.2 with hardware smoke traceability. - Update docs/NOW.md and .trinity/experience.md with W404 learnings. - Update .trinity/current-issue.md to point to W404 issue #1309. - Add .claude/plans/wave-loop-404.md with weak points, competitor scan, chosen variant, and acceptance-criteria status. - Add close-out reports: WAVE_LOOP_404_REPORT.md, FPGA_LOOP_EVIDENCE_2026-07-07.md, FPGA_LOOP_COOPERATION_2026-07-07.md. - Verified on bench: idcode 0x3636093, SRAM load done=1, STAT=0x401079FC. - Conformance suite 576/576 PASS. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
1 parent ca29005 commit 82c7df6

10 files changed

Lines changed: 601 additions & 153 deletions

File tree

‎.claude/plans/wave-loop-404.md‎

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,109 @@
1+
# Wave Loop 404 Plan — FPGA: close physical CCLK measurement or extend formal CCLK bounds
2+
3+
**Issue:** [#1309](https://github.com/t27/t27/issues/1309)
4+
**Branch:** `trinity-rust-rings`
5+
**Date:** 2026-07-06
6+
**Anchor:** φ² + φ⁻² = 3 | TRINITY
7+
8+
---
9+
10+
## Context
11+
12+
W403 closed without bench hardware by extending the Lean 4 model with the
13+
`BitstreamConfig` canonical predicate and `ColdPOR` linkage lemmas. At the start
14+
of W404 the attached Digilent FTDI cable and XC7A200T board were found to be
15+
reachable (`openFPGALoader --detect` returned idcode `0x3636093`), so the
16+
wave executed **Variant C** — a cable-connected SRAM smoke load in `tri fpga
17+
smoke-gate --require-cable`. Variant A (P12 CCLK measurement) remains blocked
18+
because no logic analyzer / oscilloscope is available.
19+
20+
---
21+
22+
## Weak points
23+
24+
1. **Physical CCLK measurement still blocked.** A Digilent FTDI cable and the
25+
XC7A200T board are connected, but no logic analyzer / oscilloscope is
26+
available for pin P12 capture. The agent can drive JTAG but cannot sample
27+
the analog CCLK waveform autonomously.
28+
2. **Operator-dependent capture.** A logic-analyzer/oscilloscope capture
29+
requires human bench time; the agent cannot perform it autonomously.
30+
3. **Cable detection fragility.** The `--require-cable` path depends on
31+
`openFPGALoader --detect` successfully returning an `idcode` line. If the
32+
board is powered off or the cable is swapped, the gate fails cleanly but
33+
cannot self-heal.
34+
4. **Competitor formal-HDL pressure.** Verilean / Sparkle HDL and Aria-HDL can
35+
produce timing/properties claims; t27 must keep adding traceability layers
36+
(formal → spec → generated code → physical measurement) to stay ahead.
37+
38+
---
39+
40+
## Competitor scan
41+
42+
- **Verilean / Sparkle HDL:** Lean 4-based HDL with embedded proofs. Closest
43+
formal competitor. Their strength is correctness of generated hardware;
44+
t27's differentiation is the spec-first `t27`/`tri` pipeline plus physical
45+
FPGA evidence.
46+
- **Aria-HDL:** meta-compiler with Lean 4 backend. Focuses on compiling
47+
existing HDL to verified code, not on the physical bring-up traceability chain.
48+
- **seLe4n:** Lean 4 microkernel. Relevant only to secure-boot claims, not
49+
directly to FPGA CCLK measurement.
50+
- **USENIX WOOT 2024 Zynq secure-boot paper:** shows that bitstream config
51+
fields matter for security; t27's formal config audit is a defensive parallel.
52+
- **FIRRTL/Chisel/Clash/Bluespec:** no formal proof of FPGA boot timing or
53+
STAT-register outcomes in their standard flows.
54+
55+
---
56+
57+
## Cooperation variants
58+
59+
See `docs/reports/FPGA_LOOP_COOPERATION_2026-07-06.md` for the pre-implementation
60+
variants. The implemented wave chose **Variant C** because the Digilent cable
61+
and XC7A200T board were detected; Variant A remains blocked by the lack of a
62+
logic analyzer / oscilloscope.
63+
64+
### Variant A — Physical CCLK measurement (deferred)
65+
66+
Capture CCLK on P12, run `tri fpga measure-cclk --csv`, and record the
67+
frequency/duty cycle in `fpga/HARDWARE_SSOT.md` §3.5. Deferred to W405 unless
68+
hardware becomes available.
69+
70+
### Variant B — Formal `OSCFSEL`/CCLK bounds (not executed)
71+
72+
Add `OSCFSEL` value constants and a `cclk_within_flash_spec` predicate to
73+
`TernaryFPGABoot.lean`; prove that the canonical config implies the N25Q128
74+
read timing is satisfied under published Artix-7 startup-clock tables. This
75+
remains a candidate for a future no-hardware wave.
76+
77+
### Variant C — `--require-cable` SRAM smoke load (implemented)
78+
79+
Extend `tri fpga smoke-gate` to detect the Digilent cable and, when present,
80+
load the GF16 matrix into SRAM and assert `DONE=HIGH`. Verified on the bench:
81+
- `openFPGALoader --detect -c digilent_hs2` returns idcode `0x3636093`.
82+
- `tri fpga load-sram` completes with `done 1`.
83+
- Post-load STAT = `0x401079FC`, matching `Trinity.StatRegister.boot_success`.
84+
85+
---
86+
87+
## Acceptance criteria
88+
89+
| ID | Criterion | Status |
90+
|----|-----------|--------|
91+
| AC-A1 | Physical CCLK trace captured on P12. | ⏸️ deferred |
92+
| AC-A2 | `fpga/HARDWARE_SSOT.md` §3.5 contains measured value. | ⏸️ deferred |
93+
| AC-B1 | New Lean 4 lemmas link `OSCFSEL`/CCLK bounds to decision trees. | ⏸️ not executed |
94+
| AC-C1 | `tri fpga smoke-gate --require-cable` reaches `DONE=HIGH` on the bench. | ✅ |
95+
| AC-D1 | `./scripts/tri test` passes. | ✅ |
96+
| AC-D2 | W404 report + evidence + W405 cooperation variants committed. | ✅ |
97+
98+
---
99+
100+
## Chosen variant
101+
102+
**Variant C** — because the Digilent FTDI cable and XC7A200T board are
103+
connected and reachable, making the hardware smoke gate the highest-leverage
104+
close-out for W404. Variant A remains the next priority once a logic analyzer
105+
or oscilloscope is available.
106+
107+
---
108+
109+
*φ² + φ⁻² = 3 | TRINITY*

‎.trinity/current-issue.md‎

Lines changed: 17 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -1,38 +1,39 @@
1-
# Wave Loop 403 — FPGA: close physical CCLK measurement or extend formal/physical smoke coverage
1+
# Wave Loop 404 — FPGA: close physical CCLK measurement or extend formal CCLK bounds
22

3-
**Issue:** #1307
3+
**Issue:** #1309
44
**Branch:** `trinity-rust-rings`
5-
**Milestone:** W402 formalized the cold-POR decision tree in Lean 4. W403 should
6-
close the remaining physical AC or extend formal/physical smoke coverage.
5+
**Milestone:** W403 extended the Lean 4 bitstream-config model. W404 should
6+
close the remaining physical AC or extend formal coverage.
77

88
---
99

1010
## Goal
1111

1212
1. Capture the actual CCLK frequency on pin P12 and record it in
1313
`fpga/HARDWARE_SSOT.md` (Variant A — default if hardware is available).
14-
2. OR extend the Lean 4 model with bitstream-configuration predicates
15-
(`STARTUPCLK`, `OSCFSEL`, `SPI_BUSWIDTH`) and link them to the decision trees
16-
(Variant B — no hardware required).
14+
2. OR extend the Lean 4 model with `OSCFSEL` variants / CCLK frequency-bound
15+
predicates and prove the canonical config is timing-safe (Variant B — no
16+
hardware required).
1717
3. OR extend `tri fpga smoke-gate` to optionally load the GF16 matrix into SRAM
1818
and assert `DONE=HIGH` when a cable is present (Variant C — stretch).
19-
4. Update close-out reports and open W404 cooperation variants.
19+
4. Update close-out reports and open W405 cooperation variants.
2020

2121
---
2222

2323
## Decomposed plan
2424

25-
See `.claude/plans/wave-loop-403.md` for the full work breakdown.
25+
See `docs/reports/FPGA_LOOP_COOPERATION_2026-07-06.md` for the full cooperation
26+
variants.
2627

2728
| Step | File(s) | Deliverable |
2829
|------|---------|-------------|
29-
| 1 | `.claude/plans/wave-loop-403.md` | Decomposed plan + weak-point + competitor scan |
30+
| 1 | `.claude/plans/wave-loop-404.md` | Decomposed plan + weak-point + competitor scan |
3031
| 2 | `fpga/HARDWARE_SSOT.md` (Variant A) | Measured CCLK frequency/duty cycle on P12 |
31-
| 3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant B) | Bitstream-config lemmas |
32+
| 3 | `proofs/lean4/Trinity/TernaryFPGABoot.lean` (Variant B) | OSCFSEL/CCLK-bound lemmas |
3233
| 4 | `cli/tri/src/fpga.rs` (Variant C) | Optional cable-connected SRAM smoke load |
33-
| 5 | `docs/reports/*` | W403 report, evidence, W404 cooperation |
34-
| 6 | `.trinity/experience.md` | W403 learnings |
35-
| 7 | git/PR | squash-merge to `trinity-rust-rings`, close #1307, open #W404 |
34+
| 5 | `docs/reports/*` | W404 report, evidence, W405 cooperation |
35+
| 6 | `.trinity/experience.md` | W404 learnings |
36+
| 7 | git/PR | squash-merge to `trinity-rust-rings`, close #1309, open #W405 |
3637

3738
---
3839

@@ -41,12 +42,12 @@ See `.claude/plans/wave-loop-403.md` for the full work breakdown.
4142
- [ ] AC-A1 (Variant A): a physical CCLK trace is captured and the dominant
4243
frequency is recorded.
4344
- [ ] AC-A2 (Variant A): `fpga/HARDWARE_SSOT.md` §3.5 contains the measured value.
44-
- [ ] AC-B1 (Variant B): new Lean 4 lemmas link canonical bitstream config to the
45+
- [ ] AC-B1 (Variant B): new Lean 4 lemmas link `OSCFSEL`/CCLK bounds to the
4546
documented decision trees.
4647
- [ ] AC-C1 (Variant C): `tri fpga smoke-gate --require-cable` reaches
4748
`DONE=HIGH` on the bench.
4849
- [ ] AC-D1: `./scripts/tri test` passes.
49-
- [ ] AC-D2: W403 report + evidence + W404 cooperation variants committed.
50+
- [ ] AC-D2: W404 report + evidence + W405 cooperation variants committed.
5051

5152
---
5253

‎.trinity/current_task/activity.md‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1368,3 +1368,19 @@
13681368
- **Commit:** Merge branch 'master' into trinity-rust-rings for W403 (Closes #1307)
13691369
- **Files:** .claude/plans/wave-loop-403.md,.trinity/current-issue.md,.trinity/current_task/activity.md,.trinity/experience.md,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_2026-07-06.md,docs/reports/FPGA_LOOP_EVIDENCE_2026-07-06.md,docs/reports/WAVE_LOOP_403_REPORT.md,fpga/HARDWARE_SSOT.md,proofs/lean4/Trinity/TernaryFPGABoot.lean
13701370

1371+
## 2026-07-04T09:16:11Z — trinity-rust-rings
1372+
- **Commit:** feat(igla): Wave Loop 403 — bitstream config linked to cold-POR decision tree in Lean 4 (Closes #1307)
1373+
- **Files:** .trinity/current-issue.md
1374+
1375+
## 2026-07-04T09:16:34Z — trinity-rust-rings
1376+
- **Commit:** chore(trinity): point current-issue.md to W404 issue #1309
1377+
- **Files:** .claude/plans/wave-loop-404.md
1378+
1379+
## 2026-07-04T09:29:40Z — trinity-rust-rings
1380+
- **Commit:** docs(trinity): add decomposed W404 plan with weak points and competitor scan (Closes #1309)
1381+
- **Files:** .claude/plans/wave-loop-404.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_2026-07-07.md,docs/reports/FPGA_LOOP_EVIDENCE_2026-07-07.md,docs/reports/WAVE_LOOP_404_REPORT.md,fpga/HARDWARE_SSOT.md
1382+
1383+
## 2026-07-04T09:30:41Z — trinity-rust-rings
1384+
- **Commit:** feat(igla): Wave Loop 404 — hardware smoke-gate --require-cable for FPGA SRAM load (Closes #1309)
1385+
- **Files:** .claude/plans/wave-loop-404.md,.trinity/current-issue.md,.trinity/current_task/activity.md,.trinity/experience.md,cli/tri/src/fpga.rs,docs/NOW.md,docs/reports/FPGA_LOOP_COOPERATION_2026-07-07.md,docs/reports/FPGA_LOOP_EVIDENCE_2026-07-07.md,docs/reports/WAVE_LOOP_404_REPORT.md,fpga/HARDWARE_SSOT.md
1386+

‎.trinity/experience.md‎

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,51 @@
11
# t27 / Trinity Agent Experience Log
22

3+
## 2026-07-06 — Wave Loop 404 (Hardware smoke-gate `--require-cable`)
4+
5+
### What worked
6+
- Checking the bench before choosing the variant changed the wave outcome: the
7+
Digilent FTDI cable and XC7A200T board were reachable, so **Variant C**
8+
(hardware smoke gate) became feasible instead of another no-hardware formal
9+
extension.
10+
- Keeping `--require-cable` as an **optional** flag preserved the board-less
11+
default path. CI without a cable still passes all static checks; a runner
12+
with hardware can opt into the SRAM load assertion.
13+
- Reusing the existing `load_sram` and `capture_stat` helpers kept the change
14+
small and avoided duplicating openFPGALoader parsing logic.
15+
- Asserting the same `boot_success` conditions used by the Lean model
16+
(`DONE=1`, `MODE=0b001`, no CRC/ID/DEC errors) links the hardware smoke gate
17+
directly to the formal predicates.
18+
- On the bench: `openFPGALoader --detect` returned idcode `0x3636093`, SRAM
19+
load completed with `done 1`, and post-load STAT matched `0x401079FC`.
20+
- Conformance suite: **576/576 PASS**.
21+
22+
### What changed behavior
23+
- `cli/tri/src/fpga.rs`: `FpgaCmd::SmokeGate` now accepts `--require-cable`,
24+
`--cable`, and `--part`. When `--require-cable` is set, the gate runs
25+
`cable_detected`, `load_sram`, `capture_stat`, and `assert_stat_boot_success`
26+
before the existing board-less checks.
27+
- `fpga/HARDWARE_SSOT.md` §3.2 now references the hardware smoke traceability.
28+
- `docs/NOW.md` updated with the W404 entry.
29+
- Close-out artifacts: `docs/reports/WAVE_LOOP_404_REPORT.md`,
30+
`FPGA_LOOP_EVIDENCE_2026-07-07.md`, and
31+
`FPGA_LOOP_COOPERATION_2026-07-07.md`.
32+
33+
### Patterns to reuse
34+
- Probe hardware availability at the start of a wave; it can change which
35+
variant is highest leverage.
36+
- Add optional hardware gates as `--require-<resource>` flags so board-less CI
37+
stays green while physical evidence can be collected when a resource is present.
38+
- Reuse existing command helpers (`load_sram`, `capture_stat`) instead of
39+
spawning openFPGALoader ad-hoc; this keeps parsing and error handling
40+
consistent.
41+
42+
### Anti-patterns to avoid
43+
- Do not make a hardware gate mandatory unless the normal CI environment is
44+
guaranteed to have the resource. A broken cable should fail the specific
45+
check, not the whole pipeline.
46+
- Do not skip the board-less path when adding hardware coverage; the static
47+
audit is still the regression barrier that runs on every PR.
48+
349
## 2026-07-05 — Wave Loop 403 (Bitstream config linked to cold-POR decision tree)
450

551
### What worked

‎cli/tri/src/fpga.rs‎

Lines changed: 93 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -217,13 +217,26 @@ pub enum FpgaCmd {
217217
///
218218
/// Asserts the canonical 200T configuration: IDCODE 0x03636093, SPI x1,
219219
/// CCLK startup, OSCFSEL=0, and no CRC register writes.
220+
///
221+
/// With `--require-cable`, also detect the Digilent FTDI cable, load the
222+
/// bitstream into FPGA SRAM via openFPGALoader, and assert DONE=HIGH.
220223
SmokeGate {
221224
/// Bitstream to audit (default: fpga/verilog/ternary_mac_demo_top_200t.bit).
222225
#[arg(long)]
223226
bit: Option<PathBuf>,
224227
/// Verilog top module to synthesize (default: ternary_mac_demo_top).
225228
#[arg(long, default_value = "ternary_mac_demo_top")]
226229
top: String,
230+
/// Require a connected Digilent cable and load the bitstream into SRAM.
231+
/// If no device is detected, the gate fails. Board-less checks still run.
232+
#[arg(long)]
233+
require_cable: bool,
234+
/// openFPGALoader cable profile for the cable-connected check.
235+
#[arg(long, default_value = "digilent_hs2")]
236+
cable: String,
237+
/// FPGA part/package for openFPGALoader (default: xc7a200tfgg676).
238+
#[arg(long, default_value = "xc7a200tfgg676")]
239+
part: String,
227240
},
228241
/// Print or interactively confirm the cold-POR boot protocol. This is the
229242
/// standalone version of the instructions embedded in `boot-log` and
@@ -524,7 +537,13 @@ pub fn run(cmd: &FpgaCmd) -> Result<()> {
524537
wait_seconds,
525538
log_dir,
526539
} => boot_log(bit, cable, part, bridge.as_ref(), *freq, *repeat, *wait_seconds, log_dir.as_ref()),
527-
FpgaCmd::SmokeGate { bit, top } => smoke_gate(bit.as_ref(), top),
540+
FpgaCmd::SmokeGate {
541+
bit,
542+
top,
543+
require_cable,
544+
cable,
545+
part,
546+
} => smoke_gate(bit.as_ref(), top, *require_cable, cable, part),
528547
FpgaCmd::BootProtocol { checklist } => boot_protocol(*checklist),
529548
FpgaCmd::PatchCor0 { bit, out, oscfsel } => patch_cor0(bit, out, *oscfsel),
530549
FpgaCmd::CclkVariants { bit, output_dir, values } => {
@@ -2636,15 +2655,86 @@ fn boot_log(
26362655
}
26372656
}
26382657

2639-
fn smoke_gate(bit: Option<&PathBuf>, top: &str) -> Result<()> {
2658+
/// Detect whether a target FPGA is reachable on the given openFPGALoader
2659+
/// cable profile. Returns false when the chain is empty / cable missing.
2660+
fn cable_detected(cable: &str) -> bool {
2661+
let Ok((_, Some(output))) = run_openfpgaloader(cable, &["--detect"], true) else {
2662+
return false;
2663+
};
2664+
output.contains("idcode")&& output.contains("manufacturer")
2665+
}
2666+
2667+
/// Assert that the decoded STAT register shows a successful boot/config.
2668+
fn assert_stat_boot_success(bits: &StatBits, ctx: &str) -> Result<()> {
2669+
if !bits.done {
2670+
bail!("{}: DONE=LOW (raw=0x{:08X}, {})", ctx, bits.raw, bits.diagnose());
2671+
}
2672+
if bits.mode != 0b001 {
2673+
bail!(
2674+
"{}: MODE=0b{:03b} != 0b001 (Master SPI x1)",
2675+
ctx,
2676+
bits.mode
2677+
);
2678+
}
2679+
if bits.crc_error {
2680+
bail!("{}: CRC_ERROR=1", ctx);
2681+
}
2682+
if bits.id_error {
2683+
bail!("{}: ID_ERROR=1", ctx);
2684+
}
2685+
if bits.dec_error {
2686+
bail!("{}: DEC_ERROR=1", ctx);
2687+
}
2688+
Ok(())
2689+
}
2690+
2691+
fn smoke_gate(
2692+
bit: Option<&PathBuf>,
2693+
top: &str,
2694+
require_cable: bool,
2695+
cable: &str,
2696+
part: &str,
2697+
) -> Result<()> {
26402698
let root = repo_root()?;
26412699
let bit_path = bit.cloned().unwrap_or_else(|| {
26422700
root.join("fpga")
26432701
.join("verilog")
26442702
.join("ternary_mac_demo_top_200t.bit")
26452703
});
26462704

2647-
println!("== FPGA board-less smoke gate ==");
2705+
println!("== FPGA smoke gate ==");
2706+
2707+
// Cable-connected hardware check (optional, gated by --require-cable).
2708+
if require_cable {
2709+
println!("[smoke-gate] require-cable: detecting FPGA via {}...", cable);
2710+
if !cable_detected(cable) {
2711+
bail!(
2712+
"no FPGA detected on cable {} (is the board powered and connected?)",
2713+
cable
2714+
);
2715+
}
2716+
println!("[smoke-gate] cable OK (FPGA detected)");
2717+
2718+
if !bit_path.is_file() {
2719+
bail!(
2720+
"bitstream not found at {} (required for --require-cable)",
2721+
bit_path.display()
2722+
);
2723+
}
2724+
2725+
println!(
2726+
"[smoke-gate] loading SRAM: {}",
2727+
bit_path.display()
2728+
);
2729+
load_sram(&bit_path, cable, part, false, false)?;
2730+
2731+
println!("[smoke-gate] reading STAT after SRAM load...");
2732+
let samples = capture_stat(cable, false, 1)?;
2733+
let bits = samples.first().cloned().expect("at least one STAT sample");
2734+
assert_stat_boot_success(&bits, "SRAM load")
2735+
.with_context(|| "hardware smoke-gate failed after SRAM load")?;
2736+
println!("[smoke-gate] hardware check OK (DONE=HIGH, mode=001, no errors)");
2737+
}
26482738

26492739
// 1. bit-config audit if the bitstream exists.
26502740
if bit_path.is_file() {

‎docs/NOW.md‎

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,13 @@
11
# NOW -- Trinity t27 sync
22

3-
Last updated: 2026-07-05
3+
Last updated: 2026-07-06
4+
5+
## w404-fpga-smoke-gate-cable -- add `--require-cable` hardware smoke gate (Closes #1309)
6+
7+
- **WHERE**: `cli/tri/src/fpga.rs`, `fpga/HARDWARE_SSOT.md`, close-out reports.
8+
- **WHAT**: Extended `tri fpga smoke-gate` with `--require-cable` mode. When the Digilent FTDI cable and XC7A200T board are connected, the gate detects the JTAG chain, loads the canonical bitstream into FPGA SRAM via openFPGALoader, captures STAT, and asserts `DONE=HIGH`, `MODE=0b001`, no CRC/ID/DEC errors — the same predicate the Lean model calls `boot_success`. Verified on the bench: idcode `0x3636093` detected, SRAM load completes with `done 1`, post-load STAT = `0x401079FC`. Board-less checks (bit-config audit, dry-run CCLK sweep, yosys synthesis) remain mandatory and still pass without hardware. Physical CCLK measurement on P12 (Variant A) still deferred — no logic analyzer/oscilloscope available. Conformance suite `576/576 PASS`.
9+
- **Why**: turns the board-less static audit into an end-to-end hardware smoke test, gives CI an optional cable-connected gate, and adds another physical evidence layer that formal-HDL competitors would have to reproduce.
10+
- **Anchor**: phi^2 + phi^-2 = 3
411

512
## w403-fpga-bitstream-config-lean4 -- extend Lean 4 formal model to bitstream configuration (Closes #1307)
613

0 commit comments

Comments
 (0)