HierSVA: LLM 기반 계층적 하드웨어 형식 검증을 위한 데이터 합성 파이프라인, 데이터셋 및 벤치마크

우리는 LLM (Large Language Model) 기반의 계층적 하드웨어 형식 검증 (Formal Verification)을 위한 파이프라인, 데이터셋 및 벤치마크를 결합한 통합 스위트인 HierSVA를 제시합니다. HierSVA-SP는 RTL 전처리 툴체인과 LLM-in-the-loop 형식 검증 흐름을 결합하여 계층적 RTL 상에서 참조용 SystemVerilog Assertions (SVA)를 생성합니다. 이를 BaseJump STL에 적용하여 계층 메타데이터와 깊이 0~9를 포함하는 342개 모듈로 구성된 데이터셋인 HierSVA-DS를 구축하였으며, 자연어 명세와 버그 변형을 포함하는 28개의 모듈-버그 쌍으로 구성된 딥 서브셋 (deep subset)을 함께 제공합니다. HierSVA-B는 어설션 (assertion) 품질을 구문 정확성 (syntax correctness), 어설션 증명 성공률 (assertion proof success rate), 공허성 (vacuity), 명세 충실도 (specification faithfulness), 뮤테이션 커버리지 (mutation coverage), 형식 코어 커버리지 (formal core coverage)의 6가지 지표 축으로 분해합니다. 최근 12개의 LLM에 HierSVA-B를 적용한 결과 세 가지 발견을 도출했습니다. 첫째, 모듈 수준의 컴파일 성공률은 67.1%입니다. 평가 가능한 실행에서 생성된 어설션 중 82.1%가 공허하지 않게 (non-vacuously) 증명되지만, 해당 어설션 세트는 주입된 적격 결함의 70.2%만을 탐지하며 형식 코어의 36.2%만을 커버합니다. 둘째, 딥 서브셋의 211개 평가 가능한 모델-모듈 항목에 대해, 어설션 세트는 0.87의 재현율 (recall)로 버그가 있는 RTL을 찾아내지만, 예측된 버그 결과의 40%가 올바른 RTL에 대한 거짓 양성 (false positive)으로 나타나 정밀도 (precision)가 0.60으로 제한됩니다. 셋째, 에이전틱 모드 (agentic mode)는 S1 스타일의 증명 가능성 및 강도 지표를 개선하지만, 이득이 정체되거나 진동하는 양상을 보입니다. 코드 및 결과물은
ef{https://github.com/HierSVAAnon/HierSVACodeAndArtifacts}{https://github.com/HierSVAAnon/HierSVACodeAndArtifacts}에서 확인할 수 있습니다. 데이터셋은
ef{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA}{https://huggingface.co/datasets/AnonymousHierSVA/HierSVA}에서 사용할 수 있습니다.