AM Radio Break-in System

無人トンネルでの緊急警報送信のための、Red Pitaya FPGAを使用した12チャンネルAM無線放送システム。

なぜトンネル内でAM無線なのか？ 建設やメンテナンス中、標準的なAMラジオを搭載した車両は、携帯電話の圏外となるトンネルを通過します。AM信号は漏洩同軸ケーブルを介してトンネル構造に沿って伝搬し、受信機は安価で堅牢であり、すべての車両に既に搭載されています。このシステムは、複数の周波数にわたって事前録音された緊急警報を放送するため、バンド内のどの局に合わせてもメッセージを受信できます。ハードウェアウォッチドッグは、制御システムが故障した場合にRF出力を確実に停止します。無人トンネルで送信機が自動的に再起動することは許容される障害モードではないからです。

特徴

アーキテクチャ

ソフトウェア層

• フレームワーク: Rust (Tauri) バックエンド + JavaScript フロントエンド
• アーキテクチャ: イベント駆動型Pub/Subを備えた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に事前録音された緊急メッセージを格納（約5 kHz再生レートで16,384サンプルバッファ）。実行時ロード用にAXIオーディオローダーが利用可能。
• ウォッチドッグタイマー (wd.v): ハードウェアフェイルセーフ — GUIのハートビートが5秒間停止すると、RF出力が停止されラッチされる。手動によるオペレーターリセットのみが出力を復元。
• 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-induction（SymbiYosys + Z3 SMTソルバ）を用いて数学的に正しいことが証明されています。個々のシナリオをチェックするシミュレーションベースのテストとは異なり、形式検証は**あらゆる可能な入力、すべての状態、全時間**にわたって正しさを証明します。

### 14の安全特性（すべてPASS）

| カテゴリ | # | プロパティ | 保証内容 |
|----------|---|----------|-----------|
| **基本** | 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 | **早期トリガなし** | **triggeredはcounter ≥ TIMEOUT_CYCLESの場合のみ** |
| | 4 | タイムアウト時にトリガが確実に発生 | 活性: タイムアウトは常にトリガを発生させる |
| | 5 | トリガ前に警告 | triggered=1 → warning=1 |
| | 5b | 対偶 | !warning → !triggered |
| | 10 | 警告ゾーンで警告がHigh | counter > WARNING_CYCLES → warning=1 |
| | 11 | カウンタの正しい増加 | カウント中、クロックサイクルごとに正確に+1 |
| **出力** | 12 | 残り時間がゼロ | counter=0 → time_remaining = TIMEOUT_SEC |
| | 13 | トリガ時の残り時間 | triggered → time_remaining = 0 |
| | 14 | 残り時間の単調減少 | カウント中、サイクルごとに減少 |

### 6つのカバレッジシナリオ（すべて到達）

| # | シナリオ | ステップ数 | 説明 |
|---|----------|-------|-------------|
| 1 | トリガ発火 | 23 | カウンタがタイムアウトに達する |
| 2 | トリガなしの警告 | 21 | 警告ゾーン内、まだタイムアウトしていない |
| 3 | 正確なタイムアウト境界 | 22 | カウンタ = TIMEOUT_CYCLES ちょうど |
| 4 | 直前のハートビート | 19 | カウンタ = T-1 でハートビート |
| 5 | トリガからの回復 | 24 | 強制リセットでトリガ状態がクリアされる |
| 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ラジオ受信機
- Ethernetケーブル（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 Command Line Tools (macOSのみ) | `xcode-select --install` | — |
| Visual Studio Build Tools (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. 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

ビルドされた `.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 のセットアップ

Red Pitaya に SSH 接続します:```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を開き、ビットストリームを生成してから、

新しい.bitファイルをscpでRed Pitayaに転送してください。

4. Python環境 (Red Pitaya)

Red PitayaはAlpine Linux上でPython 3.5を実行します。SCPIサーバーは外部依存関係がありません（stdlibのみ）。オーディオローダーはnumpyを必要とします。```bash

On Red Pitaya

pip install numpy

> **Note:** Red PitayaのPython 3.5は`venv`を標準でサポートしておらず、rootで実行されるため、パッケージはグローバルにインストールされます。これは問題ありません — 共有サーバーではなく組み込みデバイスだからです。

### 5. 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 に追加してください。

オーディオファイル

システムは3つのオーディオファイルをループで再生します: アラーム → パート1 → パート2 → (繰り返し)。

すべてのオーディオは約5 kHzにダウンサンプリングされ、FPGAの16,384サンプルBRAMバッファに収まるようにします。axi_audio_sequence_loop.py スクリプトがリサンプリング、14ビット変換、およびシーケンシャルロードを自動的に処理します。

使用方法

Red Pitayaに3つのSSHターミナルを開き、さらにGUI用に1つのローカルターミナルが必要です。

注: 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上で（同じまたは2つ目のSSHターミナル）：```bash python3 /root/am_scpi_server.py

このまま実行したままにしてください — GUIからのTCPコマンドとFPGAレジスタを橋渡しします。

### ステップ4: オーディオループを開始

Red Pitayaに2つ目のSSHターミナルを開いてください:```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: GUIを実行する

ローカルマシン上で:```bash
cd gui
npm run dev

または、ビルド済みのバイナリを src-tauri/target/release/ から直接実行します。

ステップ6: 接続とブロードキャスト

1. Red PitayaのIPアドレスを入力
2. Connectをクリック
3. 希望するチャンネル（1〜12）を有効にする
4. 必要に応じて周波数を調整
5. START BROADCASTをクリック
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の範囲）。

---

## ウォッチドッグ安全設計
![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

何が違うのか: 無人トンネル内で無線送信機を自動再起動するのは危険です。本システムではRF出力を再開する前に人間の確認を必要とします。フェイルセーフであり、フェイルリカバリではありません。

安全マージン: GUIは500msごとにポーリングします。ウォッチドッグタイムアウトは5秒です。つまりトリガー発動までに連続10回のハートビート欠落に耐えるため、一時的なネットワーク遅延に対して堅牢です。

パフォーマンスノート

推奨: 安定した受信には最大4～5チャンネル。

SCPIコマンドリファレンス

テスト

Rust単体テスト

バックエンド全体で11のテスト – 状態遷移、イベントバスのpub/sub、リトライロジック、設定バリデーションをカバーしています。```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

次に、GUIで 127.0.0.1:5000 に接続します。

トラブルシューティング

将来の開発者へ

このプロジェクトは次のEPIコホートに引き継がれます。知っておくべきことを以下にまとめます。

動作する部分

完全な信号チェーンが機能します: GUI → Rustバックエンド → TCP/SCPI → Red Pitaya → FPGA → RF出力。オーディオ再生は自動的にループします。ウォッチドッグはGUIが切断されるとRFを強制停止します。これらはすべてハードウェア上でライブデモンストレーション済みです。

改善すべき点

FPGAオーディオバッファはBRAM上で16,384サンプルに制限されており、そのため約5kHzへのダウンサンプリングが必要です。より長い、または高品質なオーディオには外部メモリ（DDRまたはSDカード）が必要です。axi_audio_sequence_loop.py スクリプトはAXI経由でオーディオを再読み込みしますが、トラック間に約1.4秒のギャップがあります。DMAを使用すればこれを解消できます。現在、使用可能な信号強度で実用的なのは4～5チャンネルのみです。外部RF増幅段を追加すれば、12チャンネルすべてを同時に使用できるようになります。

最初に理解すべき主要ファイル

model.rs（Rustバックエンド — すべてのネットワークロジックがここにあります）、am_scpi_server.py（TCPコマンドとFPGAレジスタ間のブリッジ）、および am_radio_ctrl.v（ソフトウェアとハードウェア間のレジスタインターフェース）を読んでください。これら3つのファイルがシステムのすべてのレイヤー間の接続点です。

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変調、RF出力）

謝辞

• ニューサウスウェールズ大学
• Robert Mahood — エンジニアリング監督
• Andrew Wong（UNSW） — 学術指導教員

最終版: 2026年2月13日