AM Radio Notfallsender

Ein 12-Kanal AM-Rundfunksystem, das die Red Pitaya FPGA zur Übermittlung von Notfallwarnungen in unbemannten Tunneln nutzt.

Warum AM-Radio in einem Tunnel? Während Bau- und Wartungsarbeiten durchfahren Fahrzeuge mit serienmäßigen AM-Radios Tunnel, die keine Mobilfunkabdeckung haben. AM-Signale breiten sich entlang der Tunnelstrukturen über Leaky-Feeder-Kabel aus, und die Empfänger sind günstig, robust und in jedem Fahrzeug bereits vorhanden. Das System sendet vorab aufgezeichnete Notfallwarnungen auf mehreren Frequenzen aus, sodass jedes AM-Radio, das auf einen Sender im Band eingestellt ist, die Nachricht empfängt. Ein Hardware-Watchdog stellt sicher, dass die HF-Leistung abgeschaltet wird, falls das Steuerungssystem ausfällt – denn ein automatischer Neustart eines Senders in einem unbemannten Tunnel ist keine akzeptable Fehlerart.

Funktionen

Architektur

Software-Ebene

• Framework: Rust (Tauri) Backend + JavaScript Frontend
• Architektur: MVC mit ereignisgesteuertem Pub/Sub
• Model (model.rs): NetworkManager verwaltet TCP/SCPI, Gerätezustand, 500ms Polling, automatische Wiederverbindung mit exponentiellem Backoff
• View (view.js, index.html): Zustandslos – rendert nur bestätigten Gerätezustand. Nimmt niemals Hardware-Zustand an.
• Controller (controller.js): Verarbeitet Benutzereingaben, veröffentlicht Ereignisse auf dem Bus
• Event Bus (event_bus.rs, event_bus.js): Komponenten kommunizieren über einen zentralen Bus anstatt direkt aufzurufen. Rust emittiert Ereignisse an das JS-Frontend über die Tauri-Brücke.
• Zustandsmaschine (state_machine.rs): IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING. Zwischenzustände verhindern ungültige Übergänge.
• Quelle der Wahrheit: Das Gerät, nicht die Software. Die Benutzeroberfläche aktualisiert sich erst, nachdem die Hardware bestätigt hat.

Hardware-Ebene

• NCO: 12 numerisch gesteuerte Oszillatoren erzeugen Trägerfrequenzen (505–1605 kHz)
• AM-Modulator: Kombiniert Audioquelle mit jedem Träger
• Dynamische Skalierung: Die Ausgangsleistung passt sich basierend auf der Anzahl der aktivierten Kanäle an
• Audio-Puffer: BRAM speichert vorab aufgezeichnete Notfallmeldungen (16.384 Abtastwerte bei ~5 kHz Wiedergaberate). AXI-Audio-Lader für Laufzeit-Ladung verfügbar.
• Watchdog-Timer (wd.v): Hardware-Failsafe – wenn der GUI-Heartbeat für 5 Sekunden ausbleibt, wird die HF-Leistung abgeschaltet und verriegelt. Nur ein manueller Reset durch den Bediener stellt die Ausgabe wieder her.
• SCPI-Server (am_scpi_server.py): Läuft auf der Red Pitaya, parst Textbefehle, wandelt Frequenzen in Phaseninkremente um, schreibt über /dev/mem in FPGA-Register.

Signalgenerierungsablauf```

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

---

## Formale Verifikation

Der Watchdog-Timer ist mathematisch korrekt nachgewiesen mithilfe von Bounded Model Checking und k-Induktion (SymbiYosys + Z3 SMT-Löser). Im Gegensatz zum simulationsbasierten Testen, das einzelne Szenarien überprüft, beweist die formale Verifikation die Korrektheit für **jede mögliche Eingabe, in jedem möglichen Zustand, für alle Zeit**.

### 14 Sicherheitseigenschaften (Alle BESTANDEN)

| Kategorie | # | Eigenschaft | Garantie |
|-----------|---|-------------|----------|
| **Grundlegend** | 1 | Reset löscht alles | `!rstn` → counter=0, triggered=0, warning=0 |
| | 2 | Heartbeat verhindert Auslösung | Heartbeat setzt Zähler zurück, löscht triggered und warning |
| | 6 | Deaktivieren beendet alles | `!enable` → alle Ausgänge gelöscht |
| | 7 | Zähler begrenzt | Zähler überschreitet nie TIMEOUT_CYCLES |
| | 8 | Forcierter Reset funktioniert | `force_reset` löscht den gesamten Zustand |
| | 9 | Warnung niedrig vor Schwelle | counter < WARNING_CYCLES → warning=0 |
| **Sicherheit** | 3 | **Keine vorzeitige Auslösung** | **triggered NUR wenn counter ≥ TIMEOUT_CYCLES** |
| | 4 | Auslösung garantiert bei Timeout | Lebendigkeit: Timeout löst immer trigger aus |
| | 5 | Warnung vor Auslösung | triggered=1 → warning=1 |
| | 5b | Kontraposition | !warning → !triggered |
| | 10 | Warnung hoch in Zone | counter > WARNING_CYCLES → warning=1 |
| | 11 | Zähler inkrementiert korrekt | Genau +1 pro Taktzyklus während des Zählens |
| **Ausgang** | 12 | time_remaining bei Null | counter=0 → time_remaining = TIMEOUT_SEC |
| | 13 | time_remaining bei Auslösung | triggered → time_remaining = 0 |
| | 14 | time_remaining monoton | Nimmt jeden Zyklus während des Zählens ab |

### 6 Abdeckungsszenarien (Alle erreicht)

| # | Szenario | Schritte | Beschreibung |
|---|----------|----------|--------------|
| 1 | Auslösung erfolgt | 23 | Zähler erreicht Timeout |
| 2 | Warnung ohne Auslösung | 21 | In Warnzone, noch nicht abgelaufen |
| 3 | Exakte Timeout-Grenze | 22 | Zähler = TIMEOUT_CYCLES genau |
| 4 | Heartbeat in letzter Sekunde | 19 | Heartbeat bei Zähler = T-1 |
| 5 | Wiederherstellung nach Auslösung | 24 | Ausgelöster Zustand durch force_reset gelöscht |
| 6 | Warnungs-zu-Auslösung-Lebenszyklus | 23 | Warnung dann sofortige Auslösung |

### Ausführen der Verifikation```bash
cd fpga/formal/
sby -f wd.sby

Erwartete Ausgabe: ``` 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.

### Skalierbarkeit

Die Verifikation verwendet `CLK_FREQ=1`, `TIMEOUT_SEC=5`, um den Zustandsraum handhabbar zu halten. In der Produktion wird `CLK_FREQ=125000000` verwendet. Das RTL ist parametrisiert – gleiche if/else-Logik, gleiche Zustandsübergänge. Ein Beweis im reduzierten Maßstab impliziert Korrektheit im Produktionsmaßstab.

Siehe [`fpga/formal/README.md`](https://github.com/park07/amradio/blob/HEAD/am_radio/fpga/formal/README.md)
---

## Anforderungen

### Hardware

- Red Pitaya STEMlab 125-10
- AM-Radioempfänger zum Testen
- Ethernet-Kabel (für Red Pitaya-Verbindung)

### Software

| Abhängigkeit | macOS | Windows |
|-----------|-------|---------|
| Rust + Cargo | `curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \| sh` | Laden Sie `rustup-init.exe` von [rustup.rs](https://rustup.rs) herunter |
| Node.js (LTS) | `brew install node` oder [nodejs.org](https://nodejs.org) | [nodejs.org](https://nodejs.org) |
| Xcode-Befehlszeilentools (nur macOS) | `xcode-select --install` | — |
| Visual Studio Build Tools (nur Windows) | — | [Download](https://visualstudio.microsoft.com/visual-cpp-build-tools/) — wählen Sie **"Desktop development with C++"** |

### Formale Verifikation (optional)

- SymbiYosys
- Yosys
- Z3 SMT solver

---

## Installation

### 1. Repository klonen```bash
git clone https://github.com/Park07/amradio.git
cd amradio/am_radio

2. Erstelle die GUI

macOS```bash

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

Die erstellte `.app` befindet sich in `gui/src-tauri/target/release/bundle/macos/`.

#### Windows (PowerShell)```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\.

Hinweis: Der erste Build dauert etwa 2–3 Minuten (Rust-Kompilierung). Folgende Builds sind schneller.

3. Red Pitaya einrichten

Per SSH in den Red Pitaya einloggen:```bash ssh root@<RED_PITAYA_IP>

Default password: root

Erforderliche Dateien kopieren:```bash

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-Umgebung (Red Pitaya)

Das Red Pitaya läuft mit Alpine Linux und Python 3.5. Der SCPI-Server hat keine externen Abhängigkeiten (nur stdlib). Der Audio-Loader benötigt numpy:```bash

On Red Pitaya

pip install numpy

> **Hinweis:** Das Python 3.5 des Red Pitaya unterstützt `venv` nicht standardmäßig und läuft als root, daher werden Pakete global installiert. Das ist in Ordnung – es handelt sich um ein eingebettetes Gerät, nicht um einen gemeinsam genutzten Server.

### 5. Python-Umgebung (Lokale Entwicklung – optional)

Wenn Sie die Python-Skripte lokal ausführen oder ändern möchten (z. B. zum Testen der Audioverarbeitung ohne den Red Pitaya):```bash
python3 -m venv venv
source venv/bin/activate        # macOS/Linux
# or
.\venv\Scripts\activate         # Windows PowerShell

pip install -r requirements.txt

Addiere venv/ zur .gitignore, falls noch nicht vorhanden.

Audiodateien

Das System spielt drei Audiodateien in einer Schleife ab: Alarm → Teil 1 → Teil 2 → (wiederholen).

Alle Audiodaten werden auf ~5 kHz heruntergetaktet, um in den 16.384-Sample-BRAM-Puffer des FPGA zu passen. Das Skript axi_audio_sequence_loop.py übernimmt automatisch das Resampling, die 14-Bit-Konvertierung und das sequenzielle Laden.

Nutzung

Sie benötigen drei SSH-Terminals, die mit dem Red Pitaya verbunden sind, sowie ein lokales Terminal für die GUI.

Hinweis: Die IP-Adresse des Red Pitaya kann sich bei jedem Einschalten ändern. Überprüfen Sie die DHCP-Client-Liste Ihres Routers oder verwenden Sie ping rp-f0866a.local, um sie zu finden.

Schritt 1: Verbindung zum Red Pitaya herstellen

Öffnen Sie ein Terminal und stellen Sie eine SSH-Verbindung her:```bash ssh root@<RED_PITAYA_IP>

Password: root

### Schritt 2: Laden des FPGA-Bitstreams

Auf dem Red Pitaya (erstes SSH-Terminal):```bash
cat /root/red_pitaya_top.bit > /dev/xdevcfg

Dies lädt das AM-Radio-Design auf das FPGA. Erforderlich nach jedem Power-Cycle.

Schritt 3: Starten Sie den SCPI-Server

Auf dem Red Pitaya (gleiches oder zweites SSH-Terminal):```bash python3 /root/am_scpi_server.py

### Schritt 4: Starten Sie die Audiowiedergabe

Lassen Sie dies laufen — es verbindet TCP-Befehle von der GUI mit FPGA-Registern.

Öffnen Sie ein zweites SSH-Terminal zur Red Pitaya:```bash
ssh root@<RED_PITAYA_IP>
sudo python3 /root/axi_audio_sequence_loop.py

Erwartete Ausgabe:```

AXI AUDIO SEQUENCE - AUTO LOOP Alarm -> Part 1 -> Part 2 -> (repeat)

Buffer: 16384 samples FPGA playback rate: 5000 Hz Press Ctrl+C to stop

### Schritt 5: Die GUI ausführen

Auf Ihrem lokalen Rechner:```bash
cd gui
npm run dev

Oder führen Sie die erstellte Binärdatei direkt von src-tauri/target/release/ aus.

Schritt 6: Verbinden und senden

1. Geben Sie die IP-Adresse des Red Pitaya ein
2. Klicken Sie auf Verbinden
3. Aktivieren Sie die gewünschten Kanäle (1–12)
4. Passen Sie die Frequenzen bei Bedarf an
5. Klicken Sie auf SENDEN STARTEN
6. Stimmen Sie ein AM-Radio auf eine beliebige aktivierte Frequenz ab

Vivado (nur für FPGA-Entwicklung)

Wenn Sie das FPGA-Design ändern und das Bitstream neu erstellen müssen, installieren Sie Vivado 2020.1. Red Pitaya bietet eine Setup-Anleitung hier:

https://redpitaya.readthedocs.io/en/latest/developerGuide/fpga/getting_started/vivado_install.html

Alle grundlegenden Red Pitaya Einstellungen und Tutorials sind in der offiziellen Red Pitaya Dokumentation verfügbar.

Dateistruktur```

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

---

## Kanalfrequenzen (Standard)

| Kanal | Frequenz |
|-------|----------|
| 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 |

Frequenzen zur Laufzeit einstellbar (Bereich 500–1700 kHz).

---

## Watchdog-Sicherheitsdesign
![Watchdog-Zustandsmaschine](https://assets.kitploit.com/production/public/readmes/11878/6531091e26d450ab35e4e20c91ca2b88952b40ccf8a195443fe782cb413f45c5.png)```
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

Warum anders: Das automatische Neustarten eines Funksenders in einem unbemannten Tunnel ist gefährlich. Das System erfordert menschliche Bestätigung, bevor die HF-Ausgabe wieder aufgenommen wird. Fail-safe, nicht fail-recover.

Sicherheitsmarge: Die GUI fragt alle 500ms ab. Watchdog-Timeout beträgt 5s. Das sind 10 aufeinanderfolgende verpasste Heartbeats vor dem Auslösen – widerstandsfähig gegen vorübergehende Netzwerkverzögerungen.

Leistungshinweise

Empfehlung: Maximal 4–5 Kanäle für zuverlässigen Empfang.

SCPI-Befehlsreferenz

Tests

Rust-Unit-Tests

11 Tests im gesamten Backend – Zustandsmaschinenübergänge, Event-Bus-Pub/Sub, Wiederholungslogik und Konfigurationsvalidierung.```bash cd gui/src-tauri cargo test

### Formale Verifikation (FPGA)

14 mathematisch bewiesene Sicherheitseigenschaften des Watchdog-Timers. Siehe den Abschnitt [Formale Verifikation](#formal-verification) oben.

### Mock-Server

Zum Testen der GUI ohne angeschlossenen Red Pitaya:```bash
# Terminal 1 — start mock FPGA
cd gui
npm run mock

# Terminal 2 — start GUI
cd gui
npm run dev

Dann verbinde dich in der GUI mit 127.0.0.1:5000.

Fehlerbehebung

Für zukünftige Entwickler

Dieses Projekt wird an den nächsten EPI-Jahrgang übergeben. Folgendes solltet ihr wissen.

Was funktioniert

Die gesamte Signalkette ist funktionsfähig: GUI → Rust-Backend → TCP/SCPI → Red Pitaya → FPGA → HF-Ausgang. Die Audiowiedergabe läuft automatisch in einer Schleife. Der Watchdog schaltet den HF-Ausgang ab, wenn die GUI die Verbindung verliert. Dies alles wurde live auf Hardware demonstriert.

Was verbessert werden sollte

Der FPGA-Audiopuffer ist auf 16.384 Samples im BRAM begrenzt, was eine Abtastung auf ~5 kHz erzwingt. Längeres oder höherwertiges Audio würde externen Speicher (DDR oder SD‑Karte) benötigen. Das Skript axi_audio_sequence_loop.py lädt Audio über AXI mit einer Lücke von etwa 1,4 Sekunden zwischen den Titeln – DMA würde dies beseitigen. Derzeit sind nur 4–5 Kanäle bei nutzbarer Signalstärke praktikabel; eine externe HF-Verstärkerstufe würde alle 12 Kanäle gleichzeitig ermöglichen.

Wichtige Dateien, die zuerst verstanden werden sollten

Lest model.rs (das Rust‑Backend – die gesamte Netzwerklogik befindet sich dort), am_scpi_server.py (die Brücke zwischen TCP‑Befehlen und FPGA‑Registern) und am_radio_ctrl.v (die Register‑Schnittstelle zwischen Software und Hardware). Diese drei Dateien sind die Verbindungspunkte zwischen allen Ebenen des Systems.

Red Pitaya Zugang

Die Red‑Pitaya‑IP war während der Entwicklung 192.168.0.101. SSH‑Anmeldedaten sind root/root. Das FPGA‑Bitstream wird beim Booten automatisch von der SD‑Karte geladen. Falls das Bitstream fehlt oder beschädigt ist, müsst ihr es mit Vivado aus den .sv/.v‑Quellen in fpga/ neu erstellen.

Entwicklungsworkflow

Für GUI‑Änderungen: JS/HTML in gui/src/ bearbeiten, npm run dev ausführen – die Frontend‑Hot‑Reloading-Funktion wird aktiviert. Für Rust‑Backend‑Änderungen: Dateien in gui/src-tauri/src/ bearbeiten, der Entwicklungsserver kompiliert automatisch neu (dauert ein paar Sekunden). Für FPGA‑Änderungen: Verilog in fpga/ bearbeiten, in Vivado synthetisieren, neues Bitstream erzeugen, auf die SD‑Karte des Red Pitaya kopieren.

Wichtiger Hinweis!:

• Bei meiner Arbeit waren die Audiodateien tatsächlich auf dem Red Pitaya gespeichert. Und da er nur einen maximalen Speicherpuffer von 32 KB hat, mussten wir die Notfall-Audiodateien in 3 Teile (~4 Sekunden jeder) aufteilen, und er überschrieb das vorherige Audio.
• Die Audiodateien sind nicht in diesem Repository zu finden, aber fühlt euch frei, das selbst herauszufinden. Ich empfehle, die Red‑Pitaya‑Version 14 für besseres Live‑Streaming zu verwenden. Die 125-10 ist zu veraltet, und die meisten dieser Speicherprobleme lassen sich leicht durch ein Upgrade auf 125-15 beheben. Pavel hat einen guten Hinweis, der auch für die 125-14 relevant sein könnte.

Autoren

• ("Jaewoo") William Park (JW P) — Softwarearchitektur (GUI, MVC, ereignisgesteuerte Architektur), Frontend (JS), Backend (Rust), Hardware‑Watchdog, formale Verifikation, Zustandsmaschine
• Bowen Deng — FPGA‑Entwicklung (NCO, AM‑Modulation, HF‑Ausgang)

Danksagungen

• University of New South Wales
• Robert Mahood — Technischer Betreuer
• Andrew Wong (UNSW) — Wissenschaftlicher Betreuer

Endversion: 13. Februar 2026