Sistema di Allerta Radio AM

Un sistema di trasmissione radio AM a 12 canali che utilizza FPGA Red Pitaya per la trasmissione di allarmi di emergenza in gallerie non presidiate.

Perché la radio AM in un tunnel? Durante la costruzione e la manutenzione, i veicoli con radio AM standard transitano attraverso tunnel che non hanno copertura mobile. I segnali AM si propagano lungo le strutture del tunnel tramite cavi leaky feeder, e i ricevitori sono economici, robusti e già presenti in ogni veicolo. Il sistema trasmette messaggi di emergenza preregistrati su più frequenze, in modo che qualsiasi radio AM sintonizzata su una qualsiasi stazione nella banda riceva il messaggio. Un watchdog hardware garantisce che l'emissione RF venga interrotta se il sistema di controllo fallisce — perché riavviare automaticamente un trasmettitore in un tunnel non presidiato non è una modalità di guasto accettabile.

Caratteristiche

Architettura

Livello Software

• Framework: backend Rust (Tauri) + frontend JavaScript
• Architettura: MVC con pub/sub guidato da eventi
• Model (model.rs): NetworkManager gestisce TCP/SCPI, stato del dispositivo, polling a 500 ms, riconnessione automatica con backoff esponenziale
• View (view.js, index.html): Senza stato — rende solo lo stato confermato del dispositivo. Non assume mai lo stato hardware.
• Controller (controller.js): Gestisce l'input utente, pubblica eventi sul bus
• Event Bus (event_bus.rs, event_bus.js): I componenti comunicano attraverso un bus centrale invece di chiamarsi direttamente. Rust emette eventi al frontend JS tramite il bridge Tauri.
• State Machine (state_machine.rs): IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING. Gli stati intermedi impediscono transizioni non valide.
• Fonte della Verità: Il dispositivo, non il software. L'UI si aggiorna solo dopo la conferma hardware.

Livello Hardware

• NCO: 12 oscillatori controllati numericamente generano frequenze portanti (505–1605 kHz)
• Modulatore AM: Combina la sorgente audio con ciascuna portante
• Scala Dinamica: La potenza di uscita si adatta in base al numero di canali abilitati
• Buffer Audio: La BRAM memorizza messaggi di emergenza preregistrati (buffer di 16.384 campioni a una frequenza di riproduzione di circa 5 kHz). Caricatore audio AXI disponibile per il caricamento a runtime.
• Timer Watchdog (wd.v): Fail-safe hardware — se il heartbeat della GUI si ferma per 5 secondi, l'uscita RF viene uccisa e bloccata. Solo un reset manuale dell'operatore ripristina l'uscita.
• Server SCPI (am_scpi_server.py): Esegue su Red Pitaya, analizza i comandi di testo, converte le frequenze in incrementi di fase, scrive nei registri FPGA tramite /dev/mem.

Flusso di Generazione del Segnale```

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

---

## Verifica Formale

Il watchdog timer è dimostrato matematicamente corretto utilizzando bounded model checking e k-induction (SymbiYosys + Z3 SMT solver). A differenza dei test basati su simulazione che verificano singoli scenari, la verifica formale prova la correttezza attraverso **ogni possibile input, in ogni possibile stato, per tutto il tempo**.

### 14 Proprietà di Sicurezza (Tutte SUPERATE)

| Categoria | # | Proprietà | Garanzia |
|----------|---|-----------|----------|
| **Base** | 1 | Reset cancella tutto | `!rstn` → counter=0, triggered=0, warning=0 |
| | 2 | Heartbeat previene il trigger | Heartbeat resetta il contatore, cancella triggered e warning |
| | 6 | Disable blocca tutto | `!enable` → tutti gli output azzerati |
| | 7 | Contatore limitato | Il contatore non supera mai TIMEOUT_CYCLES |
| | 8 | Force reset funziona | `force_reset` cancella tutto lo stato |
| | 9 | Warning basso prima della soglia | counter < WARNING_CYCLES → warning=0 |
| **Sicurezza** | 3 | **Nessun trigger anticipato** | **triggered SOLO quando counter ≥ TIMEOUT_CYCLES** |
| | 4 | Trigger garantito al timeout | Liveness: il timeout attiva sempre il trigger |
| | 5 | Warning prima del trigger | triggered=1 → warning=1 |
| | 5b | Contropositivo | !warning → !triggered |
| | 10 | Warning alto in zona | counter > WARNING_CYCLES → warning=1 |
| | 11 | Contatore incrementa correttamente | Esattamente +1 per ciclo di clock durante il conteggio |
| **Uscita** | 12 | time_remaining a zero | counter=0 → time_remaining = TIMEOUT_SEC |
| | 13 | time_remaining al trigger | triggered → time_remaining = 0 |
| | 14 | time_remaining monotono | Diminuisce ogni ciclo durante il conteggio |

### 6 Scenari di Copertura (Tutti Raggiunti)

| # | Scenario | Passi | Descrizione |
|---|----------|-------|-------------|
| 1 | Trigger si attiva | 23 | Il contatore raggiunge il timeout |
| 2 | Warning senza trigger | 21 | In zona warning, non ancora scaduto |
| 3 | Confine esatto del timeout | 22 | Contatore esattamente = TIMEOUT_CYCLES |
| 4 | Heartbeat all'ultimo secondo | 19 | Heartbeat al contatore = T-1 |
| 5 | Recupero da triggered | 24 | Stato triggered cancellato da force_reset |
| 6 | Ciclo di vita da warning a trigger | 23 | Warning poi trigger immediato |

### Esecuzione della Verifica```bash
cd fpga/formal/
sby -f wd.sby

Output previsto: ``` 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.

### Scalabilità

La verifica utilizza `CLK_FREQ=1`, `TIMEOUT_SEC=5` per mantenere lo spazio degli stati gestibile. In produzione si usa `CLK_FREQ=125000000`. L'RTL è parametrizzato — stessa logica if/else, stesse transizioni di stato. La dimostrazione su scala ridotta implica correttezza su scala di produzione.

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

## Requisiti

### Hardware

- Red Pitaya STEMlab 125-10
- Ricevitore/i AM Radio per test
- Cavo Ethernet (per connessione Red Pitaya)

### Software

| Dipendenze | macOS | Windows |
|-----------|-------|---------|
| Rust + Cargo | `curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \| sh` | Scarica `rustup-init.exe` da [rustup.rs](https://rustup.rs) |
| Node.js (LTS) | `brew install node` o [nodejs.org](https://nodejs.org) | [nodejs.org](https://nodejs.org) |
| Xcode Command Line Tools (solo macOS) | `xcode-select --install` | — |
| Visual Studio Build Tools (solo Windows) | — | [Scarica](https://visualstudio.microsoft.com/visual-cpp-build-tools/) — seleziona **"Sviluppo desktop con C++"** |

### Verifica formale (opzionale)

- SymbiYosys
- Yosys
- Z3 SMT solver

---

## Installazione

### 1. Clona il repository```bash
git clone https://github.com/Park07/amradio.git
cd amradio/am_radio

2. Crea la 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

L'app `.app` compilata si troverà 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\.

Nota: La prima build richiede circa 2-3 minuti (compilazione di Rust). Le build successive sono più veloci.

3. Configurare Red Pitaya

Connettiti via SSH al Red Pitaya:```bash ssh root@<RED_PITAYA_IP>

Default password: root

Copia i file necessari:```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/

Nota

Bitstream è già sulla scheda SD di Red Pitaya dalla fase di sviluppo.

Per ricostruire: apri project_William.xpr in Vivado, genera il bitstream,

poi scp il nuovo file .bit su Red Pitaya.

4. Ambiente Python (Red Pitaya)

Red Pitaya esegue Alpine Linux con Python 3.5. Il server SCPI non ha dipendenze esterne (solo stdlib). Il caricatore audio richiede numpy:```bash

On Red Pitaya

pip install numpy

> **Nota:** Il Python 3.5 della Red Pitaya non supporta `venv` nativamente e viene eseguito come root, quindi i pacchetti vengono installati a livello globale. Questo va bene — è un dispositivo embedded, non un server condiviso.

### 5. Ambiente Python (Sviluppo locale — opzionale)

Se desideri eseguire o modificare gli script Python localmente (ad esempio per testare l'elaborazione audio senza la Red Pitaya):```bash
python3 -m venv venv
source venv/bin/activate        # macOS/Linux
# or
.\venv\Scripts\activate         # Windows PowerShell

pip install -r requirements.txt

Aggiungi venv/ a .gitignore se non già presente.

File Audio

Il sistema riproduce tre file audio in loop: Allarme → Parte 1 → Parte 2 → (ripeti).

Tutto l'audio è ricampionato a ~5 kHz per adattarsi al buffer BRAM da 16,384 campioni dell'FPGA. Lo script axi_audio_sequence_loop.py gestisce automaticamente il ricampionamento, la conversione a 14 bit e il caricamento sequenziale.

Utilizzo

Sono necessari tre terminali SSH aperti verso il Red Pitaya, più un terminale locale per la GUI.

Nota: L'indirizzo IP del Red Pitaya potrebbe cambiare ogni volta che viene acceso. Controlla l'elenco dei client DHCP del router o usa ping rp-f0866a.local per trovarlo.

Passo 1: Connettersi al Red Pitaya

Apri un terminale e connettiti via SSH:```bash ssh root@<RED_PITAYA_IP>

Password: root

### Step 2: Caricare il bitstream FPGA

Sulla Red Pitaya (primo terminale SSH):```bash
cat /root/red_pitaya_top.bit > /dev/xdevcfg

Questo carica il progetto radio AM sulla FPGA. Necessario dopo ogni ciclo di accensione.

Step 3: Avviare il server SCPI

Sulla Red Pitaya (stesso o secondo terminale SSH):```bash python3 /root/am_scpi_server.py

Lascia questo in esecuzione — collega i comandi TCP dall'interfaccia grafica ai registri FPGA.

### Passaggio 4: Avvia il loop audio

Apri un secondo terminale SSH sulla Red Pitaya:```bash
ssh root@<RED_PITAYA_IP>
sudo python3 /root/axi_audio_sequence_loop.py

Risultato atteso:```

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: Esegui la GUI

Sulla tua macchina locale:```bash
cd gui
npm run dev

Oppure esegui il binario compilato direttamente da src-tauri/target/release/.

Passo 6: Connetti e trasmetti

1. Inserisci l'indirizzo IP di Red Pitaya
2. Clicca Connetti
3. Abilita i canali desiderati (1–12)
4. Regola le frequenze se necessario
5. Clicca AVVIA TRASMISSIONE
6. Sintonizza una radio AM su una qualsiasi frequenza abilitata

Vivado (solo per sviluppo FPGA)

Se hai bisogno di modificare il design FPGA e ricostruire il bitstream, installa Vivado 2020.1. Red Pitaya fornisce una guida di installazione qui:

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

Tutte le impostazioni di base e i tutorial di Red Pitaya sono disponibili nella documentazione ufficiale di Red Pitaya.

Struttura dei file```

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

---

## Frequenze dei Canali (Predefinite)

| Canale | Frequenza |
|---------|-----------|
| 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 |

Frequenze regolabili a runtime (intervallo 500–1700 kHz).

---

## Design di Sicurezza Watchdog
![Macchina a stati del 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

Perché diverso: Riavviare automaticamente un trasmettitore radio in un tunnel senza supervisione è pericoloso. Il sistema richiede la conferma umana prima che l'emissione RF riprenda. Fail-safe, non fail-recover.

Margine di sicurezza: Il GUI esegue il polling ogni 500 ms. Il timeout del watchdog è di 5 s. Significa 10 battiti consecutivi persi prima dell'attivazione — resistente a ritardi di rete transitori.

Note sulle Prestazioni

Raccomandazione: massimo 4–5 canali per una ricezione affidabile.

Riferimento Comandi SCPI

Test

Test Unitari Rust

11 test in tutto il backend — transizioni della macchina a stati, pub/sub del bus eventi, logica di retry e validazione della configurazione.```bash cd gui/src-tauri cargo test

### Verifica Formale (FPGA)

14 proprietà di sicurezza dimostrate matematicamente sul watchdog timer. Vedi la sezione [Verifica Formale](#formal-verification) qui sopra.

### Mock Server

Per testare la GUI senza un Red Pitaya connesso:```bash
# Terminal 1 — start mock FPGA
cd gui
npm run mock

# Terminal 2 — start GUI
cd gui
npm run dev

Quindi connettiti a 127.0.0.1:5000 nell'interfaccia grafica.

Risoluzione dei problemi

Per i futuri sviluppatori

Questo progetto verrà ereditato dalla prossima coorte EPI. Ecco cosa devi sapere.

Cosa funziona

L'intera catena del segnale è funzionante: GUI → backend Rust → TCP/SCPI → Red Pitaya → FPGA → uscita RF. La riproduzione audio si ripete automaticamente. Il watchdog disattiva l'RF se la GUI si disconnette. Tutto ciò è stato dimostrato dal vivo sull'hardware.

Cosa migliorare

Il buffer audio FPGA è limitato a 16.384 campioni in BRAM, il che impone un downsampling a ~5 kHz. Audio più lungo o di qualità superiore richiederebbe memoria esterna (DDR o scheda SD). Lo script axi_audio_sequence_loop.py ricarica l'audio su AXI con un intervallo di circa 1,4 secondi tra le tracce — la DMA eliminerebbe questo problema. Attualmente solo 4–5 canali sono pratici con una potenza del segnale utilizzabile; uno stadio amplificatore RF esterno consentirebbe l'uso simultaneo di tutti e 12 i canali.

File chiave da comprendere per primi

Leggi model.rs (il backend Rust — qui risiede tutta la logica di rete), am_scpi_server.py (il ponte tra i comandi TCP e i registri FPGA) e am_radio_ctrl.v (l'interfaccia dei registri tra software e hardware). Questi tre file sono i punti di handshake tra ogni strato del sistema.

Accesso al Red Pitaya

L'IP del Red Pitaya durante lo sviluppo era 192.168.0.101. Le credenziali SSH sono root/root. Il bitstream FPGA viene caricato automaticamente all'avvio dalla scheda SD. Se il bitstream è mancante o danneggiato, dovrai utilizzare Vivado per ricostruirlo a partire dalle sorgenti .sv/.v in fpga/.

Flusso di lavoro di sviluppo

Per le modifiche alla GUI: modifica JS/HTML in gui/src/, esegui npm run dev — ricarica a caldo il frontend. Per le modifiche al backend Rust: modifica i file in gui/src-tauri/src/, il server di sviluppo ricompila automaticamente (richiede alcuni secondi). Per le modifiche all'FPGA: modifica il Verilog in fpga/, sintetizza in Vivado, genera un nuovo bitstream, copia sulla scheda SD del Red Pitaya.

Nota importante!:

• Per il mio lavoro, i file audio erano effettivamente memorizzati all'interno del Red Pitaya. E poiché ha un buffer di memoria massimo di 32k, abbiamo dovuto dividere l'audio di emergenza in 3 parti (~4 secondi ciascuna) e sovrascriveva l'audio precedente.
• I file audio non si trovano in questo repository, ma sentiti libero di risolvere la cosa. Raccomando di usare la versione 14 del Red Pitaya per un migliore live streaming. Il 125-10 è troppo obsoleto e la maggior parte di questi problemi di memoria incontrati possono essere facilmente risolti passando al 125-15. Pavel ha un'ottima nota che potrebbe essere rilevante anche per il 125-14.

Autori

• ("Jaewoo") William Park (JW P) — Architettura software (GUI, MVC, architettura guidata da eventi), Frontend (JS), Backend (Rust), watchdog timer hardware, verifica formale, macchina a stati
• Bowen Deng — Sviluppo FPGA (NCO, modulazione AM, uscita RF)

Ringraziamenti

• University of New South Wales
• Robert Mahood — Supervisore di ingegneria
• Andrew Wong (UNSW) — Supervisore accademico

Versione finale: 13 febbraio 2026