park07/amradioSistema de transmissão de rádio AM de 12 canais baseado em FPGA com verificação formal de um watchdog de hardware para transmissão de alertas de emergência à prova de falhas em túneis não tripulados.
Um sistema de transmissão de rádio AM de 12 canais usando FPGA Red Pitaya para transmissão de alertas de emergência em túneis não tripulados.
Por que rádio AM em um túnel? Durante a construção e manutenção, veículos com rádios AM padrão transitam por túneis que não possuem cobertura móvel. Os sinais AM se propagam ao longo das estruturas do túnel por meio de cabos leaky feeder, e os receptores são baratos, robustos e já estão presentes em todos os veículos. O sistema transmite alertas de emergência pré-gravados em múltiplas frequências, de modo que qualquer rádio AM sintonizado em qualquer estação da banda receba a mensagem. Um watchdog de hardware garante que a saída de RF seja desligada se o sistema de controle falhar — porque reiniciar automaticamente um transmissor em um túnel não tripulado não é um modo de falha aceitável.
| Funcionalidade | Status |
|---|---|
| 12 frequências de portadora simultâneas | ✅ |
| Configuração de frequência em tempo de execução (sem alterações de hardware) | ✅ |
| Modulação AM com áudio pré-gravado | ✅ |
| Escalonamento dinâmico de potência | ✅ |
| Arquitetura MVC (Rust + JavaScript) | ✅ |
| Pub/sub orientado a eventos via barramento de eventos | ✅ |
| UI sem estado — o dispositivo é a fonte da verdade | ✅ |
| Polling de rede e reconexão automática | ✅ |
| Watchdog de hardware à prova de falhas (timeout de 5s) | ✅ |
| Verificação formal (14 propriedades, 6 coberturas, todas comprovadas) | ✅ |
model.rs): NetworkManager gerencia TCP/SCPI, estado do dispositivo, polling de 500ms, reconexão automática com backoff exponencialview.js, index.html): Sem estado — apenas renderiza o estado confirmado do dispositivo. Nunca assume o estado do hardware.controller.js): Lida com a entrada do usuário, publica eventos no barramentoevent_bus.rs, event_bus.js): Componentes se comunicam por meio de um barramento central em vez de chamarem uns aos outros diretamente. Rust emite eventos para o frontend JS via ponte Tauri.state_machine.rs): IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING. Estados intermediários impedem transições inválidas.wd.v): Hardware à prova de falhas — se o heartbeat da GUI parar por 5 segundos, a saída de RF é desligada e travada. Apenas uma reinicialização manual do operador restaura a saída.am_scpi_server.py): Executa no Red Pitaya, analisa comandos de texto, converte frequências em incrementos de fase, escreve nos registros da FPGA via /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ção Formal
O temporizador watchdog é matematicamente comprovado correto usando verificação de modelo limitada e indução-k (SymbiYosys + resolvedor SMT Z3). Diferente de testes baseados em simulação que verificam cenários individuais, a verificação formal prova a correção em **todas as entradas possíveis, em todos os estados possíveis, para todo o tempo**.
### 14 Propriedades de Segurança (Todas PASS)
| Categoria | # | Propriedade | Garantia |
|-----------|---|-------------|----------|
| **Básico** | 1 | Reset limpa tudo | `!rstn` → contador=0, triggered=0, warning=0 |
| | 2 | Heartbeat previne disparo | Heartbeat reseta contador, limpa triggered e warning |
| | 6 | Desabilitar desliga tudo | `!enable` → todas as saídas limpas |
| | 7 | Contador limitado | Contador nunca excede TIMEOUT_CYCLES |
| | 8 | Forçar reset funciona | `force_reset` limpa todo o estado |
| | 9 | Aviso baixo antes do limite | contador < WARNING_CYCLES → warning=0 |
| **Segurança** | 3 | **Sem disparo precoce** | **triggered SOMENTE quando contador ≥ TIMEOUT_CYCLES** |
| | 4 | Disparo garantido no tempo limite | Vivacidade: timeout sempre ativa o disparo |
| | 5 | Aviso antes do disparo | triggered=1 → warning=1 |
| | 5b | Contrapositiva | !warning → !triggered |
| | 10 | Aviso alto na zona | contador > WARNING_CYCLES → warning=1 |
| | 11 | Contador incrementa corretamente | Exatamente +1 por ciclo de clock durante a contagem |
| **Saída** | 12 | time_remaining em zero | contador=0 → time_remaining = TIMEOUT_SEC |
| | 13 | time_remaining no disparo | triggered → time_remaining = 0 |
| | 14 | time_remaining monotônico | Diminui a cada ciclo durante a contagem |
### 6 Cenários de Cobertura (Todos Alcançados)
| # | Cenário | Passos | Descrição |
|---|---------|--------|-----------|
| 1 | Disparo ativado | 23 | Contador atinge o tempo limite |
| 2 | Aviso sem disparo | 21 | Na zona de aviso, ainda não excedeu o tempo limite |
| 3 | Limite exato de timeout | 22 | Contador = TIMEOUT_CYCLES exatamente |
| 4 | Heartbeat de último segundo | 19 | Heartbeat no contador = T-1 |
| 5 | Recuperação após disparo | 24 | Estado de disparo limpo por force_reset |
| 6 | Ciclo de aviso para disparo | 23 | Aviso seguido de disparo imediato |```bash
cd fpga/formal/
sby -f wd.sby
Saída 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.
### Escalabilidade
A verificação usa `CLK_FREQ=1`, `TIMEOUT_SEC=5` para manter o espaço de estados tratável. A produção usa `CLK_FREQ=125000000`. O RTL é parametrizado — mesma lógica if/else, mesmas transições de estado. A prova em escala reduzida implica correção em escala de produção.
Consulte [`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 rádio AM para teste
- Cabo Ethernet (para conexão do Red Pitaya)
### Software