Show HN: Formally verified FPGA watchdog for AM broadcast in unmanned tunnels

Hacker News · Feb 18, 2026 · Collected from RSS

Full Article

AM Radio Break-in System A 12-channel AM radio broadcast system using Red Pitaya FPGA for emergency alert transmission in unmanned tunnels. Features 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) ✅ Architecture Software Layer Framework: Rust (Tauri) backend + JavaScript frontend Architecture: MVC with event-driven pub/sub Model (model.rs): NetworkManager handles TCP/SCPI, device state, 500ms polling, auto-reconnect with exponential backoff View (view.js, index.html): Stateless — only renders confirmed device state. Never assumes hardware state. Controller (controller.js): Handles user input, publishes events to bus Event Bus (event_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 (state_machine.rs): IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING. Intermediate states prevent invalid transitions. Source of Truth: The device, not the software. UI only updates after hardware confirms. Hardware Layer NCO: 12 Numerically Controlled Oscillators generate carrier frequencies (505–1605 kHz) AM Modulator: Combines audio source with each carrier Dynamic Scaling: Output power adjusts based on enabled channel count Audio Buffer: BRAM stores pre-recorded emergency messages (16,384 sample buffer at ~5 kHz playback rate). AXI audio loader available for runtime loading. Watchdog Timer (wd.v): Hardware fail-safe — if GUI heartbeat stops for 5 seconds, RF output is killed and latched. Only manual operator reset restores output. SCPI Server (am_scpi_server.py): Runs on Red Pitaya, parses text commands, converts frequencies to phase increments, writes to FPGA registers via /dev/mem. Signal Generation Flow 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 Formal Verification 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. 14 Safety Properties (All PASS) 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 6 Cover Scenarios (All Reached) # 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 Running Verification 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. Scalability 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. See fpga/formal/README.md Requirements Hardware Red Pitaya STEMlab 125-10 AM Radio receiver(s) for testing Ethernet cable (for Red Pitaya connection) Software 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++" Formal Verification (optional) SymbiYosys Yosys Z3 SMT solver Installation 1. Clone the repository git clone https://github.com/Park07/amradio.git cd amradio/ugl_am_radio 2. Build the GUI macOS # 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 # Build cd gui npm install npm run build The built .app will be in gui/src-tauri/target/release/bundle/macos/. Windows (PowerShell) # 1. Install Rust # Download and run rustup-init.exe from https://rustup.rs # Close and reopen PowerShell after install # 2. Install Visual Studio Build Tools # Download from https://visualstudio.microsoft.com/visual-cpp-build-tools/ # Select "Desktop development with C++" during installation # Close and reopen PowerShell after install # 3. Install Node.js # Download LTS from https://nodejs.org # Close and reopen PowerShell after install # 4. Verify installations rustc --version cargo --version node --version npm --version # 5. Build cd gui npm install npm run build The built .exe will be in gui\src-tauri\target\release\. Note: First build takes ~2–3 minutes (compiling Rust). Subsequent builds are faster. 3. Setup Red Pitaya SSH into the Red Pitaya: ssh root@<RED_PITAYA_IP> # Default password: root Copy required files: scp am_scpi_server.py root@<RED_PITAYA_IP>:/root/ scp axi_audio_sequence_loop.py root@<RED_PITAYA_IP>:/root/ scp alarm_fast.wav 0009_part1.wav 0009_part2_fast.wav root@<RED_PITAYA_IP>:/root/ scp fpga/red_pitaya_top.bit root@<RED_PITAYA_IP>:/root/ Note Bitstream is already on the Red Pitaya SD card from development. To rebuild: open project_William.xpr in Vivado, generate bitstream, then scp the new .bit file to the Red Pitaya. 4. Python Environment (Red Pitaya) The Red Pitaya runs Alpine Linux with Python 3.5. The SCPI server has no external dependencies (stdlib only). The audio loader requires numpy: # On Red Pitaya pip install numpy Note: The Red Pitaya's Python 3.5 does not support venv out of the box and runs as root, so packages are installed globally. This is fine — it's an embedded device, not a shared server. 5. Python Environment (Local Development — optional) If you want to run or modify the Python scripts locally (e.g. for testing audio processing without the Red Pitaya): python3 -m venv venv source venv/bin/activate # macOS/Linux # or .\venv\Scripts\activate # Windows PowerShell pip install -r requirements.txt Add venv/ to .gitignore if not already present. Audio Files The system plays three audio files in a loop: Alarm → Part 1 → Part 2 → (repeat). File Description Duration alarm_fast.wav Alarm tone ~4 sec 0009_part1.wav Emergency message part 1 ~3 sec 0009_part2_fast.wav Emergency message part 2 ~3.6 sec All audio is downsampled to ~5 kHz to fit within the FPGA's 16,384-sample BRAM buffer. The axi_audio_sequence_loop.py script handles resampling, 14-bit conversion, and sequential loading automatically. Usage You need three SSH terminals open to the Red Pitaya, plus one local terminal for the GUI. Note: The Red Pitaya's IP address may change each time it is powered on. Check your router's DHCP client list or use ping rp-f0866a.local to find it. Step 1: Connect to Red Pitaya Open a terminal and SSH in: ssh root@<RED_PITAYA_IP> # Password: root Step 2: Load the FPGA bitstream On the Red Pitaya (first SSH terminal): cat /root/red_pitaya_top.bit > /dev/xdevcfg This loads the AM radio design onto the FPGA. Required after every power cycle. Step 3: Start the SCPI server On the Red Pitaya (same or second SSH terminal): python3 /root/am_scpi_server.py Leave this running — it bridges TCP commands from the GUI to FPGA registers. Step 4: Start the audio loop Open a second SSH terminal to the Red Pitaya: ssh root@<RED_PITAYA_IP> sudo python3 /root/axi_audio_sequence_loop.py Expected output: ============================================================ AXI AUDIO SEQUENCE - AUTO LOOP Alarm -> Part 1 -> Part 2 -> (repeat) ============================================================ Buffer: 16384 samples FPGA playback rate: 5000 Hz Press Ctrl+C to stop ============================================================ Step 5: Run the GUI On your local machine: cd gui npm run dev Or run the built binary directly from src-tauri/target/release/. Step 6: Connect and broadcast Enter the Red Pitaya IP address Click Connect Enable desired channels (1–12) Adjust frequencies if needed Click START BROADCAST Tune an AM radio to any enabled frequency Vivado (for FPGA development only) If you need to modify the FPGA design and rebuild the bitstream, install Vivado 2020.1. Red Pitaya provides a setup guide here: https://redpitaya.readthedocs.io/en/latest/developerGuide/fpga/getting_started/vivado_install.html All basic Red Pitaya settings and tutori