Formal that "Floats" High: Formal Verification of Floating Point Arithmetic

이 논문은 비선형 연산과 제어/데이터 경로 결합으로 인해 어려운 부동소수점 연산의 형식 검증을 위해, 직접적인 RTL 대 RTL 모델 체킹과 분할 정복 전략, 그리고 인간-인-루프 (HITL) 가이드를 통한 AI 기반 속성 생성을 결합한 확장 가능한 검증 방법론을 제시합니다.

핵심

🏗️ 1. 문제: "소수점 계산"은 왜 위험할까요?

컴퓨터는 정수 (1, 2, 3) 는 잘 계산하지만, 소수점 (0.1, 0.2) 을 다룰 때는 아주 미세한 오차가 생기기 쉽습니다. 마치 저울을 사용할 때 아주 작은 모래알 하나만 놓쳐도 무게가 달라지는 것과 비슷해요.

기존에는 이렇게 복잡한 소수점 회로를 검증할 때, **"C 언어라는 번역기"**를 사용했습니다.

• 비유: 실제 건물 (하드웨어) 을 짓기 전에, C 언어라는 간이 설계도를 그려서 비교했습니다. 하지만 간이 설계도와 실제 건물 사이에는 '번역 오류'가 생길 수 있고, 실제 건물의 복잡한 구조를 다 담아내지 못해 숨은 결함을 놓칠 수 있었습니다.

🚀 2. 해결책: "직접 비교"와 "조각조각 나누기"

이 논문은 두 가지 핵심 전략을 제안합니다.

A. 직접 비교 (RTL-to-RTL)

• 비유: 간이 설계도 (C 언어) 를 거치지 않고, 실제 건축 현장 (RTL) 과 완벽한 설계도 (Golden Model) 를 직접 비교합니다.
• 효과: 번역 과정에서 생기는 오해를 없애고, 실제 회로가 설계대로 작동하는지 100% 정확하게 맞춥니다.

B. 조각조각 나누기 (Divide-and-Conquer)

• 비유: 거대한 퍼즐을 한 번에 맞추려다 지치기 쉽죠? 대신 퍼즐을 '상단', '중단', '하단'으로 나누어 하나씩 맞춥니다.
• 방법: 소수점 덧셈기를 '정렬 단계'와 '덧셈/반올림 단계'로 나누어, 각 단계가 올바르게 작동하는지 따로따로 증명합니다. 한 단계에서 실수가 나면 그 부분만 고치면 되니 훨씬 빠르고 정확합니다.

🤖 3. 혁신: "AI 비서"와 "인간 감독관"의 팀워크

가장 흥미로운 부분은 **인공지능 (LLM)**을 활용했다는 점입니다.

• 상황: 회로가 올바르게 작동하는지 확인하려면 수많은 '규칙 (속성)'을 직접 써야 합니다. 이는 마치 수천 개의 안전 수칙을 일일이 손으로 적는 일과 같아 매우 힘들고 시간이 걸립니다.
• 해결: 연구진은 **AI 비서 (GPT-5, Llama 등)**에게 "이 회로의 안전 수칙을 써줘"라고 요청했습니다.
  • 초기 결과: AI 가 쓴 규칙은 많았지만, 중복되거나 헷갈리는 내용이 섞여 있었습니다. (비유: AI 가 100 개의 규칙을 썼는데, 그중 90 개는 같은 내용이라 비효율적이었습니다.)
  • HITL (Human-in-the-Loop): 여기서 인간 감독관이 개입했습니다. AI 가 쓴 규칙을 검토하고, 불필요한 것은 지우고, 중요한 것은 수정했습니다.
  • 결과: AI 가 쓴 규칙을 인간이 다듬자, 손으로 쓴 규칙만큼 정확해지면서도 훨씬 적은 수의 규칙으로 모든 것을 검증할 수 있게 되었습니다.

🧪 4. 검증: "고의적인 실수" 테스트

이 방법이 정말 강력한지 확인하기 위해, 연구진은 의도적으로 회로에 결함을 심었습니다.

• 비유: 마치 안전 점검관이 건물에 일부러 약한 벽을 만들어보고, 우리의 검증 시스템이 그 약점을 찾아낼 수 있는지 테스트한 것입니다.
• 결과: AI 가 만든 규칙과 인간이 다듬은 규칙을 합치면, 의도적으로 심은 모든 미세한 결함 (소수점 오차 등) 을 찾아냈습니다.

📊 5. 결론: 왜 이 방법이 중요한가요?

• 기존 방식: C 언어 번역기를 거치거나, 규칙을 손으로 모두 써야 해서 느리고 오류가 생기기 쉬움.
• 이 논문의 방식:
  1. 직접 비교: 실제 회로와 설계도를 바로 맞춥니다.
  2. AI + 인간: AI 가 초안을 빠르게 만들고, 인간이 핵심만 다듬어 효율성을 극대화합니다.
  3. 결과: 더 적은 노력으로, 더 높은 정확도를 달성했습니다.

💡 한 줄 요약

"이 논문은 인공지능이 초안을 만들고 인간이 다듬는 방식으로, 컴퓨터의 소수점 계산이 완벽하게 정확하도록 검증하는 새롭고 효율적인 방법을 제시했습니다."

이 방법은 앞으로 더 복잡한 반도체 설계에서도 시간과 비용을 아끼면서 안전성을 보장하는 핵심 기술이 될 것으로 기대됩니다.

기술 요약

논문 개요

이 논문은 부동소수점 산술 회로 (Floating-Point Units, FPUs) 의 형식적 검증 (Formal Verification) 을 위한 확장 가능한 방법론을 제안합니다. 기존 방식이 고수준 C 모델을 참조 모델로 사용하여 RTL(레지스터 전송 수준) 설계와 비교하는 과정에서 발생하는 추상화 격차와 확장성 문제를 해결하기 위해, 직접적인 RTL-to-RTL 모델 체킹 방식을 도입하고 이를 에이전트 기반 AI를 활용한 자동화된 속성 생성과 결합했습니다.

1. 문제 제기 (Problem)

• 부동소수점 검증의 난이도: 부동소수점 연산은 지수 정렬, 정규화, 반올림 등 복잡한 제어 로직과 산술 데이터 경로가 긴밀하게 결합되어 있으며, IEEE-754 표준 준수가 필수적입니다. 이로 인해 비선형 산술 행동과 엣지 케이스 (비정규화, 오버플로우 등) 로 인해 형식적 검증이 매우 어렵습니다.
• 기존 방식의 한계: 기존의 많은 접근법은 고수준 C 모델을 '골든 레퍼런스 (Golden Reference)'로 사용하여 RTL 과 동등성을 검증합니다. 그러나 이는 C 와 하드웨어 실행 간의 의미론적 불일치 (Semantic Mismatch), 번역 오버헤드, 그리고 RTL 수준의 확장성 저하를 초래합니다. 특히 데이터 경로가 복잡한 설계에서는 C 모델 유지보수 비용이 크고 정확도가 떨어질 수 있습니다.

2. 제안된 방법론 (Methodology)

이 논문은 고수준 추상화 모델 없이 RTL 구현체와 RTL 참조 모델 간의 직접적인 비교를 핵심으로 하는 방법론을 제시합니다.

• 직접 RTL-to-RTL 모델 체킹:
  • 고수준 C 모델 대신 SystemVerilog 로 작성된 정밀한 비트 단위 IEEE-754 준수 참조 모델을 사용합니다.
  • 구현체 (Implementation) 와 참조 모델 (Specification) 을 동일한 수준에서 비교하여 추상화 격차를 제거합니다.
• 계층적 분해 전략 (Divide-and-Conquer):
  • 복잡한 부동소수점 더하기 회로를 **만티사 정렬 단계 (Mantissa Alignment Stage)**와 **덧셈 - 반올림 단계 (Add-Round Stage)**로 분해합니다.
  • 전체 증명을 하나의 정론 (Theorem) 으로 수행하는 대신, 각 단계를 검증하는 보조 정리 (Lemmas) 와 어설션 (Assertions) 을 통해 검증 복잡도를 낮추고 수렴성을 높입니다.
• CEX(Counterexample) 기반 반복 정제:
  • 형식적 도구가 생성한 반례 (CEX) 를 분석하여 구현체의 결함을 국소화하고, 어설션 또는 구현을 수정하는 반복적인 정제 과정을 거칩니다.
• 에이전트 기반 AI 속성 생성 (Agentic AI):
  • 자연어 명세와 RTL 코드를 입력받아 SystemVerilog Assertions (SVAs) 를 생성하는 다중 에이전트 시스템 (MAS) 을 도입했습니다.
  • 플래닝 (Planning), 생성 (Generation), 실행 (Execution) 단계를 거치며, LLM(대형 언어 모델) 이 속성을 생성하고, 크리틱 (Critic) 에이전트가 논리적 오류를 검토하며, 에러 수정 에이전트가 문제를 해결합니다.
  • HITL(Human-in-the-Loop): AI 생성 속성이 수렴하지 않거나 설계 의도와 다를 경우, 인간 전문가의 피드백을 통해 설계 의도를 명확히 하고 속성을 정제합니다.

3. 주요 기여 (Key Contributions)

1. 고수준 모델 불필요한 직접 RTL 검증: C 모델 의존성을 제거하고 순수 RTL-to-RTL 비교를 통해 정확도와 확장성을 확보했습니다.
2. 계층적 분해 및 증명: 부동소수점 연산을 모듈화된 단계로 나누어 검증함으로써 복잡한 데이터 경로의 형식적 증명을 가능하게 했습니다.
3. AI 기반 자동화 및 인간 피드백 결합: LLM 을 활용한 속성 생성과 HITL 정제를 결합하여, 수동 작성 속성과 유사한 품질을 자동화 수준으로 달성했습니다.
4. 고장 주입 (Fault Injection) 및 견고성 검증: 의도적으로 결함을 주입하여 형식적 속성이 정밀한 데이터 경로 오류를 얼마나 잘 탐지하는지 검증했습니다.

4. 실험 결과 (Results)

부동소수점 더하기 회로를 대상으로 Cadence Jasper Formal 플랫폼을 사용하여 실험을 수행했습니다.

• 결함 탐지 및 수정: 초기 검증 과정에서 구현체의 잘못된 피연산자 선택 로직과 부호 반전 오류 등을 발견하여 수정하고, 최종적으로 모든 속성이 증명되었습니다.
• 고장 주입 테스트: 만티사 정렬 및 덧셈 - 반올림 단계에 8 가지의 다양한 결함 (스티키 비트 왜곡, 정규화 오류 등) 을 주입한 결과, 제안된 형식적 속성들이 모든 결함을 성공적으로 탐지했습니다.
• 커버리지 및 효율성 비교:
  • RTL-to-RTL vs. Standalone: 참조 모델이 있는 RTL-to-RTL 검증이 참조 모델이 없는 단독 RTL 검증보다 훨씬 높은 커버리지 효율을 보였습니다.
  • Handwritten vs. AI Generated:
    • 수동 작성 (Handwritten) 속성: 2 개의 속성으로 98.42% 커버리지를 달성 (증명 시간 0.073 초).
    • AI 생성 (LLM) 속성 (HITL 전): 7~15 개의 속성이 필요했으나 중복이 많았고 증명 시간이 길었습니다.
    • AI 생성 속성 (HITL 후): 인간 전문가의 정제를 거친 후, 3~6 개의 간결한 속성으로 수동 작성과 유사한 커버리지 (98% 이상) 를 달성했습니다. 특히 GPT-5 는 3 개의 속성으로 1.318 초 만에 높은 효율을 보였습니다.
  • 참조 모델 부재 시: 참조 모델 없이 단독으로 검증할 경우, LLM 이 생성한 속성들은 설계 제약 조건을 제대로 파악하지 못해 커버리지가 급격히 떨어지고 도달 불가능한 (Unreachable) 항목이 증가했습니다. 이는 미세 아키텍처에 대한 전문 지식이 필요함을 시사합니다.

5. 의의 및 결론 (Significance)

• 확장 가능한 검증 프레임워크: 이 연구는 복잡한 부동소수점 연산기에 대한 형식적 검증을 고수준 추상화 모델 없이도 정밀하게 수행할 수 있는 확장 가능한 프레임워크를 제시했습니다.
• AI 와 인간의 협업 최적화: AI 가 속성 생성의 초기 단계를 담당하고, 인간 전문가가 설계 의도와 미세 아키텍처를 반영하여 정제하는 'HITL' 방식이 검증의 정확성과 효율성을 극대화함을 입증했습니다.
• 미래 방향: 현재는 부동소수점 더하기 회로에 국한되었으나, 이 방법론은 곱셈기, 나눗셈기 등 더 복잡한 FPUs 로 확장 가능하며, 향후 LLM 이 미세 아키텍처 의도를 더 잘 추출할 수 있다면 인간의 개입을 줄이고 완전 자동화된 형식적 검증이 가능해질 것으로 기대됩니다.

요약하자면, 이 논문은 RTL-to-RTL 직접 검증과 AI 기반 자동화를 결합하여 부동소수점 하드웨어 검증의 정확성과 효율성을 동시에 높인 선구적인 연구입니다.