diff --git a/benches/gust/silicon/RESULTS-wdg-f100.md b/benches/gust/silicon/RESULTS-wdg-f100.md new file mode 100644 index 0000000..17fd34c --- /dev/null +++ b/benches/gust/silicon/RESULTS-wdg-f100.md @@ -0,0 +1,61 @@ +# wdg-thin — SECOND DIE: STM32F100 (VLDISCOVERY), Cortex-M3 (2026-07-29) + +The **same** dissolved `wdg-thin-cm3.o` that fired the watchdog on the NUCLEO-G474RE +(Cortex-M4) also fires it on an **STM32F100 / Cortex-M3** — a different family, a +different die, and the architecture the object was actually compiled for +(`synth --target cortex-m3`). On the G4 it runs as thumbv7m ⊂ thumbv7em; here it runs +natively. + +Nothing about the driver was rebuilt for this: the wasm, the dissolve, and the `.o` +are identical. Only `memory.x` (flash/RAM geometry) and the firmware's target feature +differ, and neither touches the driver. + +## Captured evidence + +Two consecutive runs, `wdg-f100-run{1,2}.log`, identical in outcome: + + gust-wdg-silicon: boot 1 on STM32F100 (RCC_CSR=0x14000000, no prior WDG reset). + Arming the REAL IWDG @0x40003000 via the dissolved wdg-thin driver + (PR=5, RLR=0x123 ≈ 1.2 s)... + gust-wdg-silicon: armed (last KR write=0x0000, is_running=1). NOT refreshing — + expect a HARDWARE reset in ~1.2 s, after which boot 2 reads IWDGRSTF=1. + gust-wdg-silicon OK: IWDG watchdog reset CONFIRMED on real STM32F100 silicon + (RCC_CSR=0x34000000, IWDGRSTF=1) — the dissolved wdg-thin driver armed the + hardware watchdog and it fired the reset. + +`RCC_CSR` 0x14000000 → 0x34000000: bit 29 (`IWDGRSTF`) set by the hardware. + +## Why this run is better evidence than the G474RE one + +- **One continuous session, not two.** The G474RE capture is two `probe-rs` + invocations, because the watchdog reset kills the probe-rs session — boot 1 and + boot 2 had to be reported as separate takes. Here openocd holds the SWD session + across the reset, so boot 1 → hardware reset → boot 2 is a **single unspliced + capture**. The reset is observed in-line, not inferred from a reconnect. +- **The reset flags are cleared by the harness immediately before the run** + (`mww 0x40021024 0x01000000`, RMVF), and the CPU is started with a software reset + (`SYSRESETREQ`), which sets `SFTRSTF` — *not* `IWDGRSTF`. So a set `IWDGRSTF` at + boot 2 cannot be stale. +- **Reproduced twice**, back to back, byte-identical outcome. + +## Scope / honesty + +- This is a **second die** for the same happy path, not a new property. It evidences + portability of the dissolved object and reproduces the arm→fire effect. It does + **not** evidence `p2_cannot_un_start` — the firmware still never attempts an + un-start (see `RESULTS-wdg-g474re.md`). +- **~1.2 s remains the configured timeout**, computed from PR=5 / RLR=0x123 against a + nominal ~32 kHz LSI. It is not measured here either; the LSI is spec'd loose and the + F1 and G4 LSIs are different parts. +- Portability holds here because the **IWDG is register-identical** across the STM32 + line. It does not generalise: adc/dac/i2c/can/pwm use family-specific register maps. +- The cross-*architecture* claim is narrower still. The same wasm dissolves to + RISC-V only for import-free modules; `synth` 0.49.0 cannot yet emit a relocatable + RISC-V object for a module with imports (`external call without relocation table`), + so no thin-seam driver dissolves to RISC-V today. Filed upstream as synth#871. + What is demonstrated here is **one wasm → one Cortex-M object → two different STM32 + dies**. + +## Reproduce + + benches/gust/silicon/run-wdg-f100.sh # needs an ST-LINK + openocd diff --git a/benches/gust/silicon/RESULTS-wdg-g474re.md b/benches/gust/silicon/RESULTS-wdg-g474re.md index 5d2e7d5..f32d09e 100644 --- a/benches/gust/silicon/RESULTS-wdg-g474re.md +++ b/benches/gust/silicon/RESULTS-wdg-g474re.md @@ -32,10 +32,25 @@ reset source. A silently-no-op'd start (KR=0xCCCC) would never reset, so the tes cannot false-pass. ## Scope / honesty -- This validates the wdg driver's IWDG programming + the cannot-un-start effect - **on real silicon** — the strongest evidence tier (above the qemu probe + Renode - content-gate). The Kani proofs (7/7) remain the source-level guarantee; this shows - the *dissolved object* drives real hardware to the real effect. +- This validates the wdg driver's IWDG **unlock → configure → lock → start** key + sequence **on real silicon** — the strongest evidence tier (above the qemu probe + + Renode content-gate). The Kani proofs (7/7) remain the source-level guarantee; this + shows the *dissolved object* drives real hardware to the real effect. +- **NOT evidenced here: cannot-un-start.** An earlier revision of this file claimed + this run validated "the cannot-un-start effect on real silicon". It does not, and the + claim has been withdrawn. `gust_wdg_silicon.rs` arms the watchdog and then simply + stops refreshing it; it never *attempts* an un-start, so nothing on silicon exercised + a rejection path. `p2_cannot_un_start` is a source-level Kani property over the pure + FSM and stays exactly that. What this run evidences is one happy path, once, on one + die: the dissolved object emitted a key sequence the real IWDG accepted, and the + hardware fired. (`RESULTS` also records a second session at + `RCC_CSR=0x14000000 → 0x34000000`, so the effect has reproduced across runs. It has + since also reproduced on a **second die of a different family** — the same `.o` on an + STM32F100/Cortex-M3, twice, in one unspliced session: see `RESULTS-wdg-f100.md`.) +- The stated **~1.2 s** is the *configured* timeout computed from PR=5 / RLR=0x123 + against a nominal ~32 kHz LSI — it is not a measured interval, and the LSI is spec'd + loose. The captured probe-rs log shows a much longer wall-clock gap before the + session drops (host detection latency), so no timing claim should be read off it. - Only the **IWDG** is register-portable F1→G4. adc/dac/i2c/can/pwm use F1-specific register maps → faithful silicon needs an STM32F1 board (VLDISCOVERY) or a G4 re-target; those remain qemu/Renode-validated for now. diff --git a/benches/gust/silicon/run-wdg-f100.sh b/benches/gust/silicon/run-wdg-f100.sh new file mode 100755 index 0000000..34d34de --- /dev/null +++ b/benches/gust/silicon/run-wdg-f100.sh @@ -0,0 +1,54 @@ +#!/usr/bin/env bash +# wdg-thin on real STM32F100 silicon (VLDISCOVERY, ST-LINK/V1) — see RESULTS-wdg-f100.md +# +# Boot 1 arms the real IWDG through the dissolved wdg-thin object and stops refreshing +# it; the hardware resets the chip; boot 2 reads IWDGRSTF=1. openocd holds the SWD +# session across the reset, so the whole thing is one capture. +# +# The firmware prints via semihosting, so openocd must stay attached — this is not a +# flash-and-walk-away run. +# +# Env: +# OCD_HOST run openocd over ssh on this host (e.g. pi@192.168.178.88); local if unset +set -euo pipefail +cd "$(dirname "$0")/.." + +ELF=target/thumbv7m-none-eabi/release/gust_wdg_silicon +RCC_CSR=0x40021024 # STM32F1 reset/clock control — status +RMVF=0x01000000 # clear the reset flags +AIRCR=0xE000ED0C +SYSRESETREQ=0x05FA0004 + +echo "==> building for F100 (only memory.x and the target feature differ; the driver .o does not)" +cp memory.x /tmp/memory.x.bak +cp targets/generated/memory-stm32f100.x memory.x +trap 'cp /tmp/memory.x.bak memory.x' EXIT +rm -f "$ELF" # force a relink at 0x08000000 +touch src/bin/gust_wdg_silicon.rs +cargo build --release --bin gust_wdg_silicon \ + --no-default-features --features target-f100 --target thumbv7m-none-eabi + +OCD=(openocd -f interface/stlink-hla.cfg -c "transport select swd" + -f target/stm32f1x.cfg -c "reset_config none separate") + +run_ocd() { # run_ocd + if [ -n "${OCD_HOST:-}" ]; then + # shellcheck disable=SC2029 + ssh "$OCD_HOST" "sudo timeout 25 $(printf '%q ' "${OCD[@]}" "$@")" + else + sudo timeout 25 "${OCD[@]}" "$@" + fi +} + +if [ -n "${OCD_HOST:-}" ]; then scp "$ELF" "$OCD_HOST:/tmp/wdg_f100.elf"; FW=/tmp/wdg_f100.elf +else FW="$ELF"; fi + +echo "==> flashing" +run_ocd -c init -c "program $FW verify" -c exit + +echo "==> arming (flags cleared first, so IWDGRSTF at boot 2 cannot be stale)" +run_ocd -c init -c "arm semihosting enable" -c halt \ + -c "mww $RCC_CSR $RMVF" -c "mww $AIRCR $SYSRESETREQ" -c halt -c resume \ + 2>&1 | grep --line-buffered "gust-wdg-silicon" || true + +echo "==> expected: RCC_CSR 0x14000000 -> 0x34000000, IWDGRSTF=1" diff --git a/benches/gust/silicon/wdg-f100-run1.log b/benches/gust/silicon/wdg-f100-run1.log new file mode 100644 index 0000000..457de94 --- /dev/null +++ b/benches/gust/silicon/wdg-f100-run1.log @@ -0,0 +1,3 @@ +gust-wdg-silicon: boot 1 on STM32F100 (RCC_CSR=0x14000000, no prior WDG reset). Arming the REAL IWDG @0x40003000 via the dissolved wdg-thin driver (PR=5, RLR=0x123 ≈ 1.2 s)... +gust-wdg-silicon: armed (last KR write=0x0000, is_running=1). NOT refreshing — expect a HARDWARE reset in ~1.2 s, after which boot 2 reads IWDGRSTF=1. +gust-wdg-silicon OK: IWDG watchdog reset CONFIRMED on real STM32F100 silicon (RCC_CSR=0x34000000, IWDGRSTF=1) — the dissolved wdg-thin driver armed the hardware watchdog and it fired the reset. diff --git a/benches/gust/silicon/wdg-f100-run2.log b/benches/gust/silicon/wdg-f100-run2.log new file mode 100644 index 0000000..457de94 --- /dev/null +++ b/benches/gust/silicon/wdg-f100-run2.log @@ -0,0 +1,3 @@ +gust-wdg-silicon: boot 1 on STM32F100 (RCC_CSR=0x14000000, no prior WDG reset). Arming the REAL IWDG @0x40003000 via the dissolved wdg-thin driver (PR=5, RLR=0x123 ≈ 1.2 s)... +gust-wdg-silicon: armed (last KR write=0x0000, is_running=1). NOT refreshing — expect a HARDWARE reset in ~1.2 s, after which boot 2 reads IWDGRSTF=1. +gust-wdg-silicon OK: IWDG watchdog reset CONFIRMED on real STM32F100 silicon (RCC_CSR=0x34000000, IWDGRSTF=1) — the dissolved wdg-thin driver armed the hardware watchdog and it fired the reset.