AM 라디오 비상 방송 시스템

Red Pitaya FPGA를 사용하는 12채널 AM 라디오 방송 시스템으로, 무인 터널에서 비상 경보를 전송합니다.

터널에서 AM 라디오를 사용하는 이유? 건설 및 유지보수 중에 표준 AM 라디오를 장착한 차량은 이동 통신이 없는 터널을 통과합니다. AM 신호는 누설 동축 케이블을 통해 터널 구조를 따라 전파되며, 수신기는 저렴하고 견고하며 모든 차량에 이미 설치되어 있습니다. 이 시스템은 사전 녹음된 비상 경보를 여러 주파수로 방송하여 대역 내 어떤 방송국에 맞춰진 AM 라디오든 메시지를 수신할 수 있도록 합니다. 하드웨어 워치독은 제어 시스템이 실패할 경우 RF 출력을 차단합니다. 무인 터널에서 송신기가 자동으로 재시작되는 것은 허용 가능한 고장 모드가 아니기 때문입니다.

특징

아키텍처

소프트웨어 계층

• 프레임워크: 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이 사전 녹음된 비상 메시지를 저장합니다(~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-유도(SymbiYosys + Z3 SMT 솔버)를 사용하여 수학적으로 올바름이 증명되었습니다. 개별 시나리오를 확인하는 시뮬레이션 기반 테스트와 달리 형식 검증은 **모든 가능한 입력, 모든 가능한 상태, 모든 시간**에 걸쳐 올바름을 증명합니다.

### 14가지 안전 속성 (모두 통과)

| 범주 | # | 속성 | 보장 |
|----------|---|----------|-----------|
| **기본** | 1 | 리셋이 모든 것을 지움 | `!rstn` → counter=0, triggered=0, warning=0 |
| | 2 | 하트비트가 트리거를 방지 | 하트비트가 counter를 재설정하고, 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 | 구역 내 경고 높음 | counter > WARNING_CYCLES → warning=1 |
| | 11 | 카운터 정확하게 증가 | 카운팅 중 클록 사이클당 정확히 +1 |
| **출력** | 12 | time_remaining이 0에서 | 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으로 triggered 상태 지워짐 |
| 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.rs](https://rustup.rs)에서 `rustup-init.exe` 다운로드 |
| 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/) — **"Desktop development with C++"** 선택 |

### 공식 검증 (선택 사항)

- SymbiYosys
- Yosys
- Z3 SMT solver

---

## 설치

### 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

The built .exe will be in 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/

참고

비트스트림은 개발 과정에서 이미 Red Pitaya SD 카드에 있습니다.

재빌드하려면: Vivado에서 project_William.xpr을 열고 비트스트림을 생성한 후,

새 .bit 파일을 Red Pitaya에 scp로 전송하십시오.

4. Python 환경 (Red Pitaya)

Red Pitaya는 Python 3.5가 포함된 Alpine Linux를 실행합니다. SCPI 서버는 외부 종속성이 없습니다(표준 라이브러리만 사용). 오디오 로더는 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

Add venv/가 아직 .gitignore에 없으면 추가하세요.

오디오 파일

시스템은 세 개의 오디오 파일을 루프로 재생합니다: 알람 → 파트 1 → 파트 2 → (반복).

모든 오디오는 FPGA의 16,384-샘플 BRAM 버퍼에 맞게 약 5 kHz로 다운샘플링됩니다. axi_audio_sequence_loop.py 스크립트가 리샘플링, 14비트 변환 및 순차적 로딩을 자동으로 처리합니다.

사용법

Red Pitaya에 연결된 SSH 터미널 세 개와 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단계: 오디오 루프 시작

Red Pitaya에 두 번째 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. 연결 클릭
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

다른 점: 무인 터널에서 무선 송신기를 자동으로 재시작하는 것은 위험합니다. 시스템은 RF 출력이 재개되기 전에 사람의 확인을 요구합니다. Fail-safe(안전 우선) 방식이며, Fail-recover(자동 복구) 방식이 아닙니다.

안전 여유: 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(소프트웨어와 하드웨어 간의 레지스터 인터페이스)를 읽어보십시오. 이 세 파일은 시스템의 모든 계층 간 연결 지점입니다.

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이기 때문에 비상 오디오를 각각 약 4초 길이의 3개 부분으로 나누었으며, 이전 오디오를 덮어쓰는 방식이었습니다.
• 오디오 파일은 이 저장소에 포함되어 있지 않지만, 직접 알아서 처리하시기 바랍니다. 라이브 스트리밍을 위해 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 출력)

감사의 글

• 뉴사우스웨일스 대학교 (University of New South Wales)
• Robert Mahood — 엔지니어링 지도교수
• Andrew Wong (UNSW) — 학술 지도교수

최종 버전: 2026년 2월 13일