Autoformalizing Memory Specifications with Agents

"Autoformalizing Memory Device Specifications with Agents" 논문은 ICLR 2026 에서 발표되었으며, 이에 대한 상세한 기술 요약은 다음과 같습니다.

1. 문제 제기

반도체 칩 설계의 설계 검증 (DV) 단계는 주요 병목 현상으로, 설계 수명 주기의 50% 이상을 소모합니다. 핵심 과제는 메모리 칩의 JEDEC 표준과 같은 비구조화된 자연어 명세를 검증에 필요한 형식적이고 실행 가능한 모델로 변환하는 데 있습니다.

현재의 AI 접근 방식은 일반적으로 고립된 SystemVerilog Assertions(SVA) 생성에 중점을 둡니다. 그러나 이 접근 방식에는 다음과 같은 중대한 한계가 있습니다:

• 불완전성: SVAs 는 특정 속성을 검증하지만, 완전한 동작 모델, 자극 생성기 (stimulus generators), 또는 기능적 커버리지 지표를 생성하지는 않습니다.
• 모호성: 자연어 명세에는 종종 모호성이 포함되어 있어, 대규모 언어 모델 (LLM) 이 구문적으로 유효하지 않거나 프로토콜과 일치하지 않는 어설션을 생성하게 만듭니다.
• 복잡성: 최신 메모리 표준 (DDR5, HBM3, GDDR7) 은 정교한 타이밍 제약, 복잡한 명령 상호작용, 계층적 구조를 포함하며, 단순한 프롬프트 - 코드 생성으로는 이를 포착하기 어렵습니다.

2. 방법론

저자들은 자연어 메모리 명세를 SVAs 를 직접 생성하는 대신, 구조화되고 실행 가능한 중간 표현인 DRAMPyML로 변환하는 에이전트 기반 자동 형식화 프레임워크를 제안합니다.

2.1 중간 표현: DRAMPyML

어설션으로 바로 넘어가는 대신, 이 시스템은 Timed Petri Nets를 기반으로 구축된 Python 기반 모델링 언어인 DRAMPyML을 목표로 합니다.

• 구조: 메모리 장치를 위치 (뱅크, 랭크), 전이 (ACT, RD, WR 와 같은 명령), 그리고 아크 (일반, 억제, 리셋, 타이밍) 의 튜플로 모델링합니다.
• 장점: 이 표현은 실행 가능하여 명령 트레이스, 자극, 타이밍 검사를 생성할 수 있게 합니다. 이는 하류에서 SVAs, 테스트벤치, 커버리지 모델을 유도할 수 있는 통합 소스 역할을 합니다.
• 형식적 정의: 논문은 DRAM 페트리 네트워크를 수학적으로 정의하고 트레이스 동등성 (Trace Equivalence) 개념을 도입합니다. 저자들은 가설 3.4를 제기하고 경험적으로 검증하는데, 이는 대칭성 특성으로 인해 작은 구성 (예: 1 또는 2 개의 뱅크) 과 짧은 트레이스 길이 ($k=4$) 에 대한 트레이스 동등성을 검증하는 것이 전체 복잡 장치를 증명하기에 충분하다는 것입니다.

2.2 자동 형식화 에이전트

이 시스템은 원샷 (one-shot) 생성 방식이 아닌 반복적인 에이전트 워크플로우(논문의 Figure 2) 를 활용합니다:

1. 입력: 에이전트는 JEDEC PDF 명세, 벤더 데이터시트, 그리고 DRAMPyML 라이브러리를 수신합니다.
2. 반복 루프: 에이전트는 도구 (MCP 서버, LLM API) 를 사용하여 다음을 수행합니다:
   • 명세의 특정 섹션을 읽습니다.
   • 페트리 네트워크 그래프를 구축하기 위해 Python 코드를 작성하거나 편집합니다.
   • 자기 검증: 내부 검증 테스트를 실행하여 (데드락, 고립된 노드 확인 및 명세와 교차 검증을 위한 명령 트레이스 생성)
3. 정제: 검증 피드백을 기반으로 에이전트는 구조적 일관성과 타이밍 정확도가 충족될 때까지 모델을 반복적으로 정제합니다.
4. 프롬프트 전략: 이 연구는 명시적 관례가 포함된 단일 프롬프트인 One-Shot 프롬프팅과 환경 및 도구와의 반복적 상호작용인 에이전트 방식을 비교합니다.

3. 주요 기여

1. DRAMBench: DDR2-5, LPDDR2-5, GDDR5-7, HBM2-3 을 포함하는 13 개의 JEDEC 표준에 대한 정답 (ground-truth) DRAMPyML 형식화를 포함한 하드웨어 자동 형식화를 위한 최초의 오픈소스 벤치마크를 공개했습니다.
2. 에이전트 프레임워크: 도구 증강 검증을 사용하는 반복적 에이전트가 복잡한 명세의 경우 특히 원샷 생성보다 훨씬 뛰어난 성능을 보임을 입증했습니다.
3. 이론적 및 경험적 검증:
   • DRAM 페트리 네트워크 및 트레이스 동등성의 형식적 정의.
   • 최소 구성 (1-2 개 뱅크) 에서 짧은 트레이스 ($k \le 4$) 를 검사함으로써 생성된 모델의 의미론적 버그를 감지할 수 있으며, 상태 공간 폭발 문제를 우회할 수 있다는 경험적 증명.
4. 벤치마킹 결과: Sonnet 4.5, GPT-5.2, DeepSeek-v3p2 와 같은 최신 모델들의 포괄적 평가를 통해 토큰 비용과 성능 간의 트레이드오프를 보여주었습니다.

4. 실험 결과

저자들은 DRAMBench 데이터셋을 사용하여 두 가지 지표를 통해 모델을 평가했습니다:

• 자카드 지수 (Jaccard Index): 생성된 모델과 정답 간의 합법적 명령 트레이스 중첩을 측정합니다.
• 타이밍 제약 회상 (Timing Constraint Recall): 정답의 타이밍 제약 중 올바르게 복구된 비율을 측정합니다.

주요 발견:

• 에이전트 vs 원샷: 에이전트 접근 방식은 특히 복잡한 표준 (예: DDR5, HBM3) 이고 예시가 제공되지 않은 경우 일관되게 더 높은 최대 성능을 달성했습니다. 원샷 생성은 강력한 사전 지식이 없는 경우 익숙하지 않은 출력 형식에 어려움을 겪었습니다.
• 예시의 영향: "체리픽"된 예시 (예: DDR4 생성을 위해 DDR3 사용) 를 제공하는 것은 두 방법 모두의 성능을 크게 향상시켰으며, 때로는 단순한 작업에서 원샷 모델이 에이전트보다 우수한 성과를 내기도 했습니다.
• 모델 성능:
  • DeepSeek-v3p2(오픈 가중치) 는 폐쇄형 소스 모델 (Sonnet 4.5, GPT-5.2) 과 경쟁력 있는 성능을 보였으며, 에이전트 설정에서는 종종 이를 능가했습니다.
  • Sonnet 4.5는 예시가 제공되었을 때 HBM2 및 DDR2-4 와 같은 표준에 대해 가장 높은 구조적 완벽함을 달성했습니다.
• 실패 모드: 복잡한 실패 (예: DDR5) 에 대한 분석은 에이전트가 다음에서 어려움을 겪는 것을 드러냈습니다:
  • 올바른 원시 (primitives) 선택 (예: 잘못된 프리차지 명령).
  • 메모리 계층 구조 모델링 (예: 뱅크 그룹).
  • 올바른 추상화 수준에서 타이밍 제약 강제 (좌표 불일치로 인해 타이밍 아크가 비활성화됨).
• 토큰 효율성: 에이전트는 더 높은 정확도를 달성하지만 더 많은 토큰을 소모합니다. 그러나 복잡한 명세의 경우, 원샷 모델이 토큰 수와 관계없이 올바른 구조에 수렴하지 못하기 때문에 "토큰 대 성능" 곡선은 에이전트를 지지합니다.

5. 의의

이 연구는 하드웨어 검증의 패러다임 전환을 의미합니다:

• 어설션에서 모델로: 고립된 어설션 생성을 넘어 실행 가능하고 구조화된 동작 모델을 생성하는 것으로 이동합니다. 이는 검증의 "시프트 - 왼쪽 (shift-left)"을 가능하게 하여 설계 결함의 조기 발견과 자극, 커버리지, SVAs 와 같은 다양한 부수 자료의 자동 생성을 가능하게 합니다.
• 확장성: DRAMPyML 중간 표현과 트레이스 동등성 검사를 활용함으로써, 이전에는 자동 형식화에 너무 복잡했던 최신의 고도로 병렬화된 메모리 장치를 검증할 수 있는 확장 가능한 경로를 제공합니다.
• 오픈 사이언스: DRAMBench의 공개는 AI 를 하드웨어에 적용하는 문헌에서 이전까지 부재했던 표준화되고 전문급의 벤치마크를 제공하여, 하드웨어 자동 형식화 분야의 진전을 커뮤니티가 추적할 수 있게 합니다.

결론적으로, 이 논문은 에이전트 워크플로우와 구조화된 중간 표현(페트리 네트워크) 의 결합이 현재 직접 - 어설션 LLM 접근 방식의 한계를 극복하고 복잡한 반도체 표준 검증을 자동화하는 가장 실현 가능한 경로임을 입증합니다.