park07/amradioSistema de radiodifusión AM de 12 canales basado en FPGA con verificación formal de un watchdog de hardware para transmisión de alertas de emergencia a prueba de fallos en túneles no tripulados.
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ística | Estado |
|---|---|
| 12 frecuencias portadoras simultáneas | ✅ |
| Configuración de frecuencia en tiempo de ejecución (sin cambios de hardware) | ✅ |
| Modulación AM con audio pregrabado | ✅ |
| Escalado dinámico de potencia | ✅ |
| Arquitectura MVC (Rust + JavaScript) | ✅ |
| Publicar/suscribir impulsado por eventos mediante bus de eventos | ✅ |
| IU sin estado: el dispositivo es la fuente de verdad | ✅ |
| Sondeo de red y reconexión automática | ✅ |
| Perro guardián de hardware a prueba de fallos (tiempo de espera de 5 s) | ✅ |
| Verificación formal (14 propiedades, 6 cubrimientos, todas probadas) | ✅ |
model.rs): NetworkManager maneja TCP/SCPI, estado del dispositivo, sondeo de 500 ms, reconexión automática con retroceso exponencialview.js, index.html): Sin estado: solo renderiza el estado confirmado del dispositivo. Nunca asume el estado del hardware.controller.js): Maneja la entrada del usuario, publica eventos en el busevent_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.state_machine.rs): INACTIVO → ARMANDO → ARMADO → INICIANDO → TRANSMITIENDO → DETENIENDO. Los estados intermedios evitan transiciones no válidas.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.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.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