💻 computer science

From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation

이 논문은 자연어 명세로부터 SystemVerilog Assertion(SVA)을 자동 생성하기 위해, 설계 컨텍스트를 수집하는 RAG 단계와 JasperGold의 피드백을 통해 오류를 수정하는 검증 루프를 결합한 도구 보조형 ReAct 에이전트인 'ProofLoop'를 제안합니다.

원저자: Nowfel Mashnoor, Hadi Kamali, Kimia Azar

게시일 2026-04-28

📖 2 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Nowfel Mashnoor, Hadi Kamali, Kimia Azar

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

🏗️ 배경: "설계도는 있는데, 검사 규칙을 누가 만들지?"

우리가 아주 복잡한 레고 성(반도체 설계도, RTL)을 만든다고 상상해 보세요. 성이 튼튼한지 확인하려면 규칙이 필요합니다.

"성문이 열리면 반드시 경비병이 서 있어야 한다."
"다리가 내려가면 반드시 성벽이 닫혀 있어야 한다."

이런 규칙을 전문 용어로 **SVA(SystemVerilog Assertions)**라고 부릅니다. 문제는 이 규칙을 쓰는 게 너무 어렵다는 거예요. 마치 아주 까다로운 법률 문장을 쓰는 것과 같아서, 전문가가 아니면 실수하기 쉽고 시간도 엄청 오래 걸립니다.

🤖 기존의 문제: "똑똑하지만 눈치 없는 인공지능"

최근에는 ChatGPT 같은 인공지능(LLM)에게 "이 설계도에 맞는 검사 규칙 좀 써줘"라고 시키기도 했습니다. 하지만 기존 AI는 치명적인 약점이 있었습니다.

마치 **"설계도를 글로만 읽은 초보 인턴"**과 같았거든요.
설계도에 적힌 글자만 보고 규칙을 만들다 보니, "어? 여기 'A'라는 스위치가 있네?" 하고 규칙을 만들었는데, 알고 보니 실제 설계도에서는 이름이 'B'였거나, 그 스위치가 작동하는 타이밍이 완전히 다른 경우였습니다. 즉, '글자'는 읽지만 '실제 구조'를 이해하지 못했던 거죠.

✨ 해결책: "ProofLoop — 눈과 손을 가진 베테랑 검사관"

연구진은 이 문제를 해결하기 위해 **'ProofLoop'**라는 새로운 시스템을 만들었습니다. 이 시스템은 단순히 글만 읽는 게 아니라, 직접 설계도를 뒤져보고(눈), 검사 도구로 확인하며(손), 틀리면 다시 고치는(뇌) 과정을 거칩니다.

이 과정을 세 단계로 비유해 볼게요.

1단계: 도서관 검색 (Context Gathering)

AI에게 그냥 "해봐"라고 던져주는 게 아니라, AI에게 **'설계도 전문 도서관'**을 통째로 빌려줍니다. AI는 궁금한 게 생기면 도서관에서 관련 정보를 직접 찾아봅니다.

"잠깐, 이 스위치는 어떤 전선에 연결되어 있지? 도서관(데이터베이스)에서 찾아보자!"

2단계: 현장 조사 (Structural Analysis)

단순히 글자만 보는 게 아니라, **'현미경(JasperGold라는 전문 도구)'**을 사용합니다.

"글로는 '스위치'라고 되어 있는데, 현미경으로 보니 이 스위치는 0.001초마다 신호가 바뀌는 아주 예민한 녀석이군! 규칙을 더 정교하게 써야겠어."

3단계: 무한 피드백 루프 (Solver-in-the-Loop)

AI가 규칙을 하나 만들면, 바로 **'엄격한 채점관(Formal Tool)'**에게 가져갑니다.

채점관: "틀렸어! 문법이 이상해!" 혹은 "이 규칙은 실제 상황에서 작동 안 해!"
AI: "아, 죄송합니다. 다시 고쳐올게요!" (이 과정을 최대 3번까지 반복하며 완벽해질 때까지 다듬습니다.)

📊 결과: "압도적인 실력 차이"

결과는 놀라웠습니다.

기존 방식: 규칙을 제대로 못 만들거나, 문법이 틀려서 엉터리인 경우가 많았습니다.
ProofLoop: 문법적으로 완벽할 확률이 93.7%, 실제로 설계의 의도대로 작동하는 규칙을 만들 확률이 **82.0%**까지 올라갔습니다.

특히, 설계도가 아주 크고 복잡해질수록(마치 거대한 성을 지을수록) 기존 AI는 길을 잃고 헤맸지만, ProofLoop는 도서관과 현미경을 활용해 끝까지 정확한 규칙을 찾아냈습니다.

💡 요약하자면?

이 논문은 **"말만 번지르르한 AI"**를 **"직접 설계도를 조사하고, 틀리면 고치고, 전문 도구까지 능숙하게 다루는 '현장형 베테랑 검사관'"**으로 업그레이드하는 방법을 제시한 것입니다. 덕분에 반도체를 만드는 과정이 훨씬 빠르고 정확해질 수 있게 되었습니다.

[기술 요약] ProofLoop: LLM과 정형 검증 도구를 결합한 RTL 어설션 자동 생성 프레임워크

1. 문제 정의 (Problem Statement)

디지털 하드웨어 검증에서 **SystemVerilog Assertions (SVA)**는 설계 의도를 정형적으로 검증하기 위한 핵심 요소입니다. 그러나 SVA를 작성하는 것은 다음과 같은 이유로 매우 어렵습니다:

전문 지식 요구: RTL(Register-Transfer Level) 구조와 시간 논리(Temporal Logic)에 대한 깊은 이해가 필요합니다.
LLM의 한계: 기존의 대규모 언어 모델(LLM)을 직접 사용하여 SVA를 생성할 경우, 신호 이름 오류, 잘못된 클록/리셋 가정, 설계의 구조적 메타데이터(FSM 상태 인코딩, 팬인/팬아웃 관계 등) 파악 불가로 인해 문법 및 기능적 오류가 빈번하게 발생합니다.
확장성 문제: 설계 규모가 커질수록(SoC 수준) 전체 RTL을 LLM의 컨텍스트 창에 담기 어려워 성능이 급격히 저하됩니다.

2. 제안 방법론 (Methodology: ProofLoop)

본 논문은 ProofLoop라는 도구 증강형 ReAct(Reasoning + Acting) 에이전트를 제안합니다. 이 시스템은 단순히 텍스트를 생성하는 것을 넘어, EDA 도구인 Cadence JasperGold를 루프 안에 포함시켜(Solver-in-the-loop) 스스로 판단하고 수정합니다.

A. AST 인덱싱 및 지식 베이스 구축

RTL을 파싱하여 **AST(Abstract Syntax Tree)**를 생성합니다.
이를 모듈 인터페이스, Always 블록, 인스턴스, 할당문(Assign) 등 4가지 의미론적 단위로 분할하여 **벡터 데이터베이스(Vector DB)**에 저장합니다. 이를 통해 필요한 부분만 효율적으로 검색(RAG)할 수 있습니다.

B. Phase A: 컨텍스트 수집 (Context Gathering)

에이전트는 '생각(Thought) $\rightarrow$ 행동(Action) $\rightarrow$ 관찰(Observation)' 루프를 통해 필요한 정보를 스스로 수집합니다.

검색 도구(Retrieval Tools): 벡터 DB를 통해 관련 설계 조각을 검색합니다.
구조 분석 도구(Structural Analysis Tools): JasperGold를 호출하여 RTL 텍스트만으로는 알 수 없는 신호의 의존성(Fan-in/out), 플립플롭의 클록/리셋 동작 등을 추출합니다.

C. Phase B: SVA 생성 및 검증 루프 (Generation & Verification Loop)

에이전트가 SVA를 생성하면 JasperGold를 통해 정형 검증을 수행합니다.
Solver-in-the-loop: 검증 결과(성공, 실패, 문법 오류, 반례/Counterexample)를 에이전트에게 피드백으로 전달합니다.
에이전트는 이 피드백을 바탕하여 처음부터 다시 쓰는 것이 아니라, 오류가 발생한 부분(신호 이름, 시간 연산자 등)을 **국소적으로 수정(Targeted Repair)**하며 최대 3회까지 반복합니다.

3. 주요 기여 (Key Contributions)

에이전트 기반 컨텍스트 합성: ReAct 방식을 도입하여 에이전트가 설계 구조를 스스로 탐색하도록 설계했습니다.
Solver-in-the-loop 정제: 정형 검증 도구의 피드백을 활용해 문법 및 기능적 오류를 반복적으로 수정하는 메커니즘을 구축했습니다.
확장 가능한 구조: AST 기반 RAG를 통해 대규모 다중 모듈 설계에서도 효율적으로 동작합니다.

4. 실험 결과 (Experimental Results)

FVEval의 Design2SVA 벤치마크를 통해 평가한 결과는 다음과 같습니다.

성능 지표 (Qwen3.5-35B 모델 기준):
- 문법 정확도(Syntax Correctness): 93.7% (Baseline 78.3% 대비 대폭 향상)
- 기능 정확도(Functional Correctness): 82.0% (Baseline 43.2% 대비 약 2배 향상)
설계 복잡도에 따른 강점: 설계 규모가 커질수록(Large designs) Baseline은 성능이 급락하는 반면, ProofLoop는 안정적인 성능을 유지했습니다.
어블레이션 연구(Ablation Study):
- 구조 분석 도구가 가장 큰 기여를 했으며, 그 다음으로 검증 루프(Verification Loop), RAG 순으로 성능 향상에 기여함을 확인했습니다.
검증 루프 효과: 문법 오류의 약 59.3%가 피드백을 통해 수정되었습니다.

5. 의의 및 결론 (Significance & Conclusion)

본 연구는 LLM이 가진 '구조적 이해의 부족'이라는 근본적인 한계를 정형 검증 도구와의 능동적인 상호작용을 통해 해결했습니다. 단순히 언어 모델의 추론 능력에 의존하는 것이 아니라, EDA 도구의 물리적/구조적 메타데이터를 에이전트의 사고 과정에 통합함으로써, 자연어 명세(Specification)를 신뢰할 수 있는 논리적 형식(SVA)으로 변환하는 강력한 프레임워크를 제시했다는 점에서 큰 의의가 있습니다.