FormalRTL: Verified RTL Synthesis at Scale

이 논문은 애매한 명세와 형식적 정확성 보장의 부재로 인해 산업 규모 데이터 경로 설계에 적용하기 어려웠던 대규모 언어 모델을 활용하여, 소프트웨어 참조 모델을 형식 명세로 통합하고 계획·합성·형식 등가성 검증을 긴밀하게 결합한 'FormalRTL'이라는 다중 에이전트 프레임워크를 제안하여 확장 가능하고 신뢰할 수 있는 하드웨어 코드 생성을 실현함을 보여줍니다.

핵심

🏗️ 문제: "AI 건축가가 건물을 지으려는데..."

지금까지 AI 가 반도체 (칩) 를 설계할 때 겪던 문제는 두 가지였습니다.

1. 설계도가 너무 모호함: "거대한 빌딩을 지어줘"라고만 말하면, AI 는 "어떤 모양으로?" "몇 층으로?"를 알아맞히기 힘들어 엉뚱한 건물을 짓습니다. (자연어 설명의 한계)
2. 검증의 어려움: AI 가 지은 건물을 다 짓고 나서 "이거 안전할까?"라고 확인하려는데, 실제 사람이 직접 모든 구석구석을 걸어 다니며 (시뮬레이션) 확인하는 건 시간이 너무 오래 걸리고, 놓치는 구석 (버그) 이 생기기 쉽습니다.

💡 해결책: "FormalRTL" - 완벽한 청사진과 자동 검사관

이 논문은 **"소프트웨어 참조 모델 (C/C++ 코드)"**을 **완벽한 청사진 (Golden Specification)**으로 삼아 문제를 해결합니다.

1. 계획 단계: "현장 감독관" (Planning Agent)

• 비유: AI 가 처음부터 거대한 빌딩 전체를 한 번에 짓는 게 아니라, **C++ 로 된 완벽한 설계도 (참조 모델)**를 먼저 분석합니다.
• 작동 방식: 설계도를 보고 "1 층은 구조가 복잡하니까 A 팀이, 2 층은 B 팀이"라고 작업 부서를 나누고 순서를 정합니다. (정적 분석 및 위상적 순서)
• 효과: AI 가 혼란스러워하지 않고, 작은 블록 하나씩 차근차근 쌓아 올릴 수 있게 됩니다.

2. 시공 단계: "건축가" (Initializing Agent)

• 비유: 할당받은 팀 (AI) 이 작은 블록 (서브 모듈) 을 짓습니다.
• 작동 방식: 이때 AI 는 단순히 말로 된 지시사항만 보고 짓는 게 아니라, 앞서 분석한 C++ 설계도와 정확히 일치하게 코드를 작성합니다.

3. 검증 및 수정 단계: "자동 검사관" (Debugging Agent)

• 비유: 건물이 다 지어지면, **자동 검사관 (Formal Equivalence Checking)**이 나옵니다.
• 핵심 차이: 기존 방식은 "이건 맞다/틀리다"만 알려주지만, 이 시스템은 **"어디가 틀렸는지, 왜 틀렸는지" (Counterexample)**를 구체적으로 보여줍니다.
  • 예시: "3 층 201 호 창문이 설계도보다 1cm 작아요. 여기 수정해 주세요."
• 작동 방식: AI 는 이 구체적인 피드백을 보고 코드를 수정합니다. 이 과정이 자동으로 반복되어, 완벽하게 설계도와 일치하는 건물이 될 때까지 수정합니다.

---

🌟 이 시스템의 핵심 장점

1. 확실한 정확성 (Formal Guarantee):
   • 단순히 "대충 비슷해 보이네"가 아니라, 수학적으로 100% 정확함을 증명합니다. 마치 건물의 모든 철근이 설계도와 일치하는지 수학적으로 계산해 보는 것과 같습니다.
2. 대규모 프로젝트 가능 (Scalability):
   • 복잡한 산업용 칩 (수천 줄의 코드) 도 작은 블록으로 나누어 처리하므로, AI 가 감당하기 힘든 거대한 작업도 가능해졌습니다.
3. 실제 산업 현장 적용:
   • 단순한 실험실 수준의 장난감이 아니라, 실제 반도체 회사 (화웨이 등) 에서 사용하는 복잡한 데이터 처리 칩 (Hifloat8 등) 을 성공적으로 설계하고 검증했습니다.

📊 결과: 얼마나 잘 하나요?

• 첫 시도 성공률: AI 가 처음부터 완벽하게 짓는 경우는 드뭅니다 (약 15~90% 수준).
• 최종 성공률: 하지만 자동 검사관과 수정 과정을 거치면, 거의 모든 경우 (95~100%) 에 완벽한 건물을 완성했습니다.
• 기존 방식과의 비교: 설계도 (C++ 참조 모델) 없이 말로만 지시하는 기존 AI 방식은 건물이 커질수록 실패율이 급격히 올라갔지만, FormalRTL 은 건물이 커져도 안정적으로 작동했습니다.

🚀 결론

이 논문은 **"AI 가 반도체를 설계할 때, 단순히 말로 지시하는 대신 '완벽한 소프트웨어 설계도'를 참고하게 하고, '수학적 검사관'을 통해 실수를 바로잡게 함으로써, 산업 현장에서 쓸 수 있는 고품질 칩을 자동으로 만들 수 있다"**는 것을 증명했습니다.

이는 마치 AI 건축가가 설계도 없이 막연하게 건물을 짓는 것에서, 정밀한 CAD 도면과 자동 안전 검사 시스템을 갖춘 현대적인 건설 현장으로 진화한 것과 같습니다.

기술 요약

논문 제목: FormalRTL: Verified RTL Synthesis at Scale (FormalRTL: 대규모 검증된 RTL 합성)

1. 문제 정의 (Problem Statement)

최근 대규모 언어 모델 (LLM) 은 하드웨어 합성 자동화 가능성을 보여주었으나, 산업 수준의 데이터 패스 (datapath) 중심 설계에 적용하기에는 다음과 같은 근본적인 한계가 존재합니다.

• 명세의 모호성과 복잡성: 자연어 명세만으로는 복잡한 하드웨어의 구조적, 시간적, 산술적 요구사항을 정확하게 포착하기 어렵습니다. 이로 인해 LLM 이 아키텍처 결정을 내리거나 수천 줄의 RTL 코드를 생성할 때 오류가 빈번히 발생합니다.
• 검증의 불충분함: 기존 연구들은 주로 시뮬레이션 기반 검증 (테스트벤치) 에 의존합니다. 이는 엣지 케이스 (corner cases) 를 모두 커버하지 못하며, 기능적 정확성에 대한 **형식적 보장 (Formal Guarantee)**을 제공하지 못합니다.
• 산업적 격차: 기존 LLM 기반 접근법은 단순한 오픈소스 벤치마크 (예: 100 줄 미만의adder) 에서는 성과를 보였으나, 수천 줄의 코드가 필요한 산업용 IP 코어 설계에는 확장성이 부족했습니다.

2. 제안된 방법론 (Methodology: FormalRTL)

저자들은 FormalRTL이라는 새로운 엔드 - 투 - 엔드 멀티 에이전트 프레임워크를 제안합니다. 이 시스템은 자연어 명세 대신 **소프트웨어 참조 모델 (C/C++ 코드)**을 '실행 가능한 형식 명세 (executable formal specification)'로 활용하여 RTL 생성 및 검증을 안내합니다.

핵심 워크플로우 및 에이전트 구조:

1. 플래닝 에이전트 (Planning Agent):

   • C 참조 모델을 정적 분석 (Static Analysis, AST 기반) 하여 복잡한 설계를 모듈화된 하위 작업으로 분해합니다.
   • 함수 의존성 (Dependency) 을 기반으로 위상적 순서 (Topological Order) 를 결정하여, 하위 모듈부터 상위로 점진적으로 합성합니다.
   • 이는 자연어 명세만 기반한 계획보다 훨씬 신뢰할 수 있는 아키텍처 분할을 가능하게 합니다.

2. 초기화 에이전트 (Initializing Agent):

   • 각 하위 모듈에 대해 C 참조 모델과 명세를 기반으로 초기 RTL 코드와 검증 하네스 (Verification Harness) 를 생성합니다.
   • 하네스는 C 모델과 RTL 모델의 입력을 동일하게 가정하고 출력 동등성을 주장 (Assert) 하는 환경을 구성합니다.
   • 순차 논리 (Sequential Logic) 의 경우, 하드웨어가 최종 결과를 산출하는 데 필요한 클록 사이클 수를 명시하여 트랜잭션 동등성 검증을 가능하게 합니다.

3. 디버깅 에이전트 (Debugging Agent):

   • 형식 동등성 검사 (Formal Equivalence Checking, EC) 도구 (hw-cbmc 등) 를 사용하여 소프트웨어 (C) 와 하드웨어 (RTL) 간의 동등성을 검증합니다.
   • 구문 오류 (Syntax Error): 버그 로케이터 (Bug Locator) 를 통해 오류 위치를 식별하고 주변 코드를 추출하여 LLM 에게 전달합니다.
   • 반례 (Counterexample): EC 도구가 생성한 반례를 CE Simplifier 를 통해 간소화하여, 어떤 신호에서 불일치가 발생했는지 명확히 보여줍니다.
   • LLM 은 이 피드백을 바탕으로 패치를 생성하고 코드를 수정합니다. 이 과정은 수동 테스트벤치 작성의 노고를 대체하며 높은 커버리지를 보장합니다.

3. 주요 기여 (Key Contributions)

• 소프트웨어 참조 모델 기반 방법론: 자연어 명세 대신 C/C++ 참조 모델을 '골든 스펙'으로 활용하여 확장성과 정확성을 동시에 확보하는 새로운 하드웨어 개발 패러다임을 제시했습니다.
• 엔드 - 투 - 엔드 멀티 에이전트 엔진: 계획 (Planning), 합성 (Synthesis), 디버깅 (Debugging), 형식 검증 (Formal Verification) 을 자동화하는 통합 파이프라인을 구축했습니다.
• 산업 등급 벤치마크 구축: 학술적 (Berkeley softfloat 기반) 과 산업적 (Huawei Ascend AI 칩의 Hifloat8 기반) 시나리오를 포함한 새로운 벤치마크 스위트와 C 참조 모델을 오픈소스로 공개했습니다.

4. 실험 결과 (Results)

저자들은 16 비트 부동소수점 연산자 (FP16) 와 8 비트 Hifloat8 연산자 등 1,000 줄 이상의 RTL 코드가 필요한 복잡한 모듈들을 대상으로 실험을 수행했습니다.

• 성공률 (Success Rate):
  • 초기 성공률 (ISR): 첫 시도에서의 통과율은 모듈에 따라 낮았으나 (일부 15%30%), 디버깅 에이전트를 거친 후 **최종 성공률 (FSR) 은 대부분의 모듈에서 95100%**에 달했습니다.
  • 순차 논리 처리: 복잡한 순차 논리를 포함한 설계에서도 높은 FSR 을 달성하여 시스템의 견고성을 입증했습니다.
• 비교 분석 (Ablation Study):
  • 플래닝 방법 비교: C 참조 모델을 정적 분석하여 분할하는 방식 (FormalRTL) 은 단순 명세 기반의 모놀리식 (Monolithic) 생성 방식보다 훨씬 높은 성공률과 적은 반복 횟수를 보였습니다. 설계가 복잡해질수록 (1,000 줄 이상) 기존 방식은 실패율이 급증했으나, FormalRTL 은 안정적으로 성공했습니다.
  • 디버깅 도구 분석: 버그 로케이터와 반례 간소화 도구를 제거할 경우, 수정 반복 횟수가 크게 증가하고 성공률이 하락했습니다. 특히 '반례 기반 디버깅'이 성능에 가장 중요한 요소임을 확인했습니다.
• 품질 (QoR):
  • 생성된 RTL 은 수동 설계에 비해 면적 (Area) 과 지연 (Delay) 이 다소 크지만, 이는 기능적 정확성 (Correctness) 을 최우선으로 한 결과입니다. 검증된 베이스라인은 엔지니어가 PPA(성능, 전력, 면적) 최적화를 수행하는 데 안정적인 토대를 제공합니다.

5. 의의 및 결론 (Significance)

• 산업적 적용 가능성: 이 연구는 LLM 기반 하드웨어 합성이 단순한 프로토타이핑을 넘어, 산업 수준의 복잡한 데이터 패스 설계에 적용될 수 있음을 증명했습니다.
• 형식적 검증의 통합: 자연어에서 RTL 로의 직접 변환의 불확실성을 제거하고, 소프트웨어 참조 모델과 형식 검증을 통해 수학적 증명 수준의 정확성을 보장합니다.
• 미래 지향성: 오픈소스 형식 검증 도구의 부재와 같은 한계점을 지적하며, 향후 C-RTL 동등성 검사 도구의 발전과 특화된 디버깅 LLM 모델의 필요성을 제기했습니다.

요약하자면, FormalRTL 은 LLM 의 생성 능력을 산업적 신뢰성 (Reliability) 과 결합하여, 소프트웨어 참조 모델을 '진리 (Ground Truth)'로 삼아 자동화된 검증 가능한 하드웨어 설계를 실현한 획기적인 접근법입니다.