AM无线电广播入侵系统

一套12通道AM无线电广播系统，使用Red Pitaya FPGA在无人隧道中传输紧急警报。

为什么在隧道中使用AM无线电？ 在施工和维护期间，配备标准AM收音机的车辆会穿越没有移动网络覆盖的隧道。AM信号通过泄漏馈线电缆沿隧道结构传播，接收器廉价、坚固且已存在于每辆车中。该系统在多个频率上广播预录的紧急警报，使得调谐到该频段任何电台的任何AM收音机都能接收到消息。硬件看门狗确保在控制系统故障时切断射频输出——因为在无人隧道中自动重启发射机是不可接受的故障模式。

特性

架构

软件层

• 框架：Rust (Tauri) 后端 + JavaScript 前端
• 架构：MVC 与事件驱动发布/订阅
• 模型 (model.rs)：NetworkManager 处理 TCP/SCPI、设备状态、500ms轮询、带指数退避的自动重连
• 视图 (view.js, index.html)：无状态 —— 仅渲染已确认的设备状态。绝不假设硬件状态。
• 控制器 (controller.js)：处理用户输入，向总线发布事件
• 事件总线 (event_bus.rs, event_bus.js)：组件通过中央总线通信而非直接调用。Rust 通过 Tauri 桥将事件发送到 JS 前端。
• 状态机 (state_machine.rs)：IDLE → ARMING → ARMED → STARTING → BROADCASTING → STOPPING。中间状态防止无效转换。
• 事实来源：设备本身，而非软件。UI 仅在硬件确认后更新。

硬件层

• NCO：12个数控振荡器生成载波频率（505–1605 kHz）
• AM调制器：将音频源与每个载波组合
• 动态缩放：根据启用的通道数量调整输出功率
• 音频缓冲区：BRAM 存储预录的紧急消息（16,384样本缓冲区，约5 kHz播放速率）。提供 AXI 音频加载器用于运行时加载。
• 看门狗定时器 (wd.v)：硬件故障安全 —— 若GUI心跳停止5秒，则切断并锁存射频输出。只有操作员手动复位才能恢复输出。
• SCPI服务器 (am_scpi_server.py)：运行于 Red Pitaya，解析文本命令，将频率转换为相位增量，通过 /dev/mem 写入FPGA寄存器。

信号生成流程```

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

---

## 形式化验证

该看门狗定时器通过有界模型检查和k-归纳（SymbiYosys + Z3 SMT求解器）在数学上被证明是正确的。与基于模拟的测试检查单个场景不同，形式化验证证明了**所有可能的输入、所有可能的状态、所有时间**的正确性。

### 14个安全属性（全部通过）

| 类别 | # | 属性 | 保证 |
|----------|---|----------|-----------|
| **基本** | 1 | 复位清除所有 | `!rstn` → counter=0, triggered=0, warning=0 |
| | 2 | 心跳防止触发 | 心跳重置计数器，清除triggered和warning |
| | 6 | 禁用杀死所有 | `!enable` → 所有输出清零 |
| | 7 | 计数器有界 | 计数器永不超出TIMEOUT_CYCLES |
| | 8 | 强制复位有效 | `force_reset` 清除所有状态 |
| | 9 | 阈值前警告为低 | counter < WARNING_CYCLES → warning=0 |
| **安全** | 3 | **无提前触发** | **仅当 counter ≥ TIMEOUT_CYCLES 时 triggered** |
| | 4 | 超时保证触发 | 活性：超时总会触发trigger |
| | 5 | 触发前警告 | triggered=1 → warning=1 |
| | 5b | 逆否命题 | !warning → !triggered |
| | 10 | 区域中警告为高 | counter > WARNING_CYCLES → warning=1 |
| | 11 | 计数器正确递增 | 计数期间每个时钟周期恰好+1 |
| **输出** | 12 | 零时time_remaining | counter=0 → time_remaining = TIMEOUT_SEC |
| | 13 | 触发时time_remaining | triggered → time_remaining = 0 |
| | 14 | time_remaining单调 | 计数期间每个周期递减 |

### 6个覆盖场景（全部达到）

| # | 场景 | 步骤 | 描述 |
|---|----------|-------|-------------|
| 1 | 触发激发 | 23 | 计数器达到超时 |
| 2 | 警告而无触发 | 21 | 在警告区，尚未超时 |
| 3 | 精确超时边界 | 22 | 计数器恰好等于TIMEOUT_CYCLES |
| 4 | 最后一秒心跳 | 19 | 计数器 = T-1 时心跳 |
| 5 | 从触发中恢复 | 24 | 通过force_reset清除触发状态 |
| 6 | 警告到触发生命周期 | 23 | 警告然后立即触发 |

### 运行验证```bash
cd fpga/formal/
sby -f wd.sby

``` 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.

### 可扩展性

验证使用 `CLK_FREQ=1`、`TIMEOUT_SEC=5` 来保持状态空间可处理。生产环境使用 `CLK_FREQ=125000000`。RTL 采用参数化设计——相同的 if/else 逻辑，相同的状态转换。缩小规模下的验证结果意味着生产规模下的正确性。

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

## 系统要求

### 硬件

- Red Pitaya STEMlab 125-10
- 用于测试的 AM 收音机（一个或多个）
- 以太网线（连接 Red Pitaya）

### 软件

| 依赖项 | macOS | Windows |
|-----------|-------|---------|
| Rust + Cargo | `curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs \| sh` | 下载 `rustup-init.exe`，来自 [rustup.rs](https://rustup.rs) |
| Node.js (LTS) | `brew install node` 或访问 [nodejs.org](https://nodejs.org) | [nodejs.org](https://nodejs.org) |
| Xcode 命令行工具（仅 macOS） | `xcode-select --install` | — |
| Visual Studio 生成工具（仅 Windows） | — | [下载](https://visualstudio.microsoft.com/visual-cpp-build-tools/) — 选择 **“使用 C++ 的桌面开发”** |

### 形式验证（可选）

- SymbiYosys
- Yosys
- Z3 SMT 求解器

---

## 安装

### 1. 克隆仓库```bash
git clone https://github.com/Park07/amradio.git
cd amradio/am_radio

2. 构建图形界面

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

构建好的 `.app` 将位于 `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

构建的 .exe 文件位于 gui\src-tauri\target\release\。

注意： 首次构建大约需要2-3分钟（编译Rust）。后续构建会更快。

3. 设置 Red Pitaya

通过SSH连接到 Red Pitaya：```bash ssh root@<RED_PITAYA_IP>

Default password: root

复制所需文件：```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/

注意

开发版中，Bitstream 已存在于 Red Pitaya SD 卡上。

如需重建：在 Vivado 中打开 project_William.xpr，生成 bitstream，然后通过 scp 将新的 .bit 文件传输到 Red Pitaya。

4. Python 环境（Red Pitaya）

Red Pitaya 运行 Alpine Linux 及 Python 3.5。SCPI 服务器没有外部依赖（仅 std Lib）。音频加载器需要 numpy：```bash

On Red Pitaya

pip install numpy

> **注意：** Red Pitaya 自带的 Python 3.5 不支持开箱即用的 `venv`，并且以 root 身份运行，因此软件包会全局安装。这没问题——它是一个嵌入式设备，而不是共享服务器。

### 5. Python 环境（本地开发——可选）

如果你想要在本地运行或修改 Python 脚本（例如，在不使用 Red Pitaya 的情况下测试音频处理）：```bash
python3 -m venv venv
source venv/bin/activate        # macOS/Linux
# or
.\venv\Scripts\activate         # Windows PowerShell

pip install -r requirements.txt

如果尚未添加，请将 venv/ 添加到 .gitignore。

音频文件

系统循环播放三个音频文件：警报 → 第一部分 → 第二部分 → (重复)。

所有音频被降采样至约 5 kHz，以适应 FPGA 的 16,384 样本 BRAM 缓冲区。axi_audio_sequence_loop.py 脚本自动处理重采样、14 位转换和顺序加载。

使用方法

你需要打开三个 SSH 终端连接到 Red Pitaya，再加上一个本地终端用于 GUI。

注意： Red Pitaya 的 IP 地址每次开机后可能会变化。请查看路由器的 DHCP 客户端列表，或使用 ping rp-f0866a.local 来查找它。

第1步：连接到 Red Pitaya

打开一个终端并 SSH 登录：```bash ssh root@<RED_PITAYA_IP>

Password: root

### 步骤2：加载FPGA比特流

在Red Pitaya（第一个SSH终端）上：```bash
cat /root/red_pitaya_top.bit > /dev/xdevcfg

这将AM无线电设计加载到FPGA上。每次上电后都需要执行。

步骤 3：启动 SCPI 服务器

在 Red Pitaya 上（同一个或第二个 SSH 终端）：```bash python3 /root/am_scpi_server.py

保持运行——它将来自 GUI 的 TCP 命令桥接到 FPGA 寄存器。

### 步骤 4：启动音频循环

打开第二个 SSH 终端连接到 Red Pitaya：```bash
ssh root@<RED_PITAYA_IP>
sudo python3 /root/axi_audio_sequence_loop.py

预期输出：```

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

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

### 步骤 5：运行图形界面

在你的本地机器上：```bash
cd gui
npm run dev

或者直接从 src-tauri/target/release/ 运行构建好的二进制文件。

步骤 6：连接并广播

1. 输入 Red Pitaya IP 地址
2. 点击 连接
3. 启用所需通道（1–12）
4. 如有需要调整频率
5. 点击 开始广播
6. 将 AM 收音机调谐到任意已启用频率

Vivado（仅用于 FPGA 开发）

如果需要修改 FPGA 设计并重建比特流，请安装 Vivado 2020.1。Red Pitaya 在此处提供了安装指南：

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

所有基本的 Red Pitaya 设置与教程均可在 Red Pitaya 官方文档 中找到。

文件结构```

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

---

## 频道频率（默认）

| 频道 | 频率 |
|---------|-----------|
| 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 |

运行时频率可调（范围 500–1700 kHz）。

---

## 看门狗安全设计
![看门狗状态机](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

不同之处： 在无人隧道中自动重启无线电发射器是危险的。系统要求人工确认后才能恢复射频输出。强调故障安全，而非故障恢复。

安全裕度： GUI 每 500 毫秒轮询一次。看门狗超时时间为 5 秒。这意味着连续错过 10 次心跳才会触发——能够抵抗瞬态网络延迟。

性能备注

建议： 最多使用 4–5 个通道以保证可靠接收。

SCPI 命令参考

测试

Rust 单元测试

后端共 11 个测试——状态机转换、事件总线发布/订阅、重试逻辑和配置验证。```bash cd gui/src-tauri cargo test

### 形式验证 (FPGA)

在看门狗定时器上经过数学证明的14项安全属性。参见上文[形式验证](#formal-verification)部分。

### 模拟服务器

用于在未连接Red Pitaya的情况下测试GUI：```bash
# Terminal 1 — start mock FPGA
cd gui
npm run mock

# Terminal 2 — start GUI
cd gui
npm run dev

Then connect to 127.0.0.1:5000 in the GUI.

故障排除

给未来开发者的说明

本项目将由下一届 EPI 团队接手。以下是你们需要了解的内容。

可正常工作的部分

完整信号链路已可用：GUI → Rust 后端 → TCP/SCPI → Red Pitaya → FPGA → 射频输出。音频播放可自动循环。若 GUI 断开连接，看门狗会终止射频输出。以上功能已在硬件上现场演示。

有待改进的部分

FPGA 音频缓冲区仅限 16,384 个样本（BRAM 内），导致必须降采样至约 5 kHz。如需更长时间或更高质量的音频，则需要外部存储器（DDR 或 SD 卡）。axi_audio_sequence_loop.py 脚本通过 AXI 重载音频，曲目间存在约 1.4 秒的空隙——DMA 可消除此间隔。目前仅 4–5 个通道能以可用信号强度运行；添加外部射频放大器级后，可同时启用全部 12 个通道。

首先需要理解的关键文件

请阅读 model.rs（Rust 后端——所有网络逻辑在此）、am_scpi_server.py（TCP 命令与 FPGA 寄存器之间的桥接）以及 am_radio_ctrl.v（软件与硬件之间的寄存器接口）。这三个文件是系统各层之间的握手点。

Red Pitaya 的访问方式

开发期间 Red Pitaya 的 IP 为 192.168.0.101。SSH 凭据为 root/root。FPGA 比特流在开机时自动从 SD 卡加载。如果比特流丢失或损坏，你需要使用 Vivado 从 fpga/ 中的 .sv/.v 源文件重新构建。

开发工作流

GUI 修改：编辑 gui/src/ 中的 JS/HTML，运行 npm run dev——前端热重载。Rust 后端修改：编辑 gui/src-tauri/src/ 中的文件，开发服务器会自动重新编译（需几秒）。FPGA 修改：编辑 fpga/ 中的 Verilog 代码，在 Vivado 中综合，生成新比特流，复制到 Red Pitaya SD 卡。

重要说明！：

• 在我的工作中，音频文件实际上存储在 Red Pitaya 内部。由于内存缓冲区最大为 32k，我们不得不将应急音频分成 3 部分（每部分约 4 秒），并且会覆盖之前的音频。
• 该仓库中不包含音频文件，但请自行解决。我建议使用 Red Pitaya 第 14 版以获得更好的实时流体验。125-10 版本过于陈旧，升级到 125-15 可以轻松解决遇到的大部分内存问题。Pavel 提供了一个可能同样适用于 125-14 的重要说明。

作者

• Jaewoo William Park (JW P) — 软件架构（GUI、MVC、事件驱动架构）、前端（JS）、后端（Rust）、硬件看门狗定时器、形式化验证、状态机
• Bowen Deng — FPGA 开发（NCO、AM 调制、射频输出）

致谢

• 新南威尔士大学
• Robert Mahood — 工程指导
• Andrew Wong（新南威尔士大学）— 学术指导

最终版本：2026年2月13日