AssertLLM2: 설계 사양으로부터의 Assertion 생성을 위한 종합적인 LLM 벤치마크

Assertion 기반 검증 (Assertion-based verification, ABV)은 현대 하드웨어 설계의 초석이지만, 설계 의도를 공식적인 SystemVerilog Assertions (SVAs)로 수동 변환하는 작업은 여전히 노동 집약적이며 오류가 발생하기 쉽습니다. 대규모 언어 모델 (Large Language Models, LLMs)이 이 과정을 자동화하는 데 유망한 가능성을 보여주고 있지만, 기존의 벤치마크들은 비현실적인 작업 구성, 취약한 사양 입력, 그리고 지나치게 단순화된 평가로 인해 한계가 있습니다. 이러한 한계를 해결하기 위해, 우리는 하드웨어 검증에서의 현실적인 assertion 생성을 위한 오픈 소스 벤치마크인 AssertLLM2를 소개합니다. AssertLLM2는 13개의 기능적 카테고리에 걸쳐 83개의 실제 설계(real-world designs)를 포함하고 있습니다. 각 설계에 대해, 이 벤치마크는 구조화된 설계 사양(design specification), 검증된 의존성 완결형 골든 RTL (dependency-complete golden RTL), 그리고 체계적으로 변이된 버그가 있는 RTL 변체들을 제공합니다. 이는 두 가지 실질적인 설정(settings)을 지원합니다: 설계 오류를 방지하기 위해 사양으로부터 assertion을 생성하는 버그 방지 (bug-prevention), 그리고 의도된 동작과 결함이 있는 구현 사이의 불일치를 드러내기 위해 assertion을 생성하는 버그 탐색 (bug-hunting)입니다. 우리가 알고 있는 바로는, AssertLLM2는 버그 탐지 능력 (bug-detection capability)을 평가하기 위해 버그가 있는 RTL을 입력값으로 명시적으로 사용하는 최초의 벤치마크입니다. AssertLLM2는 더 나아가 구문적 유효성 (syntactic validity), 형식적 증명 가능성 (formal provability), 커버리지 (coverage), 그리고 변이 기반 버그 탐지 (mutation-based bug detection)를 아우르는 더욱 엄격한 평가 프레임워크를 채택합니다. 우리의 벤치마크는 assertion 생성에 대한 더욱 현실적이고 광범위한 평가를 가능하게 하며, 실제 하드웨어 검증 분야에서 최신 LLM (state-of-the-art LLMs)을 위한 엄격한 베이스라인을 구축합니다.