CktFormalizer: 자연어를 회로 표현으로 자동 형식화하기

LLM(Large Language Models)은 자연어 명세로부터 하드웨어 기술을 생성할 수 있지만, 결과물인 Verilog에는 비트 폭 불일치(width mismatches), 조합 루프(combinational loops), 불완전한 케이스 로직(incomplete case logic) 등이 포함되는 경우가 많습니다. 이러한 오류들은 구문 검사(syntax checks)는 통과할지라도 합성(synthesis)이나 실리콘 단계에서는 실패하게 됩니다. 본 논문에서는 Lean 4에 임베디드된 의존 타입(dependently-typed) HDL을 통해 LLM 기반의 하드웨어 생성을 재지시하는 프레임워크인 CktFormalizer를 제안합니다. Lean은 세 가지 역할을 수행합니다: (i) 타입 검사기(type checker): 의존 타입은 비트 폭 제약(bit-width constraints), 케이스 커버리지(case coverage), 비순환성(acyclicity)을 인코딩하여 하드웨어 결함을 반복적인 수정을 유도하는 컴파일 타임 에러로 변환합니다; (ii) 정밀도 방화벽(correctness firewall): 컴파일된 설계는 백엔드에서 조용히 실패를 일으키는 결함으로부터 구조적으로 자유롭습니다 (기존 베이스라인은 합성 및 라우팅 과정에서 올바른 설계의 20%를 손실하는 반면, CktFormalizer는 이를 모두 보존합니다); (iii) 증명 보조 도구(proof assistant): 에이전트는 유한한 SMT 기반 검증(bounded SMT-based checking)의 범위를 넘어, 임의의 입력 시퀀스와 매개변수화된 폭(parameterized widths)에 대해 기계 검증된 등가성 증명(equivalence proofs)을 구축합니다. VerilogEval (156개 문제), RTLLM (50개 문제), ResBench (56개 문제)에서 CktFormalizer는 직접적인 Verilog 생성 방식과 경쟁할 만한 시뮬레이션 통과율을 달성하는 동시에, 실질적으로 훨씬 높은 백엔드 구현 가능성(backend realizability)을 제공합니다: 컴파일된 설계의 95~100%가 전체 합성(synthesis), 배치 및 라우팅(place-and-route), DRC, LVS 흐름을 완료합니다. 폐쇄 루프 PPA(Power, Performance, Area) 최적화 단계는 검증된 아키텍처 탐색을 통해 최대 35%의 면적 감소와 30%의 전력 감소를 달성하며, 자동화된 정리 증명(automated theorem proof)을 통해 각 최적화된 변형이 공식 명세(formal specification)와 기능적으로 동일함을 보장합니다.