기술 요약: SpecAlign – SystemVerilog 어설션 생성을 위한 시맨틱 정렬 프레임워크

1. 문제 제기

현대 하드웨어 설계의 복잡성 증가로 인해 어설션 기반 검증 (ABV) 을 지원하기 위해 SystemVerilog 어설션 (SVA) 생성에 대규모 언어 모델 (LLM) 의 도입이 확대되고 있습니다. 그러나 기존 LLM 접근법은 주로 구문적 유효성과 형식 검증 (FV) 결과 (예: 특정 RTL 에서 어설션이 증명되거나 반례를 산출하는지 여부) 에 중점을 둡니다. 이러한 지표들은 생성된 어설션이 자연어 명세서에 기술된 행동 의도를 정확하게 반영하는지 여부를 다루는 시맨틱 정렬 (semantic alignment) 문제를 해결하지 못합니다.

LLM 은 특정 RTL 구현에서 구문적으로 정확하고 형식적으로 증명 가능한 어설션을 생성할 수 있지만, 시맨틱적으로는 비효율적이거나 환각 (hallucinated) 된 결과를 낳을 수 있습니다. 예를 들어, 어설션이 속성을 트리거하는 동일한 엣지에서 클럭을 샘플링하는 경우, FV 를 통과하더라도 공허한 (vacuous) 결과가 될 수 있습니다. 비교를 위한 '골든 (golden)' RTL 모델이 부재한 상황에서 이러한 어설션을 수동으로 검사하는 것은 시간이 많이 소요되며 신뢰도를 저하시킵니다. 또한, FV 엔진은 복잡한 설계에 대해 생성된 방대한 어설션 세트를 평가할 때 상태 공간 폭발 (state-space explosion) 과 같은 확장성 문제에 직면합니다. 따라서 RTL 구현 세부사항에 의존하지 않고 명세서 자체에 대한 시맨틱 일관성을 평가하는 프레임워크에 대한 시급한 필요성이 존재합니다.

2. 방법론: SpecAlign 프레임워크

SpecAlign 은 골든 RTL 에 의존하지 않고 LLM 이 생성한 SVA 를 평가하고 반복적으로 정제하기 위해 설계된 명세서 중심 프레임워크입니다. 이는 속성 정렬 루프 (Property Alignment Loop) 와 SVA 정렬 루프 (SVA Alignment Loop) 라는 두 가지 주요 반복 루프를 통해 작동합니다. 두 루프 모두 정렬 확인, 불일치 분석, 증거 추출이라는 세 가지 핵심 단계를 활용합니다.

A. 아키텍처 개요

이 프레임워크는 설계 의도의 서로 다른 표현 간의 비교를 표준화합니다. 입력은 자연어 속성 ($P$) 과 생성된 SVA($A$) 로 구성되지만, 프레임워크는 특정 추출 과정을 통해 모든 SVA 를 자연어 요약 ($N$) 으로 변환합니다. 이 표준화를 통해 속성과 어설션 모두 설계 명세서 ($S$) 에 대해 동일한 시맨틱 수준에서 평가될 수 있습니다.

B. 핵심 구성 요소

1. 정렬 확인 (Alignment Checking):

   • 분류: 프레임워크는 명세서와의 관계에 따라 자연어 설명 ($X_i$) 을 세 가지 범주로 분류합니다.
     • 함의 (Entails): 모든 요소가 명세서에 의해 지원됨.
     • 모순 (Contradicts): 적어도 하나의 요소가 명세서와 모순됨.
     • 알 수 없음 (Unknown): 요소가 지원되지도 모순되지도 않음 (종종 명세서에 없는 구현 특유의 가정으로 인해 발생).
   • 자기 일관성 투표 (Self-Consistency Voting): 신뢰성을 높이기 위해 시스템은 사고의 연쇄 (Chain-of-Thought, CoT) 프롬프트 전략을 사용합니다. 주어진 입력에 대해 $k$개의 추론 경로를 생성하고 다수결 투표를 사용하여 하위 판정을 집계합니다. 동점인 경우 보수적 우선순위가 적용됩니다: 모순 > 알 수 없음 > 함의.
   • 참조 선택: 속성 루프는 설계 명세서 ($S$) 를 참조로 사용합니다. SVA 루프는 산재된 명세서 문서의 노이즈를 줄이기 위해 '정렬된 속성 뱅크 (Aligned Property Bank)'를 (사용 가능한 경우) 사용하며, 그렇지 않으면 $S$로 대체합니다.

2. 불일치 분석 및 정제 (Inconsistency Analysis & Refinement):

   • 판정이 모순 (Contradicts) 일 때, 시스템은 불일치 분석을 수행합니다. 설명 내의 특정 충돌 요소를 식별하고, 명세서의 올바른 행동을 참조하여 구조화된 실행 가능한 피드백 ($F_i$) 을 생성합니다.
   • 이 피드백은 LLM 이 속성이나 어설션 ($P'_i$ 또는 $A'_i$) 을 재생성하도록 안내하며, 트리거 조건을 명시적으로 정의하고 명세서에 존재하지 않는 새로운 신호나 행동을 도입하지 않도록 합니다.
   • 정제된 출력은 고정된 반복 횟수에 도달하거나 출력이 정렬될 때까지 정렬 루프에서 재평가됩니다.

3. 증거 추출 (Evidence Extraction):

   • 함의 (Entails) 사례의 경우, 시스템은 명세서에서 지지 증거 (인용구 및 위치) 를 추출하여 인간 검토를 용이하게 하고 신뢰도를 강화합니다.
   • 알 수 없음 (Unknown) 사례의 경우, 시스템은 모호하거나 정의되지 않은 요소를 분류하여 진정한 모순과 미명세된 행동을 구분합니다.

4. 정량적 지표:

   • 프레임워크는 주어진 반복 단계에서 함의된 어설션 ($E$) 의 수를 전체 어설션 수 ($n$) 로 나눈 비율로 계산되는 정렬 점수 ($a_t$) 를 정의합니다 ($a_t = E/n$). 정제 과정의 목표는 이 점수를 최대화하는 것입니다.

C. 자연어 요약 추출

중요한 전처리 단계는 형식적 SVA 를 구조화된 자연어 요약으로 변환하는 것입니다. LLM 은 특정 SVA 구성 요소 (트리거, 전제, 함의 연산자, 결과, Disable If) 를 식별하고 이를 동등한 자연어 구문으로 매핑하도록 프롬프트됩니다. 이를 통해 형식적 코드의 시맨틱 의도가 비교를 위해 보존됩니다.

3. 주요 기여

본 논문은 다음과 같은 기여를 제시합니다:

• 시맨틱 평가 프레임워크: 골든 RTL 에 적용된 형식 검증에 의존하지 않고 자연어 명세서에 대해 LLM 이 생성한 SVA 를 평가하는 새로운 접근법.
• 반복적 정제 파이프라인: 기존 LLM 기반 생성 워크플로우에 통합되도록 설계된 정렬 확인, 불일치 분석, SVA 요약 추출을 포함하는 구조화된 프레임워크.
• 정량적 정렬 지표: 명세서 일관성을 측정하기 위한 시맨틱 함의 분류 기반 정렬 점수 지표로, 전통적인 FV 정확도 평가에 대한 확장 가능한 대안을 제공.
• 불일치 분석 메커니즘: 모순되는 속성과 어설션에 대해 구체적이고 실행 가능한 피드백을 생성하는 방법으로, 수동 검토와 자동 정제를 모두 지원.
• 실증적 검증: 시맨틱 정제를 통해 APB 및 UART 설계에서 모순된 어설션을 감소시켰음을 보여주는 실험 결과.

4. 실험 결과

저자들은 SpecAlign 을 두 가지 하드웨어 설계, 즉 APB(APB to I2C 인터페이스) 와 UART(UART to Bus 인터페이스) 에서 평가했습니다. 이 프레임워크는 지식 그래프를 사용하고 생성에 RTL 을 포함하는 베이스라인 방법인 AssertionForge와 비교되었습니다.

• APB 결과:
  • 베이스라인 (AssertionForge): 442 개의 SVA 를 생성했으며 정렬 점수는 0.02였습니다. 함의된 것은 8 개뿐이었으며, 148 개는 모순되었습니다.
  • SpecAlign: 442 개의 SVA 를 유지하면서 정렬 점수를 0.15로 높였습니다. 결정적으로 모순된 어설션 수는 0으로 감소했고, 함의된 어설션은 66 개로 증가했습니다. 나머지 376 개는 '알 수 없음'으로 분류되었습니다.
• UART 결과:
  • 베이스라인: 325 개의 SVA 를 생성했으며 정렬 점수는 0.06(함의 21 개, 모순 142 개) 이었습니다.
  • SpecAlign: 319 개의 SVA 를 생성했으며 정렬 점수는 0.28이었습니다. 모순된 어설션은 6 개로 감소했고, 함의된 어설션은 92 개로 증가했습니다.

결과 분석:
실험 결과, 베이스라인 방법들은 명세서와 모순되거나 자연어 명세서에 없는 구현 특유의 세부사항 (RTL) 에 크게 의존하는 어설션을 생성하는 경향이 있음을 보여주었습니다. SpecAlign 은 이러한 모순을 효과적으로 필터링합니다. SpecAlign 에서 '알 수 없음' 분류가 증가한 것 (예: APB 의 376 개) 은 실패가 아니라, 구현 특유의 가정을 명세서 지원 행동과 분리하는 더 보수적이고 정확한 분류 전략으로 해석됩니다. 이 구별은 지원되지 않는 행동을 '함의된' 것으로 잘못 라벨링하는 것을 방지합니다.

5. 중요성 및 주장

본 논문은 SpecAlign 이 전통적인 형식 검증에 대한 확장 가능한 보완책을 제공한다고 주장합니다. 시맨틱 정확도를 RTL 증명 결과와 분리함으로써, 형식 검증만으로는 어설션이 명세서에 기술된 의도된 행동을 포착하는지 여부를 판단할 수 없다는 한계를 해결합니다.

저자들은 형식 검증이 RTL 에서 어설션이 성립함을 증명하는 데 필요하지만, 어설션 의도의 품질을 평가하기에는 불충분하다고 강조합니다. SpecAlign 은 다음과 같은 방식으로 LLM 이 생성한 어설션에 대한 신뢰도를 향상시킵니다:

1. 형식 도구가 놓칠 수 있는 시맨틱 불일치 (예: 공허한 진리) 를 감지.
2. RTL 시뮬레이션이나 형식 증명 전에 모순을 식별하여 디버깅 노력을 줄임.
3. 골든 모델이 필요 없이 어설션을 반복적으로 정제할 수 있는 메커니즘 제공.

본 논문은 겸손하게 결론을 내리며, 프레임워크가 정렬을 개선하지만 향후 분류 방법론을 정교화하고 구문적 오류를 더 잘 포착하며, RTL 생성 및 디버깅과 같은 다른 하드웨어 설계 자동화 작업으로 접근법을 확장하기 위한 추가 연구가 필요하다고 명시합니다.