언어에서 논리로: LLM 및 형식적 표현을 통한 RTL 명제 생성 연결

요약

본 논문은 자연어 명세를 기반으로 SystemVerilog Assertions(SVA)를 자동으로 생성하는 ProofLoop라는 새로운 에이전트를 소개합니다. ProofLoop는 검색 증강 생성(RAG), EDA 도구 호출, 그리고 형식 검증 피드백을 반복적으로 활용하는 '솔버-인-더-루프' 접근 방식을 사용합니다. 이 프레임워크는 설계 컨텍스트를 자율적으로 수집하고, 최대 3회의 검증 라운드를 통해 SVA를 생성 및 개선함으로써 높은 문법적/기능적 정확도를 달성함을 입증했습니다.

핵심 포인트

• SVA 작성의 어려움(전문 지식 필요)을 해결하기 위해 LLM 기반 자동화 접근 방식을 제시함.
• ProofLoop는 RAG, EDA 도구 호출(JasperGold), 그리고 형식 증명 피드백을 통합한 '솔버-인-더-루프' 아키텍처를 사용합니다.
• 에이전트는 설계 컨텍스트 수집과 SVA 생성/개선 과정을 반복적으로 수행하여 정확도를 높입니다.
• 벤치마크 평가 결과, ProofLoop는 93.7%의 문법적 및 82.0%의 기능적 정확도를 달성했습니다.