Show HN: Formally verified FPGA watchdog for AM broadcast in unmanned tunnels
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
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
venvout 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.localto 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 tutorials are available on the Red Pitaya official documentation.
File Structure
ugl_am_radio/
├── gui/
│ ├── src/
│ │ ├── index.html # HTML + CSS
│ │ └── js/
│ │ ├── event_bus.js # Frontend pub/sub + Tauri listener
│ │ ├── model.js # Rust API calls (stateless)
│ │ ├── view.js # DOM rendering
│ │ └── controller.js # Event handlers
│ └── src-tauri/src/
│ ├── main.rs # Entry point
│ ├── model.rs # NetworkManager + DeviceState
│ ├── commands.rs # Tauri command bridge
│ ├── event_bus.rs # Rust pub/sub + Tauri emit
│ ├── state_machine.rs # Broadcast state transitions
│ └── config.rs # Constants
├── fpga/
│ ├── formal/
│ │ ├── wd.v # Watchdog + 14 formal properties
│ │ ├── wd.sby # SymbiYosys config
│ │ └── README.md # Formal verification docs
│ ├── am_mod.sv # AM modulation module
│ ├── am_radio_ctrl.v # 12-channel AM radio controller
│ ├── axi_audio_buffer.v # AXI audio buffer for BRAM playback
│ ├── nco_sin.v # Numerically Controlled Oscillator
│ ├── red_pitaya_top.sv # Top-level FPGA integration
│ ├── sine_lut_4096.mem # 4096-point sine lookup table
│ └── watchdog_timer.v # Watchdog timer module (production)
├── am_scpi_server.py # SCPI server (runs on Red Pitaya)
├── axi_audio_sequence_loop.py # Audio sequence loader (alarm → part1 → part2 loop)
├── alarm_fast.wav # Alarm tone
├── 0009_part1.wav # Emergency message part 1
├── 0009_part2_fast.wav # Emergency message part 2
├── requirements.txt # Python dependencies (numpy)
└── README.md
Channel Frequencies (Default)
Channel
Frequency
CH1
505 kHz
CH2
605 kHz
CH3
705 kHz
CH4
805 kHz
CH5
905 kHz
CH6
1005 kHz
CH7
1105 kHz
CH8
1205 kHz
CH9
1305 kHz
CH10
1405 kHz
CH11
1505 kHz
CH12
1605 kHz
Frequencies adjustable at runtime (500–1700 kHz range).
Watchdog Safety Design
Standard watchdog: device hangs → timer overflows → restarts device → back to normal
This watchdog: GUI dies → counter hits timeout → kills RF output → stays dead until operator resets
Why different: Automatically restarting a radio transmitter in an unmanned tunnel is dangerous. The system requires human confirmation before RF output resumes. Fail-safe, not fail-recover.
Safety margin: GUI polls every 500ms. Watchdog timeout is 5s. That's 10 consecutive missed heartbeats before trigger — resilient against transient network delays.
Performance Notes
Channels
Signal Strength
Recommendation
1–2
Excellent
✅ Best quality
3–4
Good
✅ Recommended max
5–8
Fair
⚠️ May need amplifier
9–12
Weak
⚠️ Short range only
Recommendation: 4–5 channels maximum for reliable reception.
SCPI Commands Reference
Command
Description
*IDN?
Device identification
STATUS?
Full device state
OUTPUT:STATE ON/OFF
Master broadcast enable
CH1:FREQ 505000
Set CH1 frequency (Hz)
CH1:OUTPUT ON/OFF
Enable/disable CH1
SOURCE:MSG 1
Select audio message
WATCHDOG:RESET
Reset watchdog timer
WATCHDOG:STATUS?
Query watchdog state
Testing
Rust Unit Tests
11 tests across the backend — state machine transitions, event bus pub/sub, retry logic, and config validation.
cd gui/src-tauri cargo test
Formal Verification (FPGA)
14 mathematically proven safety properties on the watchdog timer. See the Formal Verification section above.
Mock Server
For testing the GUI without a Red Pitaya connected:
Terminal 1 — start mock FPGA
cd gui npm run mock
Terminal 2 — start GUI
cd gui npm run dev
Then connect to 127.0.0.1:5000 in the GUI.
Troubleshooting
Problem
Solution
No RF output after power cycle
Reload bitstream: cat /root/red_pitaya_top.bit > /dev/xdevcfg
GUI won't connect
Check IP, ensure SCPI server is running
No audio, only carrier
Start audio loop: sudo python3 /root/axi_audio_sequence_loop.py
file does not start with RIFF id
Audio file is not a valid WAV — reconvert with ffmpeg -i input -ac 1 -ar 44100 output.wav
Weak signal
Reduce enabled channels (max 4–5)
Connection timeout
Check network, Red Pitaya power
Watchdog triggered unexpectedly
Check network stability, increase timeout if needed
linker 'link.exe' not found (Windows)
Install Visual Studio Build Tools with "Desktop development with C++"
cargo not found
Restart terminal after Rust install
npm not found
Restart terminal after Node.js install
xcode-select errors (macOS)
Run xcode-select --install
For Future Developers
This project will be inherited by the next EPI cohort. Here's what you need to know.
What works
The full signal chain is functional: GUI → Rust backend → TCP/SCPI → Red Pitaya → FPGA → RF output. Audio playback loops automatically. The watchdog kills RF if the GUI disconnects. All of this has been demonstrated live on hardware.
What to improve
The FPGA audio buffer is limited to 16,384 samples in BRAM, which forces downsampling to ~5 kHz. Longer or higher-quality audio would need external memory (DDR or SD card). The axi_audio_sequence_loop.py script reloads audio over AXI with a ~1.4 second gap between tracks — DMA would eliminate this. Currently only 4–5 channels are practical at usable signal strength; an external RF amplifier stage would allow all 12 channels simultaneously.
Key files to understand first
Read model.rs (the Rust backend — all network logic lives here), am_scpi_server.py (the bridge between TCP commands and FPGA registers), and am_radio_ctrl.v (the register interface between software and hardware). Those three files are the handshake points between every layer of the system.
Red Pitaya access
The Red Pitaya IP was 192.168.0.101 during development. SSH credentials are root/root. The FPGA bitstream loads automatically on boot from the SD card. If the bitstream is missing or corrupted, you'll need Vivado to rebuild it from the .sv/.v sources in fpga/.
Development workflow
For GUI changes: edit JS/HTML in gui/src/, run npm run dev — hot-reloads the frontend. For Rust backend changes: edit files in gui/src-tauri/src/, the dev server recompiles automatically (takes a few seconds). For FPGA changes: edit Verilog in fpga/, synthesise in Vivado, generate new bitstream, copy to Red Pitaya SD card.
Authors
- William Park — Software architecture (GUI, MVC, event bus), hardware watchdog timer, formal verification
- Bowen Deng — FPGA development (NCO, AM modulation, RF output)
Acknowledgments
- UGL Limited — Project sponsor
- University of New South Wales — EPI program
- Robert Mahood (UGL) — Engineering supervisor
- Andrew Wong (UNSW) — Academic supervisor
Final Version: 13th February 2026
Source involved in this report: Read Original Article
