AMラジオブレークインシステム

Red Pitaya FPGAを用いた無人トンネルでの緊急アラート送信に対応する12チャンネルAMラジオ放送システム。

特徴

アーキテクチャ

ソフトウェア層

• フレームワーク：Rust（Tauriバックエンド）＋JavaScriptフロントエンド
• MVC + イベント駆動pub/sub
  • Model (

    model.rs

    ):

    NetworkManager

    がTCP/SCPI、デバイス状態、500 msポーリング、指数バックオフ付き自動再接続を担当。
  • View (

    view.js

    ,

    index.html

    ): ステートレス – 確認済みデバイス状態のみ描画し、ハードウェア状態を仮定しない。
  • Controller (

    controller.js

    ): ユーザー入力を処理し、イベントをバスへ発行。
  • Event Bus (

    event_bus.rs

    ,

    event_bus.js

    ): 中央通信チャネル；RustがTauriブリッジ経由でJSへイベントを送出。
  • State Machine (

    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 s以内にRF出力を停止し保持；オペレーターリセットで復旧。
• SCPIサーバー (

  am_scpi_server.py

  ): Red Pitaya上で動作し、テキストコマンドを解析して周波数を位相増分へ変換し

  /dev/mem

  経由でFPGAレジスタを書き込む。

信号生成フロー

GUIクリック → invoke("set_frequency") →
model.rs が "FREQ:CH1 700000" をTCP経由送信 →
am_scpi_server.py が (700000 × 2³²) / 125 MHz を計算し phase_inc に変換 →
/dev/mem 経由でFPGAレジスタへ書き込み →
NCO がキャリアを生成 → AMモジュレーション → RF出力

形式検証

• ウォッチドッグタイマーは境界モデルチェックとk‑インデクション（SymbiYosys + Z3 SMTソルバー）で数学的に正しさが証明。
• 14の安全プロパティ（すべてPASS）＋6カバースナリオ（すべて到達）。

プロパティ概要

!rstn → counter=0, triggered=0, warning=0

triggered ONLY when counter ≥ TIMEOUT_CYCLES

カバースナリオ

1. トリガーファイア（カウンタがタイムアウトに到達）。
2. ウォーニングのみ。
3. 正確なタイムアウト境界。
4. ラストセカンドハートビート。

5. force_reset

   でトリガーからの回復。
6. ウォーニング→トリガーライフサイクル。

実行例

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.

ファイル構成

ugl_am_radio/
├── gui/
│   ├── src/
│   │   ├── index.html              # HTML + CSS
│   │   └── js/
│   │       ├── event_bus.js        # フロントエンド pub/sub + Tauri リスナー
│   │       ├── model.js            # Rust API呼び出し（ステートレス）
│   │       ├── view.js             # DOM描画
│   │       └── controller.js       # イベントハンドラ
│   └── src-tauri/src/
│       ├── main.rs                 # エントリポイント
│       ├── model.rs                # NetworkManager + DeviceState
│       ├── commands.rs             # Tauri コマンドブリッジ
│       ├── event_bus.rs            # Rust pub/sub + Tauri emit
│       ├── state_machine.rs        # 放送状態遷移
│       └── config.rs               # 定数
├── fpga/
│   ├── formal/
│   │   ├── wd.v                    # ウォッチドッグ＋14プロパティ
│   │   ├── wd.sby                  # SymbiYosys設定
│   │   └── README.md               # 形式検証ドキュメント
│   ├── am_mod.sv                   # AM変調モジュール
│   ├── am_radio_ctrl.v             # 12チャンネルAMラジオコントローラ
│   ├── axi_audio_buffer.v          # AXI音声バッファ（BRAM再生用）
│   ├── nco_sin.v                   # 数値制御発振器
│   ├── red_pitaya_top.sv           # トップレベルFPGA統合
│   ├── sine_lut_4096.mem           # 4096ポイント正弦 LUT
│   └── watchdog_timer.v            # ウォッチドッグタイマー（本番用）
├── am_scpi_server.py               # SCPIサーバー（Red Pitaya上実行）
├── axi_audio_sequence_loop.py      # 音声シーケンスローダー（アラーム→パート1→パート2ループ）
├── alarm_fast.wav                  # アラーム音
├── 0009_part1.wav                  # 緊急メッセージパート 1
├── 0009_part2_fast.wav             # パート 2
├── requirements.txt                # Python依存（numpy）
└── README.md

チャンネル周波数（デフォルト）

実行時に500–1700 kHzの範囲で調整可能。

ウォッチドッグ安全設計

• 標準ウォッチドッグ：デバイスがハング → タイマーオーバーフロー → デバイス再起動。
• 本プロジェクト用：GUIが停止するとカウンタがタイムアウトし、RF出力を即座に停止。操作員リセットまで無効化状態を維持。

理由：無人トンネルでのラジオ送信機を再起動することは危険であり、RF出力再開には必ず人的確認が必要。

安全マージン：GUIが500 msごとにポーリングし、5 sタイムアウト ⇒ 10連続ハートビート欠如でトリガー発生。

パフォーマンスメモ

おすすめ：信頼性確保のため、最大4–5チャンネル使用。

SCPIコマンドリファレンス

*IDN?

STATUS?

OUTPUT:STATE ON/OFF

CH1:FREQ 505000

CH1:OUTPUT ON/OFF

SOURCE:MSG 1

WATCHDOG:RESET

WATCHDOG:STATUS?

使用手順

1. Red PitayaへSSH

   ssh root@<RED_PITAYA_IP>
   

2. FPGAビットストリームロード（最初のターミナル）

   cat /root/red_pitaya_top.bit > /dev/xdevcfg
   

3. SCPIサーバー起動（同じまたは別ターミナル）

   python3 /root/am_scpi_server.py
   

4. 音声ループ開始（第三ターミナル）

   sudo python3 /root/axi_audio_sequence_loop.py
   

5. GUI実行：ローカルで起動、またはビルド済みバイナリを使用。

   gui/src-tauri/target/release/bundle/macos/*.app

   （macOS）や

   .exe

   （Windows）。

インストール

1. リポジトリクローン

git clone https://github.com/Park07/amradio.git
cd amradio/ugl_am_radio

2. GUIビルド

macOS

# Rust
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
source $HOME/.cargo/env

# Xcode CLIツール
xcode-select --install

# Homebrew経由でNode.js
brew install node

# ビルド
cd gui
npm install
npm run build

Windows (PowerShell)

# Rust
rustup-init.exe (https://rustup.rs)

# Visual Studio Build Tools
# 「C++によるデスクトップ開発」を選択してインストール

# Node.js LTS
# https://nodejs.org からダウンロード

# インストール確認
rustc --version
cargo --version
node --version
npm --version

# ビルド
cd gui
npm install
npm run build

3. Red Pitaya設定

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/

4. Python環境（Red Pitaya）

pip install numpy   # 音声ローダーのみ必要

テスト

• Rust単体テスト

  cd gui/src-tauri
  cargo test
  

• 形式検証 – 上記 Formal Verification セクション参照。
• モックサーバー（GUIのみ）

  # ターミナル1 — モックFPGA起動
  cd gui
  npm run mock
  
  # ターミナル2 — GUI起動
  cd gui
  npm run dev
  

  GUIで

  127.0.0.1:5000

  に接続。

トラブルシューティング

cat /root/red_pitaya_top.bit > /dev/xdevcfg

sudo python3 /root/axi_audio_sequence_loop.py

ffmpeg -i input -ac 1 -ar 44100 output.wav

link.exe

cargo

npm

xcode-select --install

今後の開発者向け

• 現状：全シグナルチェーンが機能；GUI切断時にRF出力停止。
• 改善点：オーディオバッファを16,384サンプル以上拡張、DMAギャップ解消、4–5チャンネル超えで外部アンプ対応。
• 主要ファイル：

  model.rs

  ,

  am_scpi_server.py

  ,

  am_radio_ctrl.v

  .
• 開発フロー：GUI →

  npm run dev

  ; Rustバックエンドは自動再コンパイル；FPGA → Vivado → 新ビットストリーム → SDカードへコピー。

作者

謝辞

• UGL Limited – プロジェクトスポンサー
• University of New South Wales – EPIプログラム
• Robert Mahood (UGL) – エンジニアリング監督
• Andrew Wong (UNSW) – 学術監督

最終版：2026年2月13日