기술 요약: CktFormalizer

문제 정의

하드웨어 설계는 여전히 오류가 발생하기 쉬운 분야로, 비트 너비 불일치, 조합 루프, 또는 유한 상태 기계 (FSM) 의 불완전한 케이스 논리와 같은 미묘한 결함은 구문 검사에서는 통과하지만 합성 중에는 침묵하며 실패하거나 나중에 고비용의 실리콘 버그로 나타날 수 있습니다. 대규모 언어 모델 (LLM) 이 자연어 명세에서 베릴로그 (Verilog) 를 생성하는 능력을 입증했음에도 불구하고, 생성된 코드는 종종 베릴로그와 VHDL 의 고유한 함정을 물려받습니다. 즉, 의존형 타입, 포괄적인 패턴 매칭, 기계 검증 증명과 같은 정적 보장이 부족합니다. 그 결과, LLM 이 생성한 하드웨어는 광범위한 수동 디버깅이 필요하며, 시뮬레이션상 기능적으로 정확하더라도 물리적 구현 (Place-and-Route, DRC, LVS) 에 도달하지 못하는 경우가 많습니다.

방법론

본 논문은 Lean 4에 내장된 의존형 타입 하드웨어 기술 언어 (HDL) 를 대상으로 하여 LLM 기반 코드 생성과 형식 검증을 통합하는 CktFormalizer 프레임워크를 제시합니다. 베릴로그를 직접 생성하는 대신, 이 시스템은 LLM 에이전트가 주 컴파일 대상인 Lean 코드를 생성하도록 유도합니다.

핵심 아키텍처

이 프레임워크는 Lean 의 세 가지 고유한 역할을 포함하는 폐쇄 루프 파이프라인을 통해 작동합니다.

1. 타입 체커 (컴파일 타임 검증기): Lean 의 의존형 타입 시스템은 비트 너비 제약, 케이스 커버리지, 그리고 비순환성을 인코딩합니다. 하드웨어 결함 (예: 너비 불일치 또는 조합 루프) 은 침묵하는 백엔드 실패가 아닌 컴파일 타임 타입 오류로 포착됩니다. 이는 LLM 에이전트에게 설계를 반복적으로 수정할 수 있는 즉각적이고 실행 가능한 피드백을 제공합니다.
2. 정확성 방화벽: Lean 에서 성공적으로 컴파일된 설계는 특정 유형의 결함 (너비 불일치, 조합 루프, 의도하지 않은 래치) 이 구조적으로 보장되어 없습니다. 이는 컴파일된 설계가 베이스라인 베릴로그 생성에서 관찰된 20% 의 손실률 없이 백엔드 합성 및 Place-and-Route (P&R) 플로우를 통과할 수 있음을 보장합니다.
3. 증명 도우미: 에이전트는 자연어 명세와 생성된 (또는 최적화된) 구현체 간의 기능적 동등성을 검증하기 위해 자동화된 정리 증명을 구성합니다. 이러한 증명은 임의의 입력 시퀀스와 매개변수화된 너비를 다루며, 유계 SMT 기반 검사의 한계를 넘어섭니다.

워크플로우

1. 생성 및 반복: 자연어 명세를 기반으로 LLM 에이전트 (Claude 로 인스턴스화됨) 가 Lean HDL 코드를 생성합니다. 이는 Lean 컴파일러 오류가 에이전트가 시맨틱 버그가 전파되기 전에 수정하도록 안내하는 반복적인 "생성 - 컴파일 - 수정" 루프에 진입합니다.
2. 추출: 컴파일에 성공하면 메타프로그램 (#synthesizeVerilog) 이 Lean 신호 조합자 그래프에서 합성 가능한 SystemVerilog 를 추출합니다.
3. 물리적 구현: 추출된 SystemVerilog 는 시뮬레이션되고 (Yosys 사용 합성), 물리적으로 구현되어 (SkyWater 130nm PDK 를 사용한 OpenROAD) GDSII 레이아웃 및 전력 - 성능 - 면적 (PPA) 지표를 생성합니다.
4. PPA 최적화 루프: 폐쇄 루프 최적화 단계는 PPA 지표를 에이전트에 피드백합니다. 에이전트는 아키텍처 변형 (예: 병렬 대 직렬 데이터 경로) 을 제안하고, 최적화된 변형이 원래 명세와 기능적으로 동등함을 보장하기 위해 기계 검증 동등성 증명을 제공해야 합니다.

주요 기여

1. 최초의 엔드투엔드 프레임워크: CktFormalizer 는 LLM 기반 하드웨어 생성과 Lean 내장 HDL 을 결합하여 자연어에서 합성 가능한 실리콘까지 폐쇄 루프 PPA 최적화를 제공하는 최초의 프레임워크입니다.
2. 타입 유도 생성: 본 논문은 타입 안전한 HDL 을 대상으로 하는 것이 직접적인 베릴로그 생성에 비해 LLM 성공률을 크게 향상시킨다는 것을 입증합니다. 컴파일 타임 타입 오류는 에이전트를 올바른 설계로 이끄는 구조화된 피드백을 제공하여, 멀티 채널 핸드셰이크 버스 인터페이스와 같은 산업 관련 IP 로 확장 가능합니다.
3. 형식 검증 통합: 이 프레임워크는 에이전트가 기계 검증 동등성 증명을 생성할 수 있게 함으로써 LLM 생성 코드와 증명 가능한 정확한 하드웨어 간의 간극을 해소합니다. 이는 아키텍처 최적화가 기능적 정확성을 훼손하지 않도록 보장합니다.

실험 결과

이 프레임워크는 VerilogEval(156 개 문제), RTLLM(50 개 문제), ResBench(56 개 문제) 의 세 가지 벤치마크에서 평가되었습니다.

• 백엔드 실현 가능성: CktFormalizer 가 기능적 정확성을 백엔드를 통해 유지한다는 것이 중요한 발견입니다. 베이스라인 (직접 베릴로그 생성) 은 합성 및 라우팅 중에 기능적으로 정확한 설계의 약 20% 를 손실하는 반면, CktFormalizer 는 전체 합성, P&R, DRC, LVS 플로우를 통해 컴파일된 설계의 **100%**를 유지합니다.
• 컴파일 및 시뮬레이션: VerilogEval 에서 CktFormalizer 는 92.3% 의 Lean 컴파일률과 72.4% 의 RTL 시뮬레이션 통과율을 달성하여 직접 베릴로그 생성 베이스라인과 경쟁력 있는 성과를 보였습니다. 에이전트 루프에 합성 피드백이 포함되면 컴파일률은 99.4% 로 상승합니다.
• PPA 최적화: 폐쇄 루프 최적화 단계는 상당한 개선을 가져왔습니다. 검증된 아키텍처 탐색을 통해 이 프레임워크는 최대 35% 의 면적 감소와 30% 의 전력 감소를 달성했습니다.
• 타이밍 클로저: Place-and-Route 를 완료한 모든 기능적으로 올바른 설계는 수동 개입 없이 타이밍 클로저 (WNS $\ge$ 0 ns) 를 달성했습니다.
• 증명 생성: 파일럿 연구에서 단계별 증명 생성 (증명 목표 피드백을 통한 반복적 정제) 은 증명 완료율을 53% 에서 63% 로 향상시켜 하드웨어 검증을 위한 증명 도우미의 타당성을 입증했습니다.

중요성 및 주장

본 논문은 의존형 타입과 LLM 에이전트가 상호 보완적이라고 주장합니다. 형식 언어 (Lean) 를 생성 대상이자 검증 기저로 동시에 사용함으로써, 이 프레임워크는 LLM 의 "생성 및 테스트" 루프를 문법적으로 유효한 프로그램에 대한 확률적 탐색에서 타입 유도 정제 과정으로 변환합니다.

저자들은 컴파일러를 검증기로 작용하게 하여 오류 감지를 EDA 파이프라인의 끝 (수정이 비용이 많이 드는 곳) 에서 컴파일 시점으로 이동시킨다고 강조합니다. 이 접근 방식은 시스템이 기능적으로 정확할 뿐만 아니라 백엔드 변환에 대해 구조적으로 견고한 하드웨어를 생성할 수 있게 하여, LLM 생성 하드웨어에서 흔히 발생하는 "침묵하는 실패" 문제를 효과적으로 해결합니다. 이 연구는 형식 언어가 신뢰할 수 있는 자동화 하드웨어 설계의 기초가 되어 LLM 이 엄격한 정확성 보장을 유지하면서 하드웨어 최적화의 복잡한 트레이드오프를 탐색할 수 있음을 시사합니다.