Système de radiodiffusion AM d'urgence

Un système de radiodiffusion AM à 12 canaux utilisant le FPGA Red Pitaya pour la transmission d'alertes d'urgence dans les tunnels sans personnel.

Pourquoi la radio AM dans un tunnel ? Pendant la construction et la maintenance, les véhicules équipés de radios AM standard traversent des tunnels sans couverture mobile. Les signaux AM se propagent le long des structures du tunnel via des câbles rayonnants, et les récepteurs sont bon marché, robustes et déjà présents dans chaque véhicule. Le système diffuse des alertes d'urgence préenregistrées sur plusieurs fréquences afin que toute radio AM réglée sur n'importe quelle station de la bande reçoive le message. Un chien de garde matériel garantit que la sortie RF est coupée si le système de contrôle échoue — car le redémarrage automatique d'un émetteur dans un tunnel sans personnel n'est pas un mode de défaillance acceptable.

Fonctionnalités

Architecture

Couche logicielle

• Framework : Backend Rust (Tauri) + frontend JavaScript
• Architecture : MVC avec pub/sous événementiel
• Modèle (model.rs) : NetworkManager gère TCP/SCPI, l'état du dispositif, le sondage à 500 ms, la reconnexion automatique avec backoff exponentiel
• Vue (view.js, index.html) : Sans état — n'affiche que l'état confirmé du dispositif. Ne présuppose jamais l'état matériel.
• Contrôleur (controller.js) : Gère les entrées utilisateur, publie des événements sur le bus
• Bus d'événements (event_bus.rs, event_bus.js) : Les composants communiquent via un bus central au lieu de s'appeler directement. Rust émet des événements vers le frontend JS via le pont Tauri.
• Machine d'états (state_machine.rs) : IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING. Les états intermédiaires empêchent les transitions invalides.
• Source de vérité : Le dispositif, pas le logiciel. L'interface utilisateur ne se met à jour qu'après confirmation matérielle.

Couche matérielle

• NCO : 12 oscillateurs numériques génèrent les fréquences porteuses (505–1605 kHz)
• Modulateur AM : Combine la source audio avec chaque porteuse
• Ajustement dynamique : La puissance de sortie s'ajuste en fonction du nombre de canaux activés
• Tampon audio : BRAM stocke les messages d'urgence préenregistrés (tampon de 16 384 échantillons à ~5 kHz). Un chargeur audio AXI permet le chargement en temps réel.
• Chien de garde (wd.v) : Sécurisé en matériel — si le battement de cœur de l'interface utilisateur s'arrête pendant 5 secondes, la sortie RF est coupée et verrouillée. Seule une réinitialisation manuelle par l'opérateur rétablit la sortie.
• Serveur SCPI (am_scpi_server.py) : S'exécute sur le Red Pitaya, analyse les commandes textuelles, convertit les fréquences en incréments de phase, écrit dans les registres FPGA via /dev/mem.

Flux de génération du signal```

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

---

## Vérification formelle

Le chien de garde (watchdog) est mathématiquement prouvé correct en utilisant le model checking borné et l'induction-k (SymbiYosys + solveur SMT Z3). Contrairement aux tests basés sur la simulation qui vérifient des scénarios individuels, la vérification formelle prouve l'exactitude pour **chaque entrée possible, dans chaque état possible, pour toujours**.

### 14 Propriétés de sécurité (Toutes réussies)

| Catégorie | # | Propriété | Garantie |
|----------|---|----------|-----------|
| **Basique** | 1 | Reset efface tout | `!rstn` → counter=0, triggered=0, warning=0 |
| | 2 | Heartbeat empêche le déclenchement | Heartbeat réinitialise le compteur, efface triggered et warning |
| | 6 | Désactivation arrête tout | `!enable` → toutes les sorties effacées |
| | 7 | Compteur borné | Le compteur ne dépasse jamais TIMEOUT_CYCLES |
| | 8 | Force reset fonctionne | `force_reset` efface tout l'état |
| | 9 | Avertissement bas avant seuil | counter < WARNING_CYCLES → warning=0 |
| **Sécurité** | 3 | **Pas de déclenchement prématuré** | **déclenché UNIQUEMENT quand counter ≥ TIMEOUT_CYCLES** |
| | 4 | Déclenchement garanti à l'expiration du délai | Vivacité : le délai déclenche toujours |
| | 5 | Avertissement avant déclenchement | triggered=1 → warning=1 |
| | 5b | Contraposée | !warning → !triggered |
| | 10 | Avertissement élevé dans la zone | counter > WARNING_CYCLES → warning=1 |
| | 11 | Compteur s'incrémente correctement | Exactement +1 par cycle d'horloge pendant le comptage |
| **Sortie** | 12 | time_remaining à zéro | counter=0 → time_remaining = TIMEOUT_SEC |
| | 13 | time_remaining au déclenchement | triggered → time_remaining = 0 |
| | 14 | time_remaining monotone | Diminue à chaque cycle pendant le comptage |

### 6 Scénarios de couverture (Tous atteints)

| # | Scénario | Pas | Description |
|---|----------|-------|-------------|
| 1 | Déclenchement se produit | 23 | Le compteur atteint le délai |
| 2 | Avertissement sans déclenchement | 21 | Dans la zone d'avertissement, pas encore expiré |
| 3 | Limite exacte du délai | 22 | Compteur = TIMEOUT_CYCLES exactement |
| 4 | Heartbeat de dernière seconde | 19 | Heartbeat au compteur = T-1 |
| 5 | Récupération après déclenchement | 24 | État déclenché effacé par force_reset |
| 6 | Cycle de vie avertissement-déclenchement | 23 | Avertissement puis déclenchement immédiat |

### Exécution de la vérification```bash
cd fpga/formal/
sby -f wd.sby

Sortie attendue: ``` 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.

### Passage à l'échelle

La vérification utilise `CLK_FREQ=1`, `TIMEOUT_SEC=5` pour garder l'espace d'état traitable. La production utilise `CLK_FREQ=125000000`. Le RTL est paramétré — même logique if/else, mêmes transitions d'état. Une preuve à échelle réduite implique la correction à l'échelle de production.

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

## Prérequis

### Matériel

- Red Pitaya STEMlab 125-10
- Récepteur(s) radio AM pour les tests
- Câble Ethernet (pour la connexion Red Pitaya)

### Logiciel

| Dépendance | macOS | Windows |
|-----------|-------|---------|
| Rust + Cargo | `curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \| sh` | Télécharger `rustup-init.exe` depuis [rustup.rs](https://rustup.rs) |
| Node.js (LTS) | `brew install node` ou [nodejs.org](https://nodejs.org) | [nodejs.org](https://nodejs.org) |
| Xcode Command Line Tools (macOS uniquement) | `xcode-select --install` | — |
| Visual Studio Build Tools (Windows uniquement) | — | [Télécharger](https://visualstudio.microsoft.com/visual-cpp-build-tools/) — sélectionnez **"Développement Desktop avec C++"** |

### Vérification formelle (optionnelle)

- SymbiYosys
- Yosys
- Z3 SMT solver

---

## Installation

### 1. Cloner le dépôt```bash
git clone https://github.com/Park07/amradio.git
cd amradio/am_radio

2. Construire l'interface graphique

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

L'`.app` construit se trouvera dans `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

Le fichier .exe construit se trouvera dans gui\src-tauri\target\release\.

Note: La première construction prend environ 2 à 3 minutes (compilation de Rust). Les constructions suivantes sont plus rapides.

3. Configuration de Red Pitaya

Connectez-vous en SSH au Red Pitaya :```bash ssh root@<RED_PITAYA_IP>

Default password: root

Copier les fichiers requis :```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/

Remarque

Bitstream est déjà sur la carte SD du Red Pitaya depuis le développement.

Pour reconstruire : ouvrir project_William.xpr dans Vivado, générer le bitstream,

puis scp le nouveau fichier .bit vers le Red Pitaya.

4. Environnement Python (Red Pitaya)

Le Red Pitaya exécute Alpine Linux avec Python 3.5. Le serveur SCPI n’a pas de dépendances externes (stdlib uniquement). Le chargeur audio nécessite numpy :```bash

On Red Pitaya

pip install numpy

> **Note :** Le Python 3.5 de la Red Pitaya ne supporte pas `venv` par défaut et s'exécute en tant que root, donc les paquets sont installés globalement. Ce n'est pas un problème — c'est un appareil embarqué, pas un serveur partagé.

### 5. Environnement Python (Développement local — facultatif)```bash
python3 -m venv venv
source venv/bin/activate        # macOS/Linux
# or
.\venv\Scripts\activate         # Windows PowerShell

pip install -r requirements.txt

Ajoutez venv/ à .gitignore si ce n'est pas déjà fait.

Fichiers audio

Le système joue trois fichiers audio en boucle : Alarme → Partie 1 → Partie 2 → (répétition).

Tout l'audio est sous-échantillonné à ~5 kHz pour tenir dans le tampon BRAM de 16 384 échantillons du FPGA. Le script axi_audio_sequence_loop.py gère automatiquement le rééchantillonnage, la conversion 14 bits et le chargement séquentiel.

Utilisation

Vous avez besoin de trois terminaux SSH ouverts vers le Red Pitaya, plus un terminal local pour l'interface graphique.

Remarque : L'adresse IP du Red Pitaya peut changer à chaque mise sous tension. Vérifiez la liste des clients DHCP de votre routeur ou utilisez ping rp-f0866a.local pour la trouver.

Étape 1 : Connecter au Red Pitaya

Ouvrez un terminal et connectez-vous en SSH :```bash ssh root@<RED_PITAYA_IP>

Password: root

### Étape 2: charger le bitstream FPGA

Sur le Red Pitaya (premier terminal SSH):```bash
cat /root/red_pitaya_top.bit > /dev/xdevcfg

Ceci charge la conception de la radio AM sur le FPGA. Requis après chaque cycle d'alimentation.

Étape 3 : Démarrer le serveur SCPI

Sur la Red Pitaya (même terminal SSH ou second) :```bash python3 /root/am_scpi_server.py

Laissez ceci en cours d'exécution — il fait le pont entre les commandes TCP de l'interface graphique et les registres FPGA.

### Étape 4 : Démarrer la boucle audio

Ouvrez un second terminal SSH vers la Red Pitaya :```bash
ssh root@<RED_PITAYA_IP>
sudo python3 /root/axi_audio_sequence_loop.py

Sortie attendue :```

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

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

### Étape 5 : Exécuter l'interface graphique

Sur votre machine locale :```bash
cd gui
npm run dev

Ou exécutez le binaire compilé directement depuis src-tauri/target/release/.

Étape 6: Connexion et diffusion

1. Saisissez l'adresse IP du Red Pitaya
2. Cliquez sur Connect
3. Activez les canaux souhaités (1–12)
4. Ajustez les fréquences si nécessaire
5. Cliquez sur START BROADCAST
6. Réglez une radio AM sur une fréquence activée

Vivado (pour le développement FPGA uniquement)

Si vous devez modifier la conception FPGA et reconstruire le bitstream, installez Vivado 2020.1. Red Pitaya fournit un guide d'installation ici :

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

Tous les paramètres et tutoriels de base de Red Pitaya sont disponibles sur la documentation officielle de Red Pitaya.

Structure des fichiers```

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

---

## Fréquences des canaux (par défaut)

| Canal | Fréquence |
|---------|-----------|
| 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 |

Fréquences ajustables en cours d'exécution (plage 500–1700 kHz).

---

## Conception de sécurité Watchdog
![Machine d'état Watchdog](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

Why different: Redémarrer automatiquement un émetteur radio dans un tunnel non habité est dangereux. Le système nécessite une confirmation humaine avant la reprise de la sortie RF. Sécurité passive, pas de récupération automatique.

Safety margin: L'interface graphique interroge toutes les 500 ms. Le délai d'expiration du chien de garde est de 5 s. Cela représente 10 battements de cœur consécutifs manqués avant le déclenchement — résistant aux délais réseau transitoires.

Notes de performances

Recommandation : 4–5 canaux maximum pour une réception fiable.

Référence des commandes SCPI

Tests

Tests unitaires Rust

11 tests à travers le backend — transitions de machine d'état, publication/abonnement de bus d'événements, logique de réessai et validation de configuration.```bash cd gui/src-tauri cargo test

### Vérification formelle (FPGA)

14 propriétés de sécurité mathématiquement prouvées sur le chien de garde. Voir la section [Vérification formelle](#formal-verification) ci-dessus.

### Serveur Mock

Pour tester l'interface graphique sans qu'un Red Pitaya ne soit connecté :```bash
# Terminal 1 — start mock FPGA
cd gui
npm run mock

# Terminal 2 — start GUI
cd gui
npm run dev

Ensuite, connectez-vous à 127.0.0.1:5000 dans l'interface graphique.

Dépannage

Pour les futurs développeurs

Ce projet sera repris par la prochaine cohorte EPI. Voici ce que vous devez savoir.

Ce qui fonctionne

La chaîne de signal complète est fonctionnelle : interface graphique → backend Rust → TCP/SCPI → Red Pitaya → FPGA → sortie RF. La lecture audio boucle automatiquement. Le watchdog coupe la RF si l'interface graphique se déconnecte. Tout cela a été démontré en direct sur le matériel.

Ce qu'il faut améliorer

Le tampon audio FPGA est limité à 16 384 échantillons dans la BRAM, ce qui force un sous-échantillonnage à environ 5 kHz. Un audio plus long ou de meilleure qualité nécessiterait une mémoire externe (DDR ou carte SD). Le script axi_audio_sequence_loop.py recharge l'audio via AXI avec un intervalle d'environ 1,4 seconde entre les pistes — le DMA éliminerait cela. Actuellement, seuls 4 à 5 canaux sont pratiques à une puissance de signal utilisable ; un étage d'amplification RF externe permettrait d'utiliser les 12 canaux simultanément.

Fichiers clés à comprendre en premier

Lisez model.rs (le backend Rust — toute la logique réseau se trouve ici), am_scpi_server.py (le pont entre les commandes TCP et les registres FPGA), et am_radio_ctrl.v (l'interface de registre entre le logiciel et le matériel). Ces trois fichiers sont les points de liaison entre toutes les couches du système.

Accès au Red Pitaya

L'adresse IP du Red Pitaya était 192.168.0.101 pendant le développement. Les identifiants SSH sont root/root. Le bitstream FPGA se charge automatiquement au démarrage depuis la carte SD. Si le bitstream est manquant ou corrompu, vous aurez besoin de Vivado pour le reconstruire à partir des sources .sv/.v dans fpga/.

Flux de travail de développement

Pour les modifications de l'interface graphique : éditez JS/HTML dans gui/src/, exécutez npm run dev — rechargement à chaud du frontend. Pour les modifications du backend Rust : éditez les fichiers dans gui/src-tauri/src/, le serveur de développement se recompile automatiquement (prend quelques secondes). Pour les modifications FPGA : éditez le Verilog dans fpga/, synthétisez dans Vivado, générez un nouveau bitstream, copiez-le sur la carte SD du Red Pitaya.

Note importante ! :

• Pour mon travail, les fichiers audio étaient en fait stockés à l'intérieur du Red Pitaya. Et comme il dispose d'un tampon mémoire maximum de 32k, nous avons dû diviser l'audio d'urgence en 3 parties (~4 secondes chacune), et il réécrivait l'audio précédent.
• Les fichiers audio ne se trouvent pas dans ce dépôt, mais n'hésitez pas à trouver comment faire. Je recommande d'utiliser la version 14 du Red Pitaya pour un meilleur streaming en direct. Le 125-10 est trop obsolète et la plupart des problèmes de mémoire rencontrés peuvent être facilement résolus en passant au 125-15. Pavel a une excellente note qui pourrait également être pertinente pour le 125-14.

Auteurs

• ("Jaewoo") William Park (JW P) — Architecture logicielle (interface graphique, MVC, architecture orientée événements), Frontend (JS), Backend (Rust), chien de garde matériel, vérification formelle, machine d'états
• Bowen Deng — Développement FPGA (NCO, modulation AM, sortie RF)

Remerciements

• University of New South Wales
• Robert Mahood — Superviseur d'ingénierie
• Andrew Wong (UNSW) — Superviseur académique

Version finale : 13 février 2026