Knowledge Graphs, the Missing Link in Agentic AI-based Formal Verification

기술 요약: 에이전트 기반 형식 검증을 위한 지식 그래프, 결여된 연결고리

문제 제기
대형 언어 모델 (LLM) 이 자연어 명세에서 시스템버릴로그 어설션 (SVA) 을 생성하여 형식 검증 (FV) 을 가속화할 잠재력을 보였음에도 불구하고, 상당한 장애물이 남아 있습니다. 주요 과제는 '그라운딩 (grounding)' 문제입니다. 명세는 종종 모호하거나 불완전한 반면, 중요한 마이크로아키텍처 세부 사항은 레지스터 전송 수준 (RTL) 코드에 존재합니다. 기존 접근법은 명세와 RTL 을 느슨하게 구조화된 텍스트로 취급하여 명세 대 RTL 그라운딩이 약해집니다. 이로 인해 의미적 불일치가 발생하고, 형식 파싱 중 빈번한 구문 오류가 발생하며, 어설션은 광범위한 반복 수정과 수동 분류가 필요합니다. 또한, 이전 방법들은 형식 도구 피드백 (예: 반례 또는 CEX 및 커버리지 리포트) 을 생성 루프에 지속적으로 통합하지 못해 체계적인 정제에 한계가 있었습니다.

방법론
저자들은 의도와 구현 간의 간극을 메우기 위해 구조화된 중간 표현 (IR) 에서 지식 그래프 (KG) 를 구축하는 검증 중심의 방법론을 제안합니다. 워크플로는 입력, 타입 지정 JSON IR, 런타임 KG, 에이전트 오케스트레이션의 네 가지 레이어로 구성됩니다.

1. 중간 표현 (IR): 시스템은 데이터를 추출하여 정규화하여 타입 지정 JSON 아티팩트로 생성합니다. 여기에는 spec_chunks.json(계층적 명세), requirements.json, design_model.json(계층 구조 및 신호와 같은 RTL 메타데이터), properties.json, 그리고 검증 결과 (formal_results.json, cex_cases.json, coverage_metrics.json) 가 포함됩니다.
2. 지식 그래프 구축: 이러한 IR 은 노드와 엣지로 내보내져 NetworkX 를 사용하여 런타임 KG 를 구축합니다. KG 는 아티팩트 레지스트리 역할을 하여 요구 사항, 설계 계층 구조, 신호, 가정 및 속성을 연결합니다. 이는 제한된 컨텍스트 검색을 가능하게 합니다. 예를 들어, 속성을 생성할 때 KG 는 특정 요구 사항, 해당 상위 명세 조각, 관련 RTL 신호 및 규칙 책을 제공합니다.
3. 멀티 에이전트 오케스트레이션: 검증 프로세스는 KG 를 쿼리하고 업데이트하는 전문 에이전트들로 분해됩니다.
   • 속성 생성: 리드 에이전트가 spec_analyst(요구 사항 분해), sva_author(SVA 구문 합성), sva_reviewer(준수성 검증), sva_patcher(피드백 기반 수정) 를 조정합니다.
   • 구문 수정: 전용 루프가 컴파일 오류를 처리합니다. 에이전트는 진단을 분석하여 일반적인 패턴 (예: 선언되지 않은 식별자) 에 대해 결정론적 수정을 적용하고, RTL 선언 및 요구 사항 텍스트와 같은 복잡한 컨텍스트를 사용하여 더 어려운 오류를 처리합니다. 속성은 최대 세 번의 수정 시도가 허용됩니다.
   • CEX 수정: 속성이 실패할 때 에이전트는 VCD 파형 및 실패 추적을 파싱합니다. spec_assertion_analyzer 는 루트 원인 (예: RTL 버그 대 과소 명세) 을 분류하고, cex_fixer 는 제약 조건을 조정하거나 어설션을 강화합니다.
   • 커버리지 개선: 에이전트는 커버리지 지표를 분석하여 도달 불가능한 코드나 공허한 속성을 식별하고, 격차를 메우기 위한 표적 속성을 생성합니다.

주요 기여
이 논문은 세 가지 주요 기여를 주장합니다.

1. 검증 중심 KG 구축: 명세 의도, RTL 구조, 생성된 속성 및 형식 도구 결과를 단일 쿼리 가능한 아티팩트로 통합하는 구조화된 IR 에서 KG 를 구축하는 새로운 접근법.
2. 추적 가능성 있는 멀티 에이전트 워크플로우: 에이전트가 KG 기반 컨텍스트를 사용하여 SV A 를 생성하고 정제하며, 요구 사항에서 설계 요소, 속성 및 검증 결과까지 명시적인 추적 링크를 유지하는 시스템.
3. 실증적 평가: KG 기반 컨텍스트가 속성 생성 효과성, 구문 유효성 및 CEX 정제 루프의 효율성에 미치는 영향을 정량화한 일곱 개의 오픈 소스 벤치마크 설계에 대한 평가.

결과
이 방법론은 GPT-5.2 모델과 Cadence JasperGold 를 사용하여 일곱 개의 설계 (FIFO, Lemming, ALU, CICD, BST, TTC Counter, CSR) 에서 평가되었습니다.

• 구문 및 컴파일: 이 접근법은 일관되게 컴파일 가능한 SV A 를 생성했으며 구문 수정 오버헤드는 낮았습니다. 특히 design_model IR 을 통한 신호 및 계층 구조의 결정론적 해결을 포함한 KG 기반 컨텍스트는 선언되지 않은 식별자와 같은 프론트엔드 문제를 크게 줄였습니다.
• 형식 커버리지: 벤치마크 전반에 걸쳐 엔드 투 엔드 형식 커버리지는 78.5% 에서 99.4% 사이였습니다.
• 정제 효율성: FIFO 및 CIC Decimator 와 같은 설계는 CEX 및 커버리지 루프 후 상당한 개선을 보였으며, 많은 초기 실패는 검색된 컨텍스트를 통해 수정 가능한 로컬 문제 (누락된 가드, 경계 조건) 로 인한 것임을 시사합니다.
• 한계: 수렴은 설계에 따라 달랐습니다. 이진 검색 트리 (BST) 와 같은 복잡한 설계나 전역 불변식 또는 깊은 시간적 추론이 필요한 설계 (예: Lemming, ALU) 는 자동 수정으로부터 제한된 개선을 보였습니다. 저자들은 현재 LLM 의 능력이 복잡한 시간적 및 산술적 추론에 어려움을 겪으며, 의미적 디버깅이 더 어려운 벤치마크의 주요 병목 현상이라고 지적합니다.

의의
이 논문은 제안된 KG 중심 접근법이 이전 연구의 치명적인 약점인 요구 사항, RTL 의미론 및 검증 결과 간의 구조화된 쿼리 가능한 링크 부재를 해결한다고 주장합니다. 형식 도구 피드백 (CEX, 커버리지 격차) 을 일시적인 출력이 아닌 영구적이고 쿼리 가능한 KG 콘텐츠로 취급함으로써 시스템은 폐쇄 루프 정제 프로세스를 가능하게 합니다. 저자들은 복잡한 추론에 대한 의미적 수정이 여전히 과제이지만, 이 프레임워크가 추적 가능하고 설계 기반인 속성 생성을 위한 견고한 기반을 제공한다고 결론지었습니다. LLM 의 능력이 발전함에 따라, 이 KG 가 제공하는 구조화된 컨텍스트와 추적을 더 잘 활용할 수 있게 되어 자동화된 형식 검증의 신뢰성이 더욱 향상될 것입니다.