park07/amradioFPGAベースの12チャンネルAMラジオ放送システム。無人トンネルにおけるフェイルセーフな緊急警報送信のためのハードウェアウォッチドッグの形式的検証を備えています。
無人トンネルでの緊急警報送信のための、Red Pitaya FPGAを使用した12チャンネルAM無線放送システム。
なぜトンネル内でAM無線なのか？ 建設やメンテナンス中、標準的なAMラジオを搭載した車両は、携帯電話の圏外となるトンネルを通過します。AM信号は漏洩同軸ケーブルを介してトンネル構造に沿って伝搬し、受信機は安価で堅牢であり、すべての車両に既に搭載されています。このシステムは、複数の周波数にわたって事前録音された緊急警報を放送するため、バンド内のどの局に合わせてもメッセージを受信できます。ハードウェアウォッチドッグは、制御システムが故障した場合にRF出力を確実に停止します。無人トンネルで送信機が自動的に再起動することは許容される障害モードではないからです。
| 機能 | 状態 |
|---|---|
| 12の同時キャリア周波数 | ✅ |
| 実行時周波数設定（ハードウェア変更不要） | ✅ |
| 事前録音音声によるAM変調 | ✅ |
| 動的電力スケーリング | ✅ |
| MVCアーキテクチャ（Rust + JavaScript） | ✅ |
| イベントバスによるイベント駆動型Pub/Sub | ✅ |
| ステートレスUI — デバイスが信頼できる情報源 | ✅ |
| ネットワークポーリングと自動再接続 | ✅ |
| フェイルセーフハードウェアウォッチドッグ（5秒タイムアウト） | ✅ |
| 形式検証（14のプロパティ、6のカバー、すべて証明済み） | ✅ |
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。中間状態が不正な遷移を防止。wd.v): ハードウェアフェイルセーフ — GUIのハートビートが5秒間停止すると、RF出力が停止されラッチされる。手動によるオペレーターリセットのみが出力を復元。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/main/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
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh source $HOME/.cargo/env
xcode-select --install
brew install node
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のコンパイル）。以降のビルドはより高速です。
Red Pitaya に SSH 接続します:```bash ssh root@<RED_PITAYA_IP>
必要なファイルをコピー:```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/
注記
Red PitayaはAlpine Linux上でPython 3.5を実行します。SCPIサーバーは外部依存関係がありません（stdlibのみ）。オーディオローダーはnumpyを必要とします。```bash
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 → (繰り返し)。