Show HN: Formally verified FPGA watchdog for AM broadcast 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.

• 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.

• 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.

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.

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.

• Red Pitaya STEMlab 125-10
• AM Radio receiver(s) for testing
• Ethernet cable (for Red Pitaya connection)

• SymbiYosys
• Yosys
• Z3 SMT solver

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

# Build
cd gui
npm install
npm run build

The built .app will be in gui/src-tauri/target/release/bundle/macos/.

# 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.

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

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.

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.

The system plays three audio files in a loop: Alarm → Part 1 → Part 2 → (repeat).

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.

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.

Open a terminal and SSH in:

ssh root@<RED_PITAYA_IP>
# Password: root

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.

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.

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
============================================================

On your local machine:

Or run the built binary directly from src-tauri/target/release/.

1. Enter the Red Pitaya IP address
2. Click Connect
3. Enable desired channels (1–12)
4. Adjust frequencies if needed
5. Click START BROADCAST
6. Tune an AM radio to any enabled frequency

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.

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

Frequencies adjustable at runtime (500–1700 kHz range).

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.

Recommendation: 4–5 channels maximum for reliable reception.

11 tests across the backend — state machine transitions, event bus pub/sub, retry logic, and config validation.

cd gui/src-tauri
cargo test

14 mathematically proven safety properties on the watchdog timer. See the Formal Verification section above.

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.

This project will be inherited by the next EPI cohort. Here's what you need to know.

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.

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.

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.

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/.

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.

• William Park — Software architecture (GUI, MVC, event bus), hardware watchdog timer, formal verification
• Bowen Deng — FPGA development (NCO, AM modulation, RF output)

• University of New South Wales — EPI program
• Robert Mahood — Engineering supervisor
• Andrew Wong (UNSW) — Academic supervisor

Final Version: 13th February 2026