CktFormalizer: 자연어로부터 회로 표현의 자동 형식화

요약

CktFormalizer는 LLM 기반 하드웨어 생성의 신뢰성 문제를 해결하기 위해 개발된 프레임워크입니다. 이 프레임워크는 Lean 4에 임베딩된 종속 타입 언어(dependently-typed HDL)를 사용하여, 자연어 사양으로부터 생성되는 Verilog 코드가 컴파일 타임에 하드웨어 결함(예: 너비 불일치, 루프 등)을 가지지 않도록 강제합니다. 이를 통해 기존 방식에서 발생하던 합성 단계의 실패율을 획기적으로 줄이고 디자인의 정확성을 높입니다.

핵심 포인트

• LLM이 생성한 하드웨어 코드(Verilog)는 종종 구문은 맞지만, 실제 합성이나 실리콘 단계에서 결함(너비 불일치, 루프 등)을 포함합니다.
• CktFormalizer는 Lean 4 기반의 종속 타입 언어(dependently-typed HDL)를 사용하여 하드웨어 생성을 재지향합니다.
• Lean의 타입 검사기는 비트 너비 제약 조건, case 커버리지, 무순환성 등을 인코딩하여 결함을 컴파일 타임 오류로 변환하고 수정 가이드를 제공합니다.
• 이 프레임워크는 디자인을 구조적으로 결함으로부터 보호하는 '정확성 방화벽(correctness firewall)' 역할을 수행합니다.