임베디드 시스템을 설계할 때 엔지니어로서 가장 등골이 서늘해지는 순간은 언제일까요? 바로 시스템이 ‘죽었는데 살아있는 척’ 할 때입니다. 특히 무인 터널의 비상 방송 시스템이라면, 오작동은 단순한 버그가 아니라 안전 사고로 이어질 수 있습니다.

최근 Hacker News에 올라온 Park07/amradio 프로젝트는 꽤 흥미로운 접근법을 보여줍니다. Red Pitaya FPGA를 기반으로 12채널 AM 라디오 방송 시스템을 구축했는데, 단순히 ‘방송이 된다’는 수준을 넘어 Rust, Tauri, 그리고 하드웨어 정형 검증(Formal Verification) 까지 동원해 안전성을 수학적으로 증명해냈습니다.

보통의 사이드 프로젝트나 학부 캡스톤 수준에서는 보기 힘든 ‘진지한 엔지니어링’의 냄새가 납니다. 오늘은 이 프로젝트가 어떻게 안전 필수(Safety-Critical) 시스템을 현대적인 스택으로 풀어냈는지, 그리고 제가 느낀 장단점은 무엇인지 깊게 파보겠습니다.

1. 아키텍처: “장치가 곧 진실이다 (Device is Source of Truth)”

이 프로젝트의 아키텍처에서 가장 마음에 드는 점은 Stateless UI 철학입니다.

많은 IoT 프로젝트들이 웹 프론트엔드(JS)에 상태를 저장하고, 하드웨어와 동기화를 맞추느라 고생합니다. “UI에서는 켜짐으로 나오는데 실제 장비는 꺼져있는” 상태 불일치 문제는 아주 흔하죠. 하지만 이 프로젝트는 Rust(Tauri) 백엔드와 JS 프론트엔드를 철저하게 View 역할로만 제한했습니다.

• Controller: 사용자 입력을 받아 Event Bus로 던짐
• Model (Rust): TCP/SCPI를 통해 하드웨어에 명령 전달 및 폴링
• View: 하드웨어로부터 확인된(confirmed) 상태만 렌더링

즉, UI가 “켜라”고 명령을 보내도, 하드웨어가 “나 켜졌어”라고 응답하기 전까지 UI 스위치는 켜지지 않습니다. 이는 산업용 제어 시스템(ICS)에서 필수적인 패턴인데, 이를 Rust의 타입 시스템과 결합해 깔끔하게 구현했습니다. state_machine.rs를 보면 IDLE -> ARMING -> ARMED 등의 상태 전이가 명시되어 있어, 소프트웨어 레벨에서의 오작동 가능성을 크게 줄였습니다.

2. Watchdog: “재부팅이 아니라 죽여라”

일반적인 소프트웨어 와치독(Watchdog)은 시스템이 멈추면 재부팅(Reset) 을 시킵니다. “껐다 켜면 해결된다”는 만고의 진리죠. 하지만 이 프로젝트는 다릅니다.

“Automatically restarting a radio transmitter in an unmanned tunnel is dangerous.” (무인 터널에서 라디오 송신기를 자동 재시작하는 건 위험하다.)

이 문구에 전적으로 동의합니다. 비상 상황이 아닌데 시스템 오류로 인해 좀비처럼 되살아나서 엉뚱한 방송을 내보내는 것보다는, 차라리 침묵(Silence) 하는 게 안전합니다.

이 시스템의 FPGA 와치독은 GUI로부터 5초간 하트비트가 없으면 RF 출력을 하드웨어 레벨에서 차단(Kill)하고 래치(Latch)를 걸어버립니다. 운영자가 직접 개입해서 리셋하기 전까지는 절대 다시 켜지지 않습니다. 이는 Fail-Recover 가 아닌 Fail-Safe 설계의 정석을 보여줍니다.

3. 정형 검증(Formal Verification): 테스트 코드는 버그의 존재만 증명한다

이 글을 쓰게 된 결정적인 이유입니다. 보통 FPGA 로직을 짤 때 Testbench를 돌리며 “이 정도면 되겠지”라고 넘어가는 경우가 많습니다. 하지만 이 프로젝트는 SymbiYosys 와 Z3 SMT Solver 를 사용해 와치독 타이머의 14가지 속성을 수학적으로 증명했습니다.

• Bounded Model Checking (BMC): 특정 사이클 내에서 오류가 없는지 확인
• K-Induction: 모든 시간, 모든 상태에서 불변(Invariant) 조건이 깨지지 않음을 증명

예를 들어, “카운터가 타임아웃에 도달하면 반드시 트리거가 발생한다(Liveness)“라거나, “경고 신호 없이는 절대 트리거되지 않는다(Safety)” 같은 속성들을 증명했습니다. 시뮬레이션 기반 테스트가 ‘내가 생각한 시나리오’만 커버한다면, 정형 검증은 ‘내가 미처 생각하지 못한 엣지 케이스’까지 수학적으로 커버합니다.

wd.sby 설정 파일을 보면 CLK_FREQ=1로 축소해서 검증을 수행했는데, 이는 상태 공간(State Space)을 줄여 솔버가 해를 빨리 찾게 하기 위함입니다. 로직이 파라미터화(Parameterized) 되어 있다면, 축소된 모델에서의 증명이 실제 스케일에서의 무결성을 강력하게 시사하기 때문에 아주 영리한 접근입니다.

4. 아쉬운 점: FPGA 리소스의 한계

물론 완벽한 프로젝트는 없습니다. 가장 눈에 띄는 병목은 오디오 버퍼 입니다.

Red Pitaya(Zynq 7010)의 BRAM(Block RAM) 용량 한계로 인해 오디오 샘플을 16,384개밖에 저장하지 못합니다. 이로 인해 오디오 샘플링 레이트를 5kHz로 다운샘플링해야 했습니다.

• 5kHz 샘플링: 사람 목소리를 알아들을 수는 있지만, ‘고품질’과는 거리가 멉니다. (전화기 음질보다 낮음)
• 해결책: FPGA 내 BRAM 대신, Zynq의 DDR 메모리를 활용하고 AXI DMA(Direct Memory Access)를 통해 오디오를 스트리밍했다면 훨씬 긴 고음질 방송이 가능했을 겁니다. 현재는 Python 스크립트가 AXI를 통해 오디오를 계속 밀어넣는 방식이라 약간의 딜레이(Gap)가 발생합니다.

또한, Python SCPI 서버(am_scpi_server.py)가 /dev/mem을 통해 레지스터에 직접 접근하는 방식은 프로토타이핑에는 좋지만, 상용 제품이라면 전용 커널 드라이버나 UIO(Userspace I/O)를 사용하는 것이 더 견고했을 것입니다.

5. 결론: “기본기가 탄탄한 모범 사례”

이 프로젝트는 단순히 “FPGA로 라디오 만들기”가 아닙니다. 현대적인 소프트웨어 공학(Rust, MVC) 과 엄격한 하드웨어 검증(Formal Verification) 이 어떻게 결합될 수 있는지를 보여주는 훌륭한 사례입니다.

특히 주니어 엔지니어들이라면 “기능 구현”에만 집중하기 쉬운데, 이 프로젝트처럼 “실패 시나리오(Failure Mode)” 를 먼저 고민하고, 그것을 시스템적으로(와치독, 정형 검증) 방어하는 설계를 눈여겨봐야 합니다.

만약 여러분이 터널에 갇혔을 때 라디오에서 비상 방송이 나온다면, 그 뒤에는 이런 치열한 엔지니어링적 고민이 숨어있을지도 모릅니다.

참고 자료:

• GitHub Repository: Park07/amradio
• Hacker News Discussion