pulseengine · avrabe · Jul 23, 2026 · Jul 23, 2026
diff --git a/benches/gust/Cargo.toml b/benches/gust/Cargo.toml
@@ -27,6 +27,13 @@ default = ["target-g474re"]
 target-g474re = []
 target-f100 = []
 
+# gust_adc_silicon reads Vrefint (an F1 internal channel, ch17) — F100-only, so it
+# is built ONLY under target-f100 (otherwise the default target-g474re build would
+# hit its compile_error). All other bins auto-discover from src/bin/ as usual.
+[[bin]]
+name = "gust_adc_silicon"
+required-features = ["target-f100"]
+
 [profile.release]
 panic = "abort"
 opt-level = "z"

diff --git a/benches/gust/build.rs b/benches/gust/build.rs
@@ -342,6 +342,9 @@ fn main() {
     if aobj.exists() {
         println!("cargo:rustc-link-arg-bin=gust_adc={}", aobj.display());
         println!("cargo:rustc-link-arg-bin=gust_adc_probe={}", aobj.display());
+        // gust_adc_silicon points the SAME dissolved .o at the real F100 ADC1 to read
+        // Vrefint (ch17) on hardware — the silicon anchor for the adc-thin driver.
+        println!("cargo:rustc-link-arg-bin=gust_adc_silicon={}", aobj.display());
         println!("cargo:rerun-if-changed={}", aobj.display());
     }
 

diff --git a/benches/gust/silicon/RESULTS-f100.md b/benches/gust/silicon/RESULTS-f100.md
@@ -44,3 +44,48 @@ work unchanged.
 _Toolchain note: current pins are synth 0.49.0 / loom 1.2.0 (#208), not the synth
 0.15.0 dissolve measured above. `gust_mix` has not been re-measured on real F100
 silicon under 0.49; the ratio above is historical until that re-run happens._
+
+---
+
+## ADC / Vrefint on real F100 silicon — `gust_adc_silicon` (2026-07-23)
+
+The dissolved **adc-thin** driver (`adc-thin-cm3.o`, synth 0.49.0) reading the on-chip
+**Vrefint** (channel 17, the 1.20 V internal reference) on the physical STM32VLDISCOVERY
+— a self-contained silicon check, no external wiring. Firmware
+`src/bin/gust_adc_silicon.rs`, flash `silicon/run-adc.sh`.
+
+**Captured (openocd ST-LINK/V1 HLA via the Pi, semihosting):**
+```
+gust-adc-silicon: reading Vrefint (ch17) on real STM32F100 ADC1 @0x40012400 via the
+  dissolved adc-thin driver (TSVREFE carried through cr2_extra)...
+gust-adc-silicon OK: Vrefint = 1646 raw on real STM32F100 silicon — the dissolved
+  adc-thin driver read the internal channel through the real ADC. From the 1.20 V
+  nominal Vrefint this implies VDDA ≈ 2985 mV (VLDISCOVERY runs ~3.0 V; band
+  1450..1780, EOC cleared=true).
+```
+
+**What this anchors:**
+- The dissolved driver's **conversion lifecycle runs on real hardware**: `adc_enable →
+  adc_configure → adc_start → adc_poll(EOC) → adc_read(DR)` drives the real ADC1 and
+  returns a correct sample. `EOC cleared=true` = the driver's **read-after-EOC
+  exactly-once** property (the DR read consumes the sample and clears EOC) held on
+  silicon, not just in the qemu probe / Renode gate.
+- **Vrefint (an F1 internal channel) requires `CR2.TSVREFE`** during the conversion.
+  This is the payoff of the gale#216 fix: `TSVREFE` is threaded through the driver's
+  `cr2_extra` mask on every managed CR2 write, so the internal channel actually
+  connects. Before the fix the driver's absolute CR2 writes dropped it and this read
+  would have been a floating/near-zero garbage code.
+- **1646 raw ⇒ VDDA ≈ 2.985 V** (from Vrefint's 1.20 V factory nominal — the classic
+  "Vrefint measures the rail" use). This is exactly VLDISCOVERY's ~3.0 V VDD, and is
+  why a naive 3.3 V-ref expectation (~1489) undershoots — the board rail is 3.0 V, so
+  Vrefint reads ~1638. A 3.3 V-ref interpretation of 1646 would put Vrefint at 1.33 V,
+  above its 1.24 V spec max — impossible — which independently confirms the 3.0 V rail
+  and that the code really is Vrefint.
+
+**Silicon-vs-model note (tracked, gale#216):** the driver writes `CR2=ADON` in both
+`adc_enable` and `adc_configure`; on F1 a `1`-written-while-ADON=1 can kick a
+conversion, so on hardware `adc_configure` may trigger an extra ch17 conversion before
+`adc_start`. Both convert ch17/Vrefint, so the DR holds a valid sample either way (the
+1646 read confirms it) — but a strict single-shot on F1 would want the FSM to separate
+power-on from register config. Harmless for this single-channel read; noted for a
+follow-on refinement.
diff --git a/benches/gust/silicon/run-adc.sh b/benches/gust/silicon/run-adc.sh
@@ -0,0 +1,42 @@
+#!/usr/bin/env bash
+# gust-adc-silicon — flash + capture the REAL-hardware ADC anchor on an
+# STM32VLDISCOVERY (Cortex-M3 / STM32F100, thumbv7m). The dissolved adc-thin
+# driver reads the on-chip Vrefint (channel 17, 1.20 V internal reference) —
+# a self-contained silicon check needing no external wiring.
+#
+#   ./run-adc.sh            # build for f100 + flash via the Pi + capture semihosting
+#
+# The VLDISCOVERY's onboard ST-LINK/V1 has old firmware that openocd can only
+# drive via the HLA interface (interface/stlink-hla.cfg), and on macOS the V1
+# needs openocd-under-sudo — so the board hangs off a Raspberry Pi (PI_HOST)
+# which runs openocd and streams semihosting back over ssh.
+#
+# EXPECTED (self-checking):
+#   "gust-adc-silicon OK: Vrefint = <~1646> raw on real STM32F100 silicon ...
+#    implies VDDA ≈ <~2985> mV ..."   -> exit SUCCESS.
+# Vrefint is factory-nominal ≈ 1.20 V; the raw code depends on VDDA (≈3.0 V on
+# VLDISCOVERY → ~1638). A raw near 0 or full-scale = the internal channel was
+# not converted (TSVREFE / clock / calibration problem). See RESULTS-f100.md.
+set -euo pipefail
+PI_HOST="${PI_HOST:-pi@192.168.178.88}"
+HERE="$(cd "$(dirname "$0")" && pwd)"
+BENCH="$(dirname "$HERE")"   # benches/gust
+cd "$BENCH"
+
+cp memory.x /tmp/gust-memory.x.bak
+trap 'cp /tmp/gust-memory.x.bak "$BENCH/memory.x"' EXIT
+cp targets/generated/memory-stm32f100.x memory.x
+
+echo "== build gust_adc_silicon for f100 (thumbv7m, target-f100) =="
+cargo build --release --bin gust_adc_silicon \
+  --no-default-features --features target-f100 --target thumbv7m-none-eabi
+ELF="target/thumbv7m-none-eabi/release/gust_adc_silicon"
+
+echo "== copy ELF to $PI_HOST and flash via openocd (ST-LINK/V1 HLA) =="
+scp "$ELF" "$PI_HOST:/tmp/gust_adc_silicon.elf"
+# Benign 'SRST error' is expected — the V1 has no hardware reset line; openocd
+# falls back to sysresetreq, which works.
+ssh "$PI_HOST" 'timeout 45 openocd -f interface/stlink-hla.cfg -f target/stm32f1x.cfg \
+  -c "init" -c "reset halt" -c "arm semihosting enable" \
+  -c "program /tmp/gust_adc_silicon.elf verify" -c "reset run" \
+  -c "sleep 3000" -c "shutdown" 2>&1 | grep -iE "gust-adc|verified"'
diff --git a/benches/gust/src/bin/gust_adc_silicon.rs b/benches/gust/src/bin/gust_adc_silicon.rs
@@ -0,0 +1,182 @@
+//! gust-adc-silicon — REAL-HARDWARE anchor for the dissolved adc-thin driver.
+//!
+//! Unlike gust_adc_probe (qemu, a `[u32;24]` RAM window faking the ADC) and gust_adc
+//! (Renode content-gate), this firmware points the DISSOLVED adc-thin-cm3.o at the
+//! REAL STM32F100 ADC1 (0x4001_2400) and reads the on-chip **Vrefint** (channel 17,
+//! the 1.2 V internal reference) — a self-contained silicon check needing no external
+//! wiring. Flash + capture:  benches/gust/silicon/run-adc.sh
+//!
+//! Expected: Vrefint is factory-nominal ≈ 1.20 V (spec 1.16..1.24 V). The raw code
+//! depends on the board's VDDA reference: on the STM32VLDISCOVERY VDDA ≈ **3.0 V**
+//! (not 3.3 V) → raw ≈ 1.20/3.0*4095 ≈ **1638**. Rather than assume the rail, this
+//! anchor checks the raw is in the plausible Vrefint band and *reports the implied
+//! VDDA* back from the known 1.20 V (the classic "Vrefint measures VDDA" use): a raw
+//! near 0 or full-scale = the internal channel was not actually converted.
+//!
+//! Reading an F1 internal channel needs `CR2.TSVREFE` (bit 23) set *during* the
+//! conversion — which the driver's absolute CR2 writes used to drop (gale#216). Fixed
+//! by threading `cr2_extra = TSVREFE` through adc_enable/adc_configure/adc_start so the
+//! dissolved driver keeps TSVREFE on every managed CR2 write.
+//!
+//! Silicon-vs-model note: the driver writes CR2=ADON in BOTH adc_enable (wake) and
+//! adc_configure (config). On the RAM-window probe a repeated ADON write is inert; on
+//! real F1 a `1`-written-while-ADON=1 can kick a conversion. Both such conversions
+//! select ch17 (SQR3 is set before the configure CR2 write), so the DR holds a Vrefint
+//! sample regardless — this anchor's job is to confirm that empirically. A future
+//! refinement (separate power-on from register config in the FSM) would make it a
+//! strict single-shot on F1; tracked with gale#216.
+//!
+//! F1 ADC bring-up the FSM does NOT model (done here in firmware): enable the ADC1
+//! clock (RCC APB2ENR), wake + tSTAB, and RSTCAL/CAL self-calibration — all one-time,
+//! before the dissolved conversion lifecycle (enable→configure→start→poll→read).
+#![no_std]
+#![no_main]
+
+use core::ptr::{read_volatile, write_volatile};
+use cortex_m_rt::entry;
+use cortex_m_semihosting::{debug, hprintln};
+use panic_halt as _;
+
+// The mmio seam the dissolved driver imports — here it drives the REAL peripheral.
+#[no_mangle]
+pub extern "C" fn mmio_read32(addr: u32) -> u32 {
+    unsafe { read_volatile(addr as *const u32) }
+}
+#[no_mangle]
+pub extern "C" fn mmio_write32(addr: u32, val: u32) {
+    unsafe { write_volatile(addr as *mut u32, val) }
+}
+
+// The dissolved adc-thin driver (state-threaded FSM; cr2_extra carries TSVREFE).
+extern "C" {
+    fn adc_enable(base: u32, state: u32, channel: u32, cr2_extra: u32) -> u32;
+    fn adc_configure(base: u32, channel: u32, sample_code: u32, cr2_extra: u32);
+    fn adc_start(base: u32, state: u32, cr2_extra: u32) -> u32;
+    fn adc_poll(base: u32, state: u32) -> u32;
+    fn adc_read(base: u32, state: u32) -> u32;
+    fn adc_sample(state: u32) -> u32;
+}
+
+// ADC_BASE (0x4001_2400) + VREFINT_CH (17) are GENERATED from the AADL model
+// (benches/gust/targets/) — see gust-target-gen. F100 only (thumbv7m).
+#[cfg(not(feature = "target-f100"))]
+compile_error!("gust_adc_silicon: build with --no-default-features --features target-f100 (Vrefint is an F1/F100 internal channel)");
+#[cfg(feature = "target-f100")]
+#[path = "../../targets/generated/gust_target_stm32f100.rs"]
+#[allow(dead_code)]
+mod target;
+use target::{ADC_BASE, BOARD, VREFINT_CH};
+
+// STM32F1 ADC register offsets + bits (device knowledge as data, mirrors the driver).
+const CR2: u32 = 0x08;
+const SR: u32 = 0x00;
+const SR_EOC: u32 = 1 << 1;
+const CR2_ADON: u32 = 1 << 0;
+const CR2_CAL: u32 = 1 << 2;
+const CR2_RSTCAL: u32 = 1 << 3;
+const CR2_TSVREFE: u32 = 1 << 23; // enable the temp-sensor / Vrefint internal channels
+
+// RCC — enable the ADC1 peripheral clock. At reset the F100 runs on HSI 8 MHz, so
+// PCLK2 = 8 MHz and the default ADCPRE (/2) gives ADCCLK = 4 MHz (≤ 14 MHz) — no
+// prescaler change needed.
+const RCC_APB2ENR: u32 = 0x4002_1018;
+const RCC_APB2ENR_ADC1EN: u32 = 1 << 9;
+
+const SAMPLE_CODE: u32 = 7; // 239.5-cycle sample time — Vrefint needs a long Ts (≥17.1 µs)
+const ADC_FAULT: u32 = 0xFFFF_FFFF;
+
+// Vrefint (1.20 V nominal) raw band across a plausible VDDA of ~2.8..3.3 V: 1.20 V
+// reads 1489 (@3.3) .. 1755 (@2.8). VLDISCOVERY runs ~3.0 V → ~1638. A raw outside
+// this whole band means the internal channel was not converted (float/rail), not a
+// mere rail difference.
+const VREF_LO: u32 = 1450;
+const VREF_HI: u32 = 1780;
+const VREFINT_MV: u32 = 1200; // factory-nominal Vrefint, for the implied-VDDA report
+
+#[inline]
+fn rd(addr: u32) -> u32 {
+    unsafe { read_volatile(addr as *const u32) }
+}
+#[inline]
+fn wr(addr: u32, val: u32) {
+    unsafe { write_volatile(addr as *mut u32, val) }
+}
+#[inline(always)]
+fn delay(n: u32) {
+    for _ in 0..n {
+        cortex_m::asm::nop();
+    }
+}
+
+#[entry]
+fn main() -> ! {
+    hprintln!(
+        "gust-adc-silicon: reading Vrefint (ch{}) on real {} ADC1 @0x{:08x} via the \
+         dissolved adc-thin driver (TSVREFE carried through cr2_extra)...",
+        VREFINT_CH, BOARD, ADC_BASE
+    );
+
+    // --- F1 ADC bring-up the FSM does not model (one-time, firmware-side) ---
+    // 1) ADC1 peripheral clock.
+    wr(RCC_APB2ENR, rd(RCC_APB2ENR) | RCC_APB2ENR_ADC1EN);
+
+    // 2) Wake the ADC + select Vrefint through the dissolved driver: Off -> Ready,
+    //    CR2 = ADON | TSVREFE (first ADON write = power-up, no conversion).
+    let s1 = unsafe { adc_enable(ADC_BASE, 0, VREFINT_CH, CR2_TSVREFE) };
+    if s1 == ADC_FAULT {
+        hprintln!("gust-adc-silicon FAIL: adc_enable(ch{}) faulted", VREFINT_CH);
+        debug::exit(debug::EXIT_FAILURE);
+        loop {}
+    }
+    delay(2000); // tSTAB (~1 µs @ ADCCLK) with wide margin before calibration
+
+    // 3) Self-calibrate (RSTCAL then CAL), preserving ADON|TSVREFE. The driver does not
+    //    model calibration; it is standard F1 one-time bring-up in the Ready phase.
+    wr(ADC_BASE + CR2, CR2_ADON | CR2_TSVREFE | CR2_RSTCAL);
+    while rd(ADC_BASE + CR2) & CR2_RSTCAL != 0 {}
+    wr(ADC_BASE + CR2, CR2_ADON | CR2_TSVREFE | CR2_CAL);
+    while rd(ADC_BASE + CR2) & CR2_CAL != 0 {}
+
+    // --- dissolved conversion lifecycle: configure -> start -> poll -> read ---
+    // configure: SMPR1 ch17 = 239.5 cyc, SQR3 = 17, SQR1 len = 1, CR2 = ADON|TSVREFE.
+    unsafe { adc_configure(ADC_BASE, VREFINT_CH, SAMPLE_CODE, CR2_TSVREFE) };
+    // start: CR2 = ADON | SWSTART | TSVREFE -> conversion of ch17.
+    let s2 = unsafe { adc_start(ADC_BASE, s1, CR2_TSVREFE) };
+    if s2 == ADC_FAULT {
+        hprintln!("gust-adc-silicon FAIL: adc_start faulted (s1=0x{:08x})", s1);
+        debug::exit(debug::EXIT_FAILURE);
+        loop {}
+    }
+    // poll to EOC, then consume the sample (read-after-EOC exactly-once).
+    let s3 = unsafe { adc_poll(ADC_BASE, s2) };
+    let s4 = unsafe { adc_read(ADC_BASE, s3) };
+    let sample = unsafe { adc_sample(s4) };
+    let eoc = rd(ADC_BASE + SR) & SR_EOC; // should be cleared by the DR read
+
+    if s3 == ADC_FAULT || s4 == ADC_FAULT {
+        hprintln!("gust-adc-silicon FAIL: poll/read faulted (s3=0x{:08x} s4=0x{:08x})", s3, s4);
+        debug::exit(debug::EXIT_FAILURE);
+        loop {}
+    }
+
+    if sample >= VREF_LO && sample <= VREF_HI {
+        // Vrefint is known ≈ 1.20 V, so the sample implies VDDA = 1.20 V * 4095 / raw.
+        let vdda_mv = VREFINT_MV * 4095 / sample;
+        hprintln!(
+            "gust-adc-silicon OK: Vrefint = {} raw on real {} silicon — the dissolved \
+             adc-thin driver read the internal channel through the real ADC. From the \
+             1.20 V nominal Vrefint this implies VDDA ≈ {} mV (VLDISCOVERY runs ~3.0 V; \
+             band {}..{}, EOC cleared={}).",
+            sample, BOARD, vdda_mv, VREF_LO, VREF_HI, eoc == 0
+        );
+        debug::exit(debug::EXIT_SUCCESS);
+    } else {
+        hprintln!(
+            "gust-adc-silicon FAIL: Vrefint raw = {} outside {}..{} — internal channel \
+             not converted (TSVREFE/clock/calibration issue).",
+            sample, VREF_LO, VREF_HI
+        );
+        debug::exit(debug::EXIT_FAILURE);
+    }
+    loop {}
+}