기술 요약: VERI-SURE

1. 문제 정의

전자 설계 자동화(EDA) 분야의 레지스터 전송 레벨(RTL) 설계를 위한 대규모 언어 모델(LLM) 배포는 실리콘 등급의 정확성을 달리는 데 있어 상당한 장애물에 직면해 있다. LLM이 소프트웨어 코드 생성에서는 진보를 이루었으나, RTL 생성은 하드웨어의 병렬적 특성, 엄격한 사이클 단위 타이밍, 그리고 프로토콜 의미론(semantics)으로 인해 독특한 과제를 안고 있다. 본 논문은 현재의 LLM 기반 RTL 파이프라인에서 세 가지 주요 병목 현상을 식별한다:

1. 평가 신뢰성 제한: 시뮬레이션 중심의 평가는 테스트 커버리지가 불충분하여 미묘한 시간적 코너 케이스(temporal corner cases)를 포착하지 못하는 경우가 많다.
2. 디버깅 비효 efficiency: 반복적인 디버깅은 전체 파일 재생성으로 인한 "회귀 및 수정 환각(regressions and repair hallucinations)"을 초래하여, 관련 없는 로직까지 불안정하게 만든다.
3. 의미론적 드리프트(Semantic Drift): 자연어 의도가 여러 에이전트 간의 핸드오프나 반복 과정에서 재해석됨에 따라, 원래의 설계 의도가 저하되어 일관성 없는 구현으로 이어질 수 있다.

VerilogEval-v2와 같은 기존 벤치마크는 고급 산술 유닛, 통신 프로토콜, 클록 도메인 교차(CDC) 패턴과 같은 산업계의 요구사항을 충분히 대변하지 못하는 짧고 교육적인 모듈 위주라는 비판을 받는다.

2. 방법론: VERI-SURE 프레임워크

VERI-SURE는 코드 합성, 검증, 그리고 국소적 수정을 위한 루프를 닫기 위해 설계된 계약 인식형(contract-aware) 멀티 에이전트 프레임워크이다. 이는 단발성 번역을 넘어 자동화된 생성-검증-디버그 사이클로 나아간다.

핵심 구성 요소

• 설계 계약 (Architect 에이전트): 프레임워크는 자연어 사양을 구조화된 JSON 형식의 설계 계약으로 추출하는 것으로 시작한다. 이 계약은 인터페이스 의미론, 클록/리셋 컨벤션, 사이클 정확한 동작, 코너 케이스를 명시적으로 정의한다. 이는 의미론적 드리프트를 방지하기 위해 모든 후속 에이전트가 공유하는 "진실의 원천(source of truth)" 역할을 한다.
• 멀티 에이전트 워크플로우:
  • Coder 에이전트: 계약을 기반으로 합성 가능한 RTL 코드를 생성한다.
  • Verifier 에이전트: 계약에 부합하는 셀프 체크 기능이 있는 테스트벤치를 생성한다.
  • Debugger 에이전트: 시뮬레이션 실패 시 자율적인 디버깅 루프를 주도한다.
  • Asserter 에이전트: 순차적 또는 프로토콜 위반(예: 잘못된 엣지 샘플링, 리셋 불일치)을 탐지하기 위한 타겟팅된 SystemVerilog 어설션을 생성한다.
  • Boolean Proofer 에이전트: 후보 수정 사항을 검증하고 회귀를 방지하기 위해 조합 논리에 대한 형식 검증(formal verification)을 수행한다.
• 핵-메커니즘 (Key Mechanisms):
  • 트레이스 기반 시간 분석 및 정적 슬라이싱: 시뮬레이션이 실패할 때, 시스템은 단순히 텍스트 로그에만 의존하지 않는다. 시스템은 가치 변화 덤프(VCD) 파형을 분석하여 최초의 발산 시간($t_f$)을 식별한다. 그 후 **정적 의존성 슬라이싱(static dependency slicing)**을 사용하여 실패하는 신호에 영향을 미치는 "로직의 원뿔(cone of logic)"을 계산한다. 이를 통해 실패 지점을 전체 파일이 아닌 최소한의 의심되는 코드 블록(라인 범위)으로 격리한다.
  • 국소적 패칭(Localized Patching): 슬라이싱 분석의 안내에 따라, Debugger 에이전트는 의심되는 블록에 대해서만 정밀한 블록 단위 편집(읽기/교체)을 적용한다. 이는 전체 파일 재작성의 불안정성을 피하기 위함이다. 롤백 규칙은 패치가 실패 시그니처를 개선하는 경우(예: 더 늦은 최초 실패 시간 또는 더 적은 불일치)에만 유지되도록 보장한다.
  • 멀티 브랜치 검증: 프레임워크는 두 가지 검증 브랜치를 통합한다:
    1. 트레이스 기반 시간 분석: 순차적 및 타이밍 이슈를 위한 것.
    2. 형식 검증: Assertion 기반 체크(Asserter를 통해)와 조합 제약 조건을 검증하고 유한 시뮬레이션을 넘어 정확성을 증명하기 위한 Boolean 등가 증명(SymbiYosys를 사용하는 Boolean Proofer를 통해)을 결합한다.

3. 벤치마크: VERILOGEVAL-V2-EXT

산업 수준의 RTL 생성을 더 잘 평가하기 위해, 저자들은 VERILOGEVAL-V2-EXT를 도입한다. 이 벤치마크는 기존 VerilogEval-v2를 확장하여 53개의 새로운 산업급 설계 태스크를 추가하였으며, 총 209개의 문제를 포함한다.

• 내용: 새로운 태스크는 UART, FIFO와 같은 통신 프로토콜, 고급 산술, DSP 커널, 다중 사이클 데이터패스 등 복잡한 도메인을 다룬다.
• 계층화: 문제는 구조적 신호(코드 라인 수, assign/always 블록 수, 데이터패스 너비)와 수동 검토를 기준으로 Easy, Medium, Hard 난이도로 분류된다. 이를 통해 더 세밀한 실패 모드 분석이 가능하다.

4. 실험 결과

저자들은 VERI-SURE를 15개의 독립형 LLM(상용 폐쇄형 및 오픈 웨이트 모델 포함), 단일 에이전트 피드백 루프, 그리고 이전의 멀티 에이전트 시스템(MAGE, VerilogCoder)과 비교 평가하였다.

• 성능: VERI-SURE는 VERILOGEVAL-V2-EXT 벤치마크에서 93.30%의 상태 최고(SOTA) functional Pass@1을 달성하였으며, 100%의 구문 성공률을 기록했다.
• Hard 태스크: 프레임워크는 "Hard" 태스크에서 가장 큰 강점을 보였으며, **85.07%**의 functional pass rate를 달성하여 최고의 단독 모델인 Gemini-3-Pro(62.69%)와 다른 에이전트 기반 베이스라인들을 크게 앞질렀다.
• 백본 불가지론(Backbone Agnosticism): VERI-SURE는 GPT-5.2에서 가장 높은 성능을 보였지만, 오픈 웨이트 모델인 DeepSeek-3.2의 성능도 61.24%(단독 모델)에서 71.29%로 크게 향상시켰다.
• 절제 연구 (Ablation Studies):
  • Tracing, Slicing, Patching 메커니즘을 제거했을 때 가장 큰 성능 저하(전체 11.0%, Hard 태스크 16.4%)가 발생하여, 정밀한 국소화가 결정적임을 확인했다.
  • Formal Verification을 제거하면 Hard 태스크의 pass rate가 11.9% 포인트 감소하여, 시뮬레이션이 놓치는 깊은 논리적 버그를 디버깅하는 데 필수적임을 입증했다.
  • Contract 메커니즘은 제거 시 전체 성능이 2.9% 하락하였으며, 이는 의도 일관성을 유지하는 데 있어 계약의 역할을 보여준다.

5. 의의 및 주장

본 논문은 VERI-SURE가 트레이스 기반 분석과 형식 검증을 결합한 하이브리드 접근 방식을 통해 시뮬레이션 중심의 평가에서 벗어남으로써, 자동화된 RTL 설계가 "실리콘 등급의 정확성"에 더 가까워질 수 있음을 입증한다고 주장한다.

주요 주장은 다음과 같다:

• 의미론적 드리프트 완화: 구조화된 설계 계약을 강제함으로써, 에이전트들의 의도를 정렬하고 요구사항의 점진적인 재해석을 방지한다.
• 수정의 안정성: 의존성 슬라이싱 기반의 패칭 메커니즘은 전체 파일 재생성과 관련된 회귀 위험 및 수정 환축을 효과적으로 줄인다.
• 시뮬레이션을 넘어서: 형식 증명의 통합은 순수 시뮬레이션이 할 수 없는 방식, 특히 조합 등가성 및 복잡한 타이밍 제약 조건에 대해 기능적 정확성을 검증할 수 있게 한다.
• 산업적 관련성: VERILOGEVAL-V2-EXT의 도입은 학술적 벤치마크와 산업용 IP 블록 요구사항 사이의 간극을 메우며, 엔드 투 엔드 RTL 생성 능력을 평가하기 위한 더 현실적이고 변별력 있는 테스트베드를 제공한다.

저자들은 대규모 사전 학습이 강력한 토대를 제공하지만, 복잡한 멀리 사이클 하드웨어 설계를 위해 높은 신뢰성을 달성하려면 형식 검증을 포함한 구조화된 에이전트 워크플로우가 필수적이라고 결론짓는다.