park07/amradioSistema di trasmissione radio AM a 12 canali basato su FPGA con verifica formale di un watchdog hardware per la trasmissione di allarmi di emergenza a prova di guasto in gallerie non presidiate.
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.
| Caratteristica | Stato |
|---|---|
| 12 frequenze portanti simultanee | ✅ |
| Configurazione della frequenza a runtime (nessuna modifica hardware) | ✅ |
| Modulazione AM con audio preregistrato | ✅ |
| Scala dinamica della potenza | ✅ |
| Architettura MVC (Rust + JavaScript) | ✅ |
| Pub/sub guidato da eventi tramite bus eventi | ✅ |
| UI senza stato — il dispositivo è la fonte della verità | ✅ |
| Polling di rete e riconnessione automatica | ✅ |
| Watchdog hardware con fail-safe (timeout 5 s) | ✅ |
| Verifica formale (14 proprietà, 6 coperture, tutte provate) | ✅ |
model.rs): NetworkManager gestisce TCP/SCPI, stato del dispositivo, polling a 500 ms, riconnessione automatica con backoff esponenzialeview.js, index.html): Senza stato — rende solo lo stato confermato del dispositivo. Non assume mai lo stato hardware.controller.js): Gestisce l'input utente, pubblica eventi sul busevent_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.rs): IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING. Gli stati intermedi impediscono transizioni non valide.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.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.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/main/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