Daily Arxiv

전 세계에서 발간되는 인공지능 관련 논문을 정리하는 페이지 입니다.
본 페이지는 Google Gemini를 활용해 요약 정리하며, 비영리로 운영 됩니다.
논문에 대한 저작권은 저자 및 해당 기관에 있으며, 공유 시 출처만 명기하면 됩니다.

AssertionForge: Enhancing Formal Verification Assertion Generation with Structured Representation of Specifications and RTL

Created by
  • Haebom

저자

Yunsheng Bai, Ghaith Bany Hamad, Syed Suhaib, Haoxing Ren

개요

자연어 명세로부터 SystemVerilog Assertions (SVAs)를 생성하는 것은 명세의 모호성과 불완전성으로 인해 형식 검증(FV)에서 주요 과제로 남아 있습니다. AssertLLM과 같은 기존의 LLM 기반 접근 방식은 명세 문서에서만 정보를 추출하는 데 집중하여 RTL 코드에 존재하는 필수적인 내부 신호 상호 작용 및 설계 세부 정보를 포착하지 못하여 불완전하거나 잘못된 어서션을 생성하는 경우가 많습니다. 본 논문에서는 명세와 RTL 모두에서 도메인 특정 엔티티 및 관계 유형을 갖는 하드웨어 특정 스키마를 사용하여 지식 그래프(KG)를 구성하는 새로운 접근 방식을 제안합니다. 명세로부터 초기 KG를 생성한 다음 RTL 코드에서 추출한 정보와 체계적으로 융합하여 통합되고 포괄적인 KG를 생성합니다. 이러한 결합된 표현은 설계에 대한 보다 철저한 이해를 가능하게 하고 KG에서 다양한 검증 컨텍스트를 추출하도록 설계된 다중 해상도 컨텍스트 합성 프로세스를 허용합니다. 네 가지 설계에 대한 실험은 제안된 방법이 기존 방법보다 SVA 품질을 크게 향상시킨다는 것을 보여줍니다. 이러한 구조화된 표현은 FV를 개선할 뿐만 아니라 코드 생성 및 설계 이해와 같은 향후 연구를 위한 길을 열어줍니다.

시사점, 한계점

시사점: RTL 코드와 명세를 통합한 지식 그래프를 활용하여 SVA 생성의 정확도와 완성도를 크게 향상시켰습니다. 기존 LLM 기반 방법의 한계를 극복하고 다양한 검증 컨텍스트를 추출하는 다중 해상도 컨텍스트 합성 프로세스를 제시했습니다. 코드 생성 및 설계 이해 등 향후 연구의 가능성을 제시합니다.
한계점: 제안된 방법의 성능 평가는 네 가지 설계에 국한되어 있으며, 더욱 다양하고 복잡한 설계에 대한 추가적인 실험이 필요합니다. 하드웨어 특정 스키마의 일반성과 확장성에 대한 추가적인 연구가 필요합니다. 자연어 명세의 모호성을 완전히 해결하는 것은 여전히 어려운 과제입니다.
👍