park07/amradioFPGA-based 12-channel AM radio broadcast system with formal verification of a hardware watchdog for fail-safe emergency alert transmission in unmanned tunnels.
A 12-channel AM radio broadcast system using Red Pitaya FPGA for emergency alert transmission in unmanned tunnels.
Why AM radio in a tunnel? During construction and maintenance, vehicles with standard AM radios transit through tunnels that have no mobile coverage. AM signals propagate along tunnel structures via leaky feeder cables, and receivers are cheap, robust, and already present in every vehicle. The system broadcasts pre-recorded emergency alerts across multiple frequencies so that any AM radio tuned to any station in the band will receive the message. A hardware watchdog ensures RF output is killed if the control system fails — because automatically restarting a transmitter in an unmanned tunnel is not an acceptable failure mode.
| Feature | Status |
|---|---|
| 12 simultaneous carrier frequencies | ✅ |
| Runtime frequency configuration (no hardware changes) | ✅ |
| AM modulation with pre-recorded audio | ✅ |
| Dynamic power scaling | ✅ |
| MVC architecture (Rust + JavaScript) | ✅ |
| Event-driven pub/sub via event bus | ✅ |
| Stateless UI — device is source of truth | ✅ |
| Network polling & auto-reconnect | ✅ |
| Fail-safe hardware watchdog (5s timeout) | ✅ |
| Formal verification (14 properties, 6 covers, all proven) | ✅ |
model.rs): NetworkManager handles TCP/SCPI, device state, 500ms polling, auto-reconnect with exponential backoffview.js, index.html): Stateless — only renders confirmed device state. Never assumes hardware state.controller.js): Handles user input, publishes events to busevent_bus.rs, event_bus.js): Components communicate through a central bus instead of calling each other directly. Rust emits events to JS frontend via Tauri bridge.state_machine.rs): IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING. Intermediate states prevent invalid transitions.wd.v): Hardware fail-safe — if GUI heartbeat stops for 5 seconds, RF output is killed and latched. Only manual operator reset restores output.am_scpi_server.py): Runs on Red Pitaya, parses text commands, converts frequencies to phase increments, writes to FPGA registers via /dev/mem.GUI click → invoke("set_frequency") → model.rs sends "FREQ:CH1 700000" over TCP
→ am_scpi_server.py converts to phase_inc = (700000 × 2³²) / 125MHz
→ writes to FPGA register via /dev/mem → NCO generates carrier → AM modulates → RF output
The watchdog timer is mathematically proven correct using bounded model checking and k-induction (SymbiYosys + Z3 SMT solver). Unlike simulation-based testing which checks individual scenarios, formal verification proves correctness across every possible input, in every possible state, for all time.
| Category | # | Property | Guarantee |
|---|---|---|---|
| Basic | 1 | Reset clears all | !rstn → counter=0, triggered=0, warning=0 |
| 2 | Heartbeat prevents trigger | Heartbeat resets counter, clears triggered and warning | |
| 6 | Disable kills everything | !enable → all outputs cleared | |
| 7 | Counter bounded | Counter never exceeds TIMEOUT_CYCLES | |
| 8 | Force reset works | force_reset clears all state | |
| 9 | Warning low before threshold | counter < WARNING_CYCLES → warning=0 | |
| Safety | 3 | No early trigger | triggered ONLY when counter ≥ TIMEOUT_CYCLES |
| 4 | Trigger guaranteed at timeout | Liveness: timeout always fires trigger | |
| 5 | Warning before trigger | triggered=1 → warning=1 | |
| 5b | Contrapositive | !warning → !triggered | |
| 10 | Warning high in zone | counter > WARNING_CYCLES → warning=1 | |
| 11 | Counter increments correctly | Exactly +1 per clock cycle during counting | |
| Output | 12 | time_remaining at zero | counter=0 → time_remaining = TIMEOUT_SEC |
| 13 | time_remaining at trigger | triggered → time_remaining = 0 | |
| 14 | time_remaining monotonic | Decreases every cycle during counting |
| # | Scenario | Steps | Description |
|---|---|---|---|
| 1 | Trigger fires | 23 | Counter reaches timeout |
| 2 | Warning without trigger | 21 | In warning zone, not yet timed out |
| 3 | Exact timeout boundary | 22 | Counter = TIMEOUT_CYCLES exactly |
| 4 | Last-second heartbeat | 19 | Heartbeat at counter = T-1 |
| 5 | Recovery from triggered | 24 | Triggered state cleared by force_reset |
| 6 | Warning-to-trigger lifecycle | 23 | Warning then immediate trigger |
cd fpga/formal/
sby -f wd.sby
Expected output:
SBY [wd_prove] DONE (PASS, rc=0)
summary: successful proof by k-induction.
SBY [wd_cover] DONE (PASS, rc=0)
summary: 6/6 cover statements reached.
Verification uses CLK_FREQ=1, TIMEOUT_SEC=5 to keep state space tractable. Production uses CLK_FREQ=125000000. The RTL is parameterised — same if/else logic, same state transitions. Proof at reduced scale implies correctness at production scale.
fpga/formal/README.md| Dependency | macOS | Windows |
|---|---|---|
| Rust + Cargo | curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh | Download rustup-init.exe from rustup.rs |
| Node.js (LTS) | brew install node or nodejs.org | nodejs.org |
| Xcode Command Line Tools (macOS only) | xcode-select --install | — |
| Visual Studio Build Tools (Windows only) | — | Download — select "Desktop development with C++" |
git clone https://github.com/Park07/amradio.git
cd amradio/am_radio
# Install Rust (if not installed)
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
source $HOME/.cargo/env
# Install Xcode CLI tools (if not installed)
xcode-select --install
# Install Node.js via Homebrew (if not installed)
brew install node