Finding
The dissolved thin-seam ADC driver (benches/gust/drivers/adc-thin) writes ADC_CR2 absolutely, never OR-preserving other bits:
adc_enable → CR2 = ADON (lib.rs:280)adc_configure → CR2 = ADON (lib.rs:271)adc_start → CR2 = ADON | SWSTART (lib.rs:293)
On STM32F1, reading an internal channel — Vrefint (ch17) or the temperature sensor (ch16) — requires CR2.TSVREFE (bit 23) to be set during the conversion, because TSVREFE gates the analog switch connecting the internal source to the ADC mux. Sampling begins after the SWSTART write, so if TSVREFE is not present in the adc_start CR2 value, the internal source is disconnected during sample-and-hold and the reading is garbage.
Because adc_start's write is ADON | SWSTART (bit 23 = 0), any TSVREFE a caller set beforehand is cleared at the exact instant conversion is triggered. Net: the driver as verified cannot drive F1 internal channels.
Impact
Blocks the v0.5.0 workstream-D silicon anchor gust_adc_silicon reading Vrefint on the physical STM32F100 (the self-contained, no-wiring silicon check). The F100 target-model support for ADC/Vrefint landed in #215 (generated ADC_BASE/VREFINT_CH consts); the firmware+flash step is what this blocks.
Not hacking around it
Setting TSVREFE and racing to keep it set during a slow sample window is non-deterministic and not acceptable for a silicon anchor. Reading an external channel needs a known reference voltage / wiring the bare VLDISCOVERY doesn't provide, so it can't assert an expected value self-containedly.
Fix options (each needs Kani re-verify + regenerated adc-thin-cm3.o)
- Caller-supplied CR2 mask (preferred, generic): thread a
cr2_extra: u32 through adc_configure/adc_start (and adc_enable) that is OR'd into every CR2 write. Covers TSVREFE, ALIGN, EXTSEL/EXTTRIG, DMA — not just Vrefint. Keeps the managed bits (ADON/SWSTART/CONT) authoritative; extends the FSM's write model to CR2 = managed | extra.
- Read-modify-write CR2:
CR2 = (rd(CR2) & KEEP) | managed. Smaller signature change but couples the driver to prior register state (less clean for the verified model; RMW under the FSM needs care).
Option 1 is the more honest generic seam. The verification obligations (single-shot, read-after-EOC, phase-gating) are unaffected by an opaque OR-mask on the CR2 writes.
Provenance
Confirmed from source (lib.rs:271/280/293) this session; no TSVREFE reference exists anywhere in the driver or firmware. Filed as design friction per the feature-loop "surface, don't work around" rule.
Finding
The dissolved thin-seam ADC driver (
benches/gust/drivers/adc-thin) writesADC_CR2absolutely, never OR-preserving other bits:adc_enable→CR2 = ADON(lib.rs:280)adc_configure→CR2 = ADON(lib.rs:271)adc_start→CR2 = ADON | SWSTART(lib.rs:293)On STM32F1, reading an internal channel — Vrefint (ch17) or the temperature sensor (ch16) — requires
CR2.TSVREFE(bit 23) to be set during the conversion, because TSVREFE gates the analog switch connecting the internal source to the ADC mux. Sampling begins after the SWSTART write, so if TSVREFE is not present in theadc_startCR2 value, the internal source is disconnected during sample-and-hold and the reading is garbage.Because
adc_start's write isADON | SWSTART(bit 23 = 0), any TSVREFE a caller set beforehand is cleared at the exact instant conversion is triggered. Net: the driver as verified cannot drive F1 internal channels.Impact
Blocks the v0.5.0 workstream-D silicon anchor
gust_adc_siliconreading Vrefint on the physical STM32F100 (the self-contained, no-wiring silicon check). The F100 target-model support for ADC/Vrefint landed in #215 (generatedADC_BASE/VREFINT_CHconsts); the firmware+flash step is what this blocks.Not hacking around it
Setting TSVREFE and racing to keep it set during a slow sample window is non-deterministic and not acceptable for a silicon anchor. Reading an external channel needs a known reference voltage / wiring the bare VLDISCOVERY doesn't provide, so it can't assert an expected value self-containedly.
Fix options (each needs Kani re-verify + regenerated
adc-thin-cm3.o)cr2_extra: u32throughadc_configure/adc_start(andadc_enable) that is OR'd into every CR2 write. Covers TSVREFE, ALIGN, EXTSEL/EXTTRIG, DMA — not just Vrefint. Keeps the managed bits (ADON/SWSTART/CONT) authoritative; extends the FSM's write model toCR2 = managed | extra.CR2 = (rd(CR2) & KEEP) | managed. Smaller signature change but couples the driver to prior register state (less clean for the verified model; RMW under the FSM needs care).Option 1 is the more honest generic seam. The verification obligations (single-shot, read-after-EOC, phase-gating) are unaffected by an opaque OR-mask on the CR2 writes.
Provenance
Confirmed from source (lib.rs:271/280/293) this session; no TSVREFE reference exists anywhere in the driver or firmware. Filed as design friction per the feature-loop "surface, don't work around" rule.