park07/amradioFPGA 기반 12채널 AM 라디오 방송 시스템으로, 무인 터널에서 페일세이프 비상 경보 전송을 위한 하드웨어 워치독의 정형 검증을 포함합니다.
Red Pitaya FPGA를 사용하는 12채널 AM 라디오 방송 시스템으로, 무인 터널에서 비상 경보를 전송합니다.
터널에서 AM 라디오를 사용하는 이유? 건설 및 유지보수 중에 표준 AM 라디오를 장착한 차량은 이동 통신이 없는 터널을 통과합니다. AM 신호는 누설 동축 케이블을 통해 터널 구조를 따라 전파되며, 수신기는 저렴하고 견고하며 모든 차량에 이미 설치되어 있습니다. 이 시스템은 사전 녹음된 비상 경보를 여러 주파수로 방송하여 대역 내 어떤 방송국에 맞춰진 AM 라디오든 메시지를 수신할 수 있도록 합니다. 하드웨어 워치독은 제어 시스템이 실패할 경우 RF 출력을 차단합니다. 무인 터널에서 송신기가 자동으로 재시작되는 것은 허용 가능한 고장 모드가 아니기 때문입니다.
| 기능 | 상태 |
|---|---|
| 12개의 동시 반송파 주파수 | ✅ |
| 런타임 주파수 설정 (하드웨어 변경 불필요) | ✅ |
| 사전 녹음된 오디오를 사용한 AM 변조 | ✅ |
| 동적 전력 조정 | ✅ |
| MVC 아키텍처 (Rust + JavaScript) | ✅ |
| 이벤트 버스를 통한 이벤트 기반 발행/구독 | ✅ |
| 무상태 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-유도(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/main/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
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
The built .exe will be in 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는 Python 3.5가 포함된 Alpine Linux를 실행합니다. SCPI 서버는 외부 종속성이 없습니다(표준 라이브러리만 사용). 오디오 로더는 numpy가 필요합니다:```bash
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