Sistema de Interrupción de Radio AM

Un sistema de radiodifusión de radio AM de 12 canales que utiliza Red Pitaya FPGA para la transmisión de alertas de emergencia en túneles no tripulados.

¿Por qué radio AM en un túnel? Durante la construcción y el mantenimiento, los vehículos con radios AM estándar transitan por túneles que no tienen cobertura móvil. Las señales AM se propagan a lo largo de las estructuras del túnel a través de cables de alimentador con fugas, y los receptores son baratos, robustos y ya están presentes en todos los vehículos. El sistema transmite alertas de emergencia pregrabadas a través de múltiples frecuencias para que cualquier radio AM sintonizada en cualquier estación de la banda reciba el mensaje. Un perro guardián de hardware garantiza que la salida de RF se detenga si el sistema de control falla, porque reiniciar automáticamente un transmisor en un túnel no tripulado no es un modo de fallo aceptable.

Características

Arquitectura

Capa de Software

• Framework: backend en Rust (Tauri) + frontend en JavaScript
• Arquitectura: MVC con publicación/suscripción impulsada por eventos
• Modelo (model.rs): NetworkManager maneja TCP/SCPI, estado del dispositivo, sondeo de 500 ms, reconexión automática con retroceso exponencial
• Vista (view.js, index.html): Sin estado: solo renderiza el estado confirmado del dispositivo. Nunca asume el estado del hardware.
• Controlador (controller.js): Maneja la entrada del usuario, publica eventos en el bus
• Bus de eventos (event_bus.rs, event_bus.js): Los componentes se comunican a través de un bus central en lugar de llamarse directamente entre sí. Rust emite eventos al frontend JS a través del puente Tauri.
• Máquina de estados (state_machine.rs): INACTIVO → ARMANDO → ARMADO → INICIANDO → TRANSMITIENDO → DETENIENDO. Los estados intermedios evitan transiciones no válidas.
• Fuente de verdad: El dispositivo, no el software. La IU solo se actualiza después de que el hardware confirme.

Capa de Hardware

• NCO: 12 osciladores controlados numéricamente generan frecuencias portadoras (505–1605 kHz)
• Modulador AM: Combina la fuente de audio con cada portadora
• Escalado dinámico: La potencia de salida se ajusta según el número de canales habilitados
• Búfer de audio: BRAM almacena mensajes de emergencia pregrabados (búfer de 16,384 muestras a una velocidad de reproducción de ~5 kHz). Cargador de audio AXI disponible para carga en tiempo de ejecución.
• Temporizador de perro guardián (wd.v): A prueba de fallos de hardware: si el latido de la GUI se detiene durante 5 segundos, la salida de RF se elimina y se bloquea. Solo un restablecimiento manual del operador restaura la salida.
• Servidor SCPI (am_scpi_server.py): Se ejecuta en Red Pitaya, analiza comandos de texto, convierte frecuencias en incrementos de fase, escribe en registros FPGA a través de /dev/mem.

Flujo de generación de señales```

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

## Verificación formal

El temporizador watchdog está matemáticamente probado como correcto utilizando verificación de modelos acotada e inducción‑k (SymbiYosys + Z3 SMT solver). A diferencia de las pruebas basadas en simulación que verifican escenarios individuales, la verificación formal demuestra la corrección en **todas las entradas posibles, en todos los estados posibles, para siempre**.

### 14 Propiedades de seguridad (Todas PASAN)

| Categoría | # | Propiedad | Garantía |
|-----------|---|-----------|----------|
| **Básico** | 1 | Reset lo limpia todo | `!rstn` → counter=0, triggered=0, warning=0 |
| | 2 | Heartbeat evita disparo | Heartbeat reinicia el contador, limpia triggered y warning |
| | 6 | Deshabilitar lo mata todo | `!enable` → todas las salidas limpiadas |
| | 7 | Contador acotado | El contador nunca excede TIMEOUT_CYCLES |
| | 8 | Force reset funciona | `force_reset` limpia todo el estado |
| | 9 | Advertencia baja antes del umbral | counter < WARNING_CYCLES → warning=0 |
| **Seguridad** | 3 | **Sin disparo temprano** | **triggered SOLO cuando counter ≥ TIMEOUT_CYCLES** |
| | 4 | Disparo garantizado en timeout | Vivacidad: timeout siempre activa el disparo |
| | 5 | Advertencia antes del disparo | triggered=1 → warning=1 |
| | 5b | Contrapositivo | !warning → !triggered |
| | 10 | Advertencia alta en zona | counter > WARNING_CYCLES → warning=1 |
| | 11 | Contador incrementa correctamente | Exactamente +1 por ciclo de reloj durante el conteo |
| **Salida** | 12 | time_remaining en cero | counter=0 → time_remaining = TIMEOUT_SEC |
| | 13 | time_remaining en disparo | triggered → time_remaining = 0 |
| | 14 | time_remaining monótono | Disminuye cada ciclo durante el conteo |

### 6 Escenarios de cobertura (Todos alcanzados)

| # | Escenario | Pasos | Descripción |
|---|-----------|-------|-------------|
| 1 | Disparo se activa | 23 | El contador alcanza el timeout |
| 2 | Advertencia sin disparo | 21 | En zona de advertencia, aún no ha expirado |
| 3 | Límite exacto de timeout | 22 | Contador = TIMEOUT_CYCLES exactamente |
| 4 | Heartbeat de último segundo | 19 | Heartbeat en contador = T-1 |
| 5 | Recuperación de triggered | 24 | Estado triggered limpiado por force_reset |
| 6 | Ciclo de vida de advertencia a disparo | 23 | Advertencia luego disparo inmediato |

### Ejecutando verificación```bash
cd fpga/formal/
sby -f wd.sby

Salida esperada: ``` 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.

### Escalabilidad

La verificación utiliza `CLK_FREQ=1`, `TIMEOUT_SEC=5` para mantener manejable el espacio de estados. La producción utiliza `CLK_FREQ=125000000`. El RTL está parametrizado — la misma lógica if/else, las mismas transiciones de estado. La prueba a escala reducida implica corrección a escala de producción.

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

## Requisitos

### Hardware

- Red Pitaya STEMlab 125-10
- Receptor(es) de radio AM para pruebas
- Cable Ethernet (para conexión Red Pitaya)

### Software

| Dependencia | macOS | Windows |
|-----------|-------|---------|
| Rust + Cargo | `curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \| sh` | Descargue `rustup-init.exe` desde [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) | — | [Descargar](https://visualstudio.microsoft.com/visual-cpp-build-tools/) — seleccione **"Desktop development with C++"** |

### Verificación formal (opcional)

- SymbiYosys
- Yosys
- Z3 SMT solver

---

## Instalación

### 1. Clonar el repositorio```bash
git clone https://github.com/Park07/amradio.git
cd amradio/am_radio

2. Construir 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

La aplicación `.app` compilada estará en `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

El archivo .exe compilado estará en gui\src-tauri\target\release\.

Nota: La primera compilación toma entre 2 y 3 minutos (compilando Rust). Las compilaciones posteriores son más rápidas.

3. Configurar Red Pitaya

Conéctate por SSH a la Red Pitaya:```bash ssh root@<RED_PITAYA_IP>

Default password: root

Copiar los archivos necesarios:```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 ya está en la tarjeta SD de Red Pitaya desde el desarrollo.

Para reconstruir: abre project_William.xpr en Vivado, genera el bitstream,

luego scp el nuevo archivo .bit a la Red Pitaya.

4. Entorno Python (Red Pitaya)

La Red Pitaya ejecuta Alpine Linux con Python 3.5. El servidor SCPI no tiene dependencias externas (solo stdlib). El cargador de audio requiere numpy:```bash

On Red Pitaya

pip install numpy

> **Nota:** El Python 3.5 de Red Pitaya no soporta `venv` de serie y se ejecuta como root, por lo que los paquetes se instalan de forma global. Esto está bien: es un dispositivo embebido, no un servidor compartido.

### 5. Entorno de Python (Desarrollo local — opcional)

Si deseas ejecutar o modificar los scripts de Python localmente (por ejemplo, para probar el procesamiento de audio sin 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

Añade venv/ a .gitignore si aún no está presente.

Archivos de audio

El sistema reproduce tres archivos de audio en un bucle: Alarma → Parte 1 → Parte 2 → (repetir).

Todo el audio se reduce a ~5 kHz para caber en el búfer BRAM de 16,384 muestras de la FPGA. El script axi_audio_sequence_loop.py se encarga automáticamente del remuestreo, la conversión a 14 bits y la carga secuencial.

Uso

Necesitas tres terminales SSH abiertas hacia la Red Pitaya, más una terminal local para la GUI.

Nota: La dirección IP de la Red Pitaya puede cambiar cada vez que se enciende. Verifique la lista de clientes DHCP de su router o use ping rp-f0866a.local para encontrarla.

Paso 1: Conectar a la Red Pitaya

Abra una terminal y conéctese por SSH:```bash ssh root@<RED_PITAYA_IP>

Password: root

### Paso 2: Cargar el bitstream de FPGA

En la Red Pitaya (primer terminal SSH):```bash
cat /root/red_pitaya_top.bit > /dev/xdevcfg

Esto carga el diseño de radio AM en la FPGA. Necesario después de cada ciclo de encendido.

Paso 3: Iniciar el servidor SCPI

En la Red Pitaya (el mismo o un segundo terminal SSH):```bash python3 /root/am_scpi_server.py

Deja esto funcionando — puentea los comandos TCP desde la GUI a los registros de la FPGA.

### Paso 4: Iniciar el bucle de audio

Abre un segundo terminal SSH a la Red Pitaya:```bash
ssh root@<RED_PITAYA_IP>
sudo python3 /root/axi_audio_sequence_loop.py

Salida esperada:```

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

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

### Paso 5: Ejecutar la GUI

En tu máquina local:```bash
cd gui
npm run dev

O ejecuta el binario compilado directamente desde src-tauri/target/release/.

Paso 6: Conectar y transmitir

1. Ingresa la dirección IP de Red Pitaya
2. Haz clic en Conectar
3. Habilita los canales deseados (1–12)
4. Ajusta las frecuencias si es necesario
5. Haz clic en INICIAR TRANSMISIÓN
6. Sintoniza una radio AM en cualquier frecuencia habilitada

Vivado (solo para desarrollo FPGA)

Si necesitas modificar el diseño FPGA y reconstruir el bitstream, instala Vivado 2020.1. Red Pitaya proporciona una guía de instalación aquí:

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

Todas las configuraciones básicas y tutoriales de Red Pitaya están disponibles en la documentación oficial de Red Pitaya.

Estructura de archivos```

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

---
## Frecuencias de canales (Predeterminado)

| Canal | Frecuencia |
|---------|-----------|
| 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 |

Frecuencias ajustables en tiempo de ejecución (rango de 500–1700 kHz).

---

## Diseño de seguridad Watchdog
![Máquina de estados 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

Por qué es diferente: Reiniciar automáticamente un transmisor de radio en un túnel no tripulado es peligroso. El sistema requiere confirmación humana antes de que se reanude la salida de RF. A prueba de fallos, no recuperable ante fallos.

Margen de seguridad: La GUI sondea cada 500 ms. El tiempo de espera del watchdog es de 5 s. Eso son 10 latidos perdidos consecutivos antes de la activación — resistente a retrasos transitorios de red.

Notas de rendimiento

Recomendación: Máximo 4–5 canales para recepción fiable.

Referencia de comandos SCPI

Pruebas

Pruebas unitarias de Rust

11 pruebas en el backend — transiciones de máquina de estados, publicación/suscripción en bus de eventos, lógica de reintentos y validación de configuración.```bash cd gui/src-tauri cargo test

### Verificación Formal (FPGA)

14 propiedades de seguridad demostradas matemáticamente en el temporizador de vigilancia. Vea la sección [Verificación Formal](#formal-verification) anterior.

### Servidor Simulado

Para probar la GUI sin una Red Pitaya conectada:```bash
# Terminal 1 — start mock FPGA
cd gui
npm run mock

# Terminal 2 — start GUI
cd gui
npm run dev

Luego conéctate a 127.0.0.1:5000 en la GUI.

Solución de problemas

Para futuros desarrolladores

Este proyecto será heredado por la próxima cohorte de EPI. Esto es lo que necesitan saber.

Lo que funciona

Toda la cadena de señal es funcional: GUI → backend Rust → TCP/SCPI → Red Pitaya → FPGA → salida RF. La reproducción de audio se repite automáticamente. El watchdog desactiva la RF si la GUI se desconecta. Todo esto se ha demostrado en vivo sobre hardware.

Qué mejorar

El búfer de audio de la FPGA está limitado a 16,384 muestras en BRAM, lo que fuerza un submuestreo a ~5 kHz. Audio más largo o de mayor calidad necesitaría memoria externa (DDR o tarjeta SD). El script axi_audio_sequence_loop.py recarga el audio a través de AXI con un intervalo de ~1.4 segundos entre pistas — DMA eliminaría esto. Actualmente solo 4–5 canales son prácticos con una intensidad de señal utilizable; una etapa amplificadora externa de RF permitiría los 12 canales simultáneamente.

Archivos clave para entender primero

Leer model.rs (el backend Rust — toda la lógica de red reside aquí), am_scpi_server.py (el puente entre comandos TCP y registros FPGA), y am_radio_ctrl.v (la interfaz de registros entre software y hardware). Esos tres archivos son los puntos de enlace entre cada capa del sistema.

Acceso a Red Pitaya

La IP de Red Pitaya era 192.168.0.101 durante el desarrollo. Las credenciales SSH son root/root. El bitstream de la FPGA se carga automáticamente al arrancar desde la tarjeta SD. Si el bitstream falta o está dañado, necesitarás Vivado para reconstruirlo desde las fuentes .sv/.v en fpga/.

Flujo de trabajo de desarrollo

Para cambios en la GUI: editar JS/HTML en gui/src/, ejecutar npm run dev — recarga en caliente el frontend. Para cambios en el backend Rust: editar archivos en gui/src-tauri/src/, el servidor de desarrollo recompila automáticamente (tarda unos segundos). Para cambios en la FPGA: editar Verilog en fpga/, sintetizar en Vivado, generar nuevo bitstream, copiar a la tarjeta SD de Red Pitaya.

¡Nota importante!:

• Para mi trabajo, los archivos de audio estaban realmente almacenados dentro de la Red Pitaya. Y como tiene un búfer de memoria máximo de 32k, tuvimos que dividir el audio de emergencia en 3 partes (~4 segundos cada una), y sobrescribía el audio anterior.
• Los archivos de audio no se encuentran en este repositorio, pero siéntete libre de averiguarlo. Recomiendo usar la versión 14 de Red Pitaya para mejor transmisión en vivo. La 125-10 es demasiado anticuada y la mayoría de estos problemas de memoria encontrados se pueden resolver fácilmente actualizando a 125-15. Pavel tiene una excelente nota que también podría ser relevante para la 125-14.

Autores

• ("Jaewoo") William Park (JW P) — Arquitectura de software (GUI, MVC, arquitectura basada en eventos), Frontend (JS), Backend (Rust), temporizador watchdog por hardware, verificación formal, máquina de estados
• Bowen Deng — Desarrollo FPGA (NCO, modulación AM, salida RF)

Agradecimientos

• University of New South Wales
• Robert Mahood — Supervisor de ingeniería
• Andrew Wong (UNSW) — Supervisor académico

Versión final: 13 de febrero de 2026