Sistema de Intervenção por Rádio AM

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.

Funcionalidades

Arquitetura

Camada de Software

• Framework: Backend Rust (Tauri) + frontend JavaScript
• Arquitetura: MVC com pub/sub orientado a eventos
• Model (model.rs): NetworkManager gerencia TCP/SCPI, estado do dispositivo, polling de 500ms, reconexão automática com backoff exponencial
• View (view.js, index.html): Sem estado — apenas renderiza o estado confirmado do dispositivo. Nunca assume o estado do hardware.
• Controller (controller.js): Lida com a entrada do usuário, publica eventos no barramento
• Barramento de Eventos (event_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.
• Máquina de Estados (state_machine.rs): IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING. Estados intermediários impedem transições inválidas.
• Fonte da Verdade: O dispositivo, não o software. A UI só é atualizada após confirmação do hardware.

Camada de Hardware

• NCO: 12 Osciladores Controlados Numericamente geram frequências portadoras (505–1605 kHz)
• Modulador AM: Combina a fonte de áudio com cada portadora
• Escalonamento Dinâmico: A potência de saída se ajusta com base no número de canais habilitados
• Buffer de Áudio: BRAM armazena mensagens de emergência pré-gravadas (buffer de 16.384 amostras a uma taxa de reprodução de ~5 kHz). Carregador de áudio AXI disponível para carregamento em tempo de execução.
• Timer Watchdog (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.
• Servidor SCPI (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.

Fluxo de Geração de Sinal```

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/HEAD/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

| Dependência | macOS | Windows |
|-----------|-------|---------|
| Rust + Cargo | `curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \| sh` | Baixe `rustup-init.exe` em [rustup.rs](https://rustup.rs) |
| Node.js (LTS) | `brew install node` ou [nodejs.org](https://nodejs.org) | [nodejs.org](https://nodejs.org) |
| Ferramentas de Linha de Comando do Xcode (somente macOS) | `xcode-select --install` | — |
| Ferramentas de Build do Visual Studio (somente Windows) | — | [Baixar](https://visualstudio.microsoft.com/visual-cpp-build-tools/) — selecione **"Desenvolvimento de desktop com C++"** |

### Verificação Formal (opcional)

- SymbiYosys
- Yosys
- Z3 SMT solver

---

## Instalação

### 1. Clone o repositório```bash
git clone https://github.com/Park07/amradio.git
cd amradio/am_radio

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

O `.app` compilado estará em `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

O .exe compilado estará em gui\src-tauri\target\release\.

Nota: A primeira compilação leva cerca de 2–3 minutos (compilando Rust). Compilações subsequentes são mais rápidas.

3. Configurar Red Pitaya

SSH para o Red Pitaya:```bash ssh root@<RED_PITAYA_IP>

Default password: root

Copiar ficheiros necessários:```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 is already on the Red Pitaya SD card from development.

To rebuild: open project_William.xpr in Vivado, generate bitstream,

then scp the new .bit file to the Red Pitaya.

4. Ambiente Python (Red Pitaya)

O Red Pitaya executa Alpine Linux com Python 3.5. O servidor SCPI não possui dependências externas (apenas stdlib). O carregador de áudio requer numpy:```bash

On Red Pitaya

pip install numpy

> **Nota:** O Python 3.5 do Red Pitaya não suporta `venv` nativamente e é executado como root, então os pacotes são instalados globalmente. Isso é normal — é um dispositivo embarcado, não um servidor compartilhado.

### 5. Ambiente Python (Desenvolvimento Local — opcional)```bash
python3 -m venv venv
source venv/bin/activate        # macOS/Linux
# or
.\venv\Scripts\activate         # Windows PowerShell

pip install -r requirements.txt

Adicione venv/ ao .gitignore se ainda não estiver presente.

Arquivos de Áudio

O sistema toca três arquivos de áudio em loop: Alarme → Parte 1 → Parte 2 → (repetir).

Todo o áudio é reamostrado para ~5 kHz para caber no buffer BRAM de 16.384 amostras da FPGA. O script axi_audio_sequence_loop.py lida automaticamente com a reamostragem, conversão para 14 bits e carregamento sequencial.

Uso

Você precisa de três terminais SSH abertos para o Red Pitaya, mais um terminal local para a GUI.

Nota: O endereço IP do Red Pitaya pode mudar cada vez que ele é ligado. Verifique a lista de clientes DHCP do seu roteador ou use ping rp-f0866a.local para encontrá-lo.

Passo 1: Conectar ao Red Pitaya

Abra um terminal e faça SSH:```bash ssh root@<RED_PITAYA_IP>

Password: root

### Passo 2: Carregar o bitstream do FPGA

Na Red Pitaya (primeiro terminal SSH):```bash
cat /root/red_pitaya_top.bit > /dev/xdevcfg

Isso carrega o design de rádio AM na FPGA. Necessário após cada ciclo de energia.

Passo 3: Iniciar o servidor SCPI

Na Red Pitaya (mesmo terminal SSH ou segundo terminal):```bash python3 /root/am_scpi_server.py

Deixe isso em execução — ele faz a ponte entre comandos TCP da GUI e registros FPGA.

### Passo 4: Inicie o loop de áudio

Abra um segundo terminal SSH para a Red Pitaya:```bash
ssh root@<RED_PITAYA_IP>
sudo python3 /root/axi_audio_sequence_loop.py

Saída 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

### Passo 5: Executar a GUI

Na sua máquina local:```bash
cd gui
npm run dev

Ou execute o binário compilado diretamente de src-tauri/target/release/.

Passo 6: Conectar e transmitir

1. Insira o endereço IP do Red Pitaya
2. Clique em Conectar
3. Ative os canais desejados (1–12)
4. Ajuste as frequências, se necessário
5. Clique em INICIAR TRANSMISSÃO
6. Sintonize um rádio AM em qualquer frequência habilitada

Vivado (apenas para desenvolvimento FPGA)

Se precisar modificar o design FPGA e reconstruir o bitstream, instale o Vivado 2020.1. O Red Pitaya fornece um guia de configuração aqui:

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

Todas as configurações básicas e tutoriais do Red Pitaya estão disponíveis na documentação oficial do Red Pitaya.

Estrutura de Arquivos```

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

---

## Frequências dos Canais (Padrão)

| Canal | Frequência |
|---------|-----------|
| 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 |

Frequências ajustáveis em tempo de execução (faixa de 500–1700 kHz).

---

## Design de Segurança Watchdog
![Watchdog State Machine](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 que é diferente: Reiniciar automaticamente um transmissor de rádio em um túnel não tripulado é perigoso. O sistema exige confirmação humana antes que a saída de RF seja retomada. À prova de falhas, não de recuperação de falhas.

Margem de segurança: A GUI pesquisa a cada 500ms. O tempo limite do watchdog é de 5s. Isso equivale a 10 batimentos cardíacos consecutivos perdidos antes do disparo — resiliente contra atrasos de rede transitórios.

Notas de Desempenho

Recomendação: máximo de 4–5 canais para recepção confiável.

Referência de Comandos SCPI

Testes

Testes Unitários em Rust

11 testes em todo o backend — transições de máquina de estados, pub/sub do barramento de eventos, lógica de repetição e validação de configuração.```bash cd gui/src-tauri cargo test

### Verificação Formal (FPGA)

14 propriedades de segurança matematicamente comprovadas no watchdog timer. Veja a seção [Verificação Formal](#formal-verification) acima.

### Servidor Mock

Para testar a GUI sem um Red Pitaya conectado:```bash
# Terminal 1 — start mock FPGA
cd gui
npm run mock

# Terminal 2 — start GUI
cd gui
npm run dev

Em seguida, conecte-se a 127.0.0.1:5000 na GUI.

Solução de Problemas

Para Futuros Desenvolvedores

Este projeto será herdado pela próxima turma do EPI. Aqui está o que você precisa saber.

O que funciona

A cadeia completa de sinais é funcional: GUI → backend Rust → TCP/SCPI → Red Pitaya → FPGA → saída RF. A reprodução de áudio se repete automaticamente. O watchdog desliga a RF se a GUI desconectar. Tudo isso foi demonstrado ao vivo em hardware.

O que melhorar

O buffer de áudio da FPGA é limitado a 16.384 amostras na BRAM, o que força o downsampling para ~5 kHz. Áudio mais longo ou de maior qualidade exigiria memória externa (DDR ou cartão SD). O script axi_audio_sequence_loop.py recarrega áudio via AXI com um intervalo de ~1,4 segundos entre as faixas — o DMA eliminaria isso. Atualmente, apenas 4–5 canais são práticos com força de sinal utilizável; um estágio de amplificador RF externo permitiria todos os 12 canais simultaneamente.

Arquivos-chave para entender primeiro

Leia model.rs (o backend Rust — toda a lógica de rede reside aqui), am_scpi_server.py (a ponte entre comandos TCP e registros da FPGA) e am_radio_ctrl.v (a interface de registros entre software e hardware). Esses três arquivos são os pontos de sincronização entre todas as camadas do sistema.

Acesso ao Red Pitaya

O IP do Red Pitaya durante o desenvolvimento era 192.168.0.101. As credenciais SSH são root/root. O bitstream da FPGA é carregado automaticamente na inicialização a partir do cartão SD. Se o bitstream estiver faltando ou corrompido, você precisará do Vivado para reconstruí-lo a partir das fontes .sv/.v em fpga/.

Fluxo de trabalho de desenvolvimento

Para alterações na GUI: edite JS/HTML em gui/src/, execute npm run dev — recarrega o frontend automaticamente. Para alterações no backend Rust: edite arquivos em gui/src-tauri/src/, o servidor de desenvolvimento recompila automaticamente (leva alguns segundos). Para alterações na FPGA: edite Verilog em fpga/, sintetize no Vivado, gere novo bitstream, copie para o cartão SD do Red Pitaya.

Nota Importante!:

• Para o meu trabalho, os arquivos de áudio foram armazenados dentro do Red Pitaya. E como ele tem um buffer de memória máximo de 32k, tivemos que dividir o áudio de emergência em 3 partes (~4 segundos cada), e ele reescrevia o áudio anterior.
• Os arquivos de áudio não estão neste repositório, mas sinta-se à vontade para descobrir isso. Recomendo usar a versão 14 do Red Pitaya para uma melhor transmissão ao vivo. O 125-10 é muito desatualizado e a maioria desses problemas de memória encontrados pode ser facilmente resolvida atualizando para o 125-15. Pavel tem uma ótima nota que pode ser relevante também para o 125-14.

Autores

• ("Jaewoo") William Park (JW P) — Arquitetura de software (GUI, MVC, arquitetura orientada a eventos), Frontend (JS), Backend (Rust), temporizador watchdog de hardware, verificação formal, máquina de estados
• Bowen Deng — Desenvolvimento FPGA (NCO, modulação AM, saída RF)

Agradecimentos

• University of New South Wales
• Robert Mahood — Supervisor de engenharia
• Andrew Wong (UNSW) — Supervisor acadêmico

Versão Final: 13 de Fevereiro de 2026