🤖 AI

NeuroAbs: A Neuro-Symbolic RTL Abstraction Framework for Property Checking Acceleration

본 논문은 RTL 신호 식별을 위한 LLM과 AST 기반의 심볼릭 표현을 활용하고, SMT 기반의 건전성 검증 및 CEGAR 정교화 기법을 결합하여 RTL 추상화를 자동화함으로써 하드웨어 속성 검증을 획기적으로 가속화하는 뉴로-심볼릭 프레임워크인 NeuroAbs를 제시한다.

원저자: Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng, Ziyi Yang, Wenbin Che, Wei Zhang, Yangdi Lyu, Hongce Zhang

게시일 2026-08-19

📖 3 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Zhiyuan Yan, Xiaofeng Zhou, Ziyue Zheng, Ziyi Yang, Wenbin Che, Wei Zhang, Yangdi Lyu, Hongce Zhang

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

현대 전자 공학의 숨겨진 세계에서, 우리 전화기, 자동차, 컴퓨터를 구동하는 칩들은 수십억 개의 아주 작은 스위치들로 만들어집니다. 이 칩들이 제조되기 전, 엔지니어들은 어떤 명령을 받더라도 의도한 대로 정확하게 작동할 것임을 반드시 증명해야 합니다. '형식 검증(formal verification)'이라고 알려진 이 과정은 설계에 숨겨진 결함이 없음을 보장하는 엄격한 수학적 점검입니다. 그러나 이러한 설계가 더욱 복잡해짐에 따라, 이를 검증하는 작업은 압도적인 과제가 됩니다. 칩이 진입할 수 있는 가능한 상태의 수가 너무나 방대하여, 가장 강력한 컴퓨터조차 합리적인 시간 내에 그 모든 상태를 탐색하는 데 어려움을 겪습니다. 이를 해결하기 위해 엔지니어들은 종종 '추상화(abstraction)'라고 불리는 기법을 사용하는데, 이는 특정 테스트에 중요하지 않은 세부 사항들을 제거함으로써 복잡한 설계를 단순화하는 방식으로, 마치 특정 여행에 필요한 주요 도로만을 보여주고 모든 골목길과 뒷길은 무시하는 도시의 지도와 같이 작동합니다.

수년 동안, 이러한 단순화된 모델을 만드는 작업은 인간 전문가의 지루한 수작업에 의존하거나, 특정 설계의 미묘한 차이를 놓치기 쉬운 경직되고 미리 프로그래밍된 규칙에 의존해야 했습니다. 'NeuroAbs'라는 새로운 접근 방식은 인공지능의 패턴 인식 능력과 형식 수학의 엄격한 논리를 결합하여 다른 길을 제시합니다. 이 방법은 대규모 언어 모델(방대한 양의 텍텍스트로 학습된 고급 AI 시스템)을 사용하여 하드웨어 설계의 의도와 충족해야 할 특정 속성을 이해합니다. AI는 회로의 어느 부분이 현재 테스트와 무관한지를 식별하고, 이를 어떻게 단순화할지 제안합니다. 하지만 AI는 때때로 실수를 하거나 논리를 깨뜨리는 변경 사항을 제안할 수 있기 때문에, 시스템은 AI를 맹목적으로 신뢰하지 않습니다. 대신, AI가 변경 사항을 제안하면 별도의 엄격한 수학 엔진이 해당 변경 사항이 안전한지 즉시 확인하는 '뉴로-심볼릭(neuro-symbolic)' 프레임워크로서 작동합니다. 만약 단순화가 너무 공격적이어서 실제 오류를 숨길 위험이 있다면, 시스템은 모델을 자동으로 정교화하여, 속도의 이점을 잃지 않으면서도 정확도를 회복할 수 있을 만큼만 단순화의 층위를 다시 벗겨냅니다.

연구진은 여러 실제 프로세서 설계와 많은 기기에 사용되는 일반적인 통신 인터페이스를 포함한 주변 장치 부품들에 대해 NeuroAbs 프레ร임워크를 테스트했습니다. 그들은 이 시스템이 전통적인 규칙 기반 방식이 놓쳤던 논리 단순화의 기회들을 성공적으로 식별할 수 있다는 것을 발견했습니다. 예를 들어, 프로세서의 특정 명령을 검증할 때, AI는 다른 관련 없는 명령들을 처리하는 로직을 일반적인 자리 표시자(placeholder)로 안전하게 대체할 수 있음을 파악했습니다. 이를 통해 검증 엔진은 회로의 관련 부분에만 집중할 수 있었습니다. 실험에서 이 접근 방식은 설계가 올바르다는 것을 증명하는 데 걸리는 시간을 크게 단축했습니다. 연구진이 NeuroAbs를 기존의 고성능 검증 도구와 통합했을 때, 많은 경우에 형식적 증명에 도달하는 데 필요한 시간이 거의 절반으로 줄어들었습니다. 완전한 증명이 시간 제한 내에 불가능한 경우에도, 단순화된 모델 덕분에 시스템은 회로의 동작을 훨씬 더 깊게 탐색하여, 그렇지 않았다면 숨겨져 있었을 잠재적인 버그들을 찾아낼 수 있었습니다.

이 방법의 성공은 AI의 유연성과 형식 논리의 정밀함 사이의 세심한 균형에 달려 있습니다. 시스템은 먼저 설계와 특정 테스트 시나리오를 분석하여 어떤 신호가 중요한지를 짚어냅니다. 그런 다음 AI를 사용하여 해당 특정 영역의 코드를 재작성하고, 복잡한 계산을 더 단순한 추상적 값으로 대체합니다. 결정적으로, 모든 재작성은 근본적인 칩의 동작을 변경하여 테스트를 무효화하지 않는지 확인하기 위해 엄격한 수학적 검사를 거칩니다. 만약 검사가 실패하면, 시스템은 피드백 루프를 사용하여 정확히 어떤 단순화가 문제를 일으켰는지 식별하고, 해당 부분을 원래의 형태로 되돌립니다. 이 반복적인 과정은 최종 모델이 빠르게 검증할 수 있을 만큼 충분히 단순하면서도, 신뢰할 수 있을 만큼 정확하도록 보장합니다. 결과는 이 하이브리드 접근 방식이 단순 산술 연산부터 복잡한 분기 구조에 이르기까지 다양한 유형의 하드웨어 로직을 처리할 수 있음을 보여주며, 차세대 칩 설계의 강력한 도구가 될 수 있음을 입증합니다.

이러한 단순화된 모델의 생성을 자동화함으로써, NeuroAbs는 하드웨어 공학의 주요 병목 현상을 해결합니다. 이전에는 무엇을 어떻게 단순화할지에 대한 결정이 인간의 직관이나 모든 독특한 설계 과제에 적응할 수 없는 고정된 규칙에 의존해야 했습니다. 이 새로운 프레임워크는 인공지능이 매 단계마다 검증하는 시스템에 의해 고정되어 있다면, 이러한 과업을 수행하도록 효과적으로 유도될 수 있음을 보여줍니다. 연구 결과는 하드웨어 검증의 미래가 기계가 패턴 인식과 제안이라는 힘든 일을 처리하고 수학적 엄격함이 최종 제품의 안전과 정확성을 보장하는 이러한 협력적 시스템에 있을 수 있음을 시사합니다. 칩 설계가 계속해서 복잡해짐에 따라, NeuroAbs와 같은 도구는 우리가 의지하는 기기들이 검증된 진실이라는 토대 위에 구축되도록 보장하며 그 속도를 맞출 수 있는 유망한 방법을 제공합니다.

기술 요약: NeuroAbs

문제 정의

형식 검증(Formal Verification), 특히 속성 확인(Property Checking/Model Checking)은 하드웨어 설계의 기능적 정확성을 보장하는 데 필수적입니다. 그러나 레지스터 전송 레벨(RTL) 설계의 규모와 복잡성이 커짐에 따라, 사용자가 지정한 속성을 효율적으로 증명하는 것이 중요한 병목 현상이 되고 있습니다. 추상화 기법은 구체적인 모델을 단순화된 표현으로 대체하여 시스템 복잡도를 줄이는 데 흔히 사용되지만, 기존 방법들은 두 가지 주요 한계점을 가집니다:

수동 추상화(Manual Abstraction): 인간의 통찰력에 크게 의존하며 노동 집약적입니다. 엔지니어가 특정 속성에 무관한 설계 부분을 수동으로 식별해야 합니다.
규칙 기반 자동 추상화(Rule-Based Automatic Abstraction): 구조적 추상화, 구문 가이드 추상화, 데이터패스 추상화(예: 산술 연산을 미해석 함수로 대체)와 같은 기법들은 유연성이 부족합니다. 이러한 방식은 사전 정의된 구문 규칙에 의존하기 때문에, 특정 검증 시나리오의 의미론적 의도와 대상 속성에 따른 추상화 기회를 식별하는 데 실패하는 경우가 많습니다.

결과적으로, 현재의 방법들은 특정 검증 목표와 무관한 로직을 안전하게 추상화할 기회를 놓치거나, 너무 거친(coarse) 추상화를 생성하여 허위 반례(spurious counterexamples)를 만들거나, 혹은 너무 보수적인(conservative) 추상화를 생성하여 검증 가속화를 저해하기도 합니다.

방법론: NeuroAbs 프레임워크

본 논문은 RTL 추상화를 자동화하기 위해 대규모 언어 모델(LLM)을 심볼릭 추론(Symbolic Reasoning)과 결려한 신경-심볼릭(Neuro-symbolic) 프레임워크인 NeuroAbs를 제안합니다. 이 프레임워크는 세 가지 별도의 단계로 작동합니다:

1. LLM 지원 신호 분석 (신경 구성 요소)

전체 RTL 코드베이스를 LLM에 입력하는 것은 컨텍스트 제한을 초과하므로, NeuroAbs는 추상화 대상 후보 신호를 식별하기 위해 **신호 분석기(Signal Analyzer)**를 사용합니다.

입력: 설계 사양, 검증 시나리오 설명, 신호 정의.
프로세스: 사고 사슬(Chain-of-Thought, CoT) 프롬프팅과 커스텀 시스템 지침을 사용하여, LLM은 검증 시나리오를 분석하여 "시나리오 관련 신호"를 식별합니다. LLM은 어떤 신호가 특정 속성과 관련된 로직을 제어하는지 결정하고, 고정된 값(예: 오퍼코드(opcode)를 특정 명령어 유형으로 설정)을 제안합니다.
정적 분석 통합: LLM의 출력은 RTL 정적 분석(예: 상수 전파)과 결합되어 해당 신호들에 의해 영향을 받는 특정 코드 영역과 문장을 국소화(localize)합니다. 이를 통해 범위를 전체 설계에서 작은 규모의 후보 문장 세트로 좁힙니다.

2. AST 가이드 추상화 (신경-심볼릭 핵심)

구조적 무결성을 보장하고 LLM이 무관한 로직을 재작성하는 것을 방지하기 위해, NeuroAbs는 RTL을 추상 구문 트리(AST)로 변환합니다.

국소화(Localization): 시스템은 식별된 후보 신호를 특정 문장 수준의 AST 노드 및 이를 둘러싼 구조적 컨텍스트(예: always 블록, case 문)에 매핑합니다.
변환(Transformation): 두 번째 LLM인 **추상화 도구(Abstractor)**는 국소화된 AST 노드만을 재작성하는 임무를 수행합니다. 이 모델은 원본과 추상화된 문장의 예시를 제공하는 퓨샷 학습(Few-shot learning)을 사용하여 후보 추상화를 생성합니다.
제약 조건: LLM은 속성과 무관하다고 판단된 문장의 특정 부분만을 재작성하도록 제약됩니다(예: 속성이 ADD 연산에 대해서만 관심을 갖는 경우, AND 연산을 알 수 없는 값 X로 대체). 이때 관련 로직은 그대로 보존합니다.

3. 심볼릭 검증 및 정제 (심볼릭 구성 요소)

생성된 모든 추상화는 원래의 설계를 안전한 **과잉 근사(Over-approximation)**로 보장하도록 엄격하게 검증됩니다.

SMT 체크: 프레임워크는 만족 가능성 모듈 이론(SMT) 솔버(특히 Z3)를 사용하여 $\forall V, S(V) \implies \hat{S}(V)$ $\forall V, S (V) ⟹ \hat{S} (V)$ 조건을 검증합니다. 이는 추상화된 문장에서 허용되는 모든 동작이 원본 설계에서도 허용됨을 보장합니다.
- X-값 처리: SMT 솔버는 기본적으로 미정값(X)을 지원하지 않으므로, 이를 존재 양화사( $\exists Y$ )에 의해 구속된 새로운 변수로 변환하여 솔버가 이를 비결정론적 선택으로 처리할 수 있도록 합니다.
맞춤형 CEGAR 루프 (R-CEGAR): 추상 모델이 속성 증명에 실패하고 반례를 생성하면, 시스템은 해당 반례가 허위(spurious)인지 확인합니다.
- 만약 허위라면, 반례 축소(Counterexample reduction) 기술을 적용하여 트레이스를 일반화하고 어떤 추상화된 문장이 위반을 유발했는지 정확히 찾아냅니다.
- 시스템은 전체 추상화를 폐기하는 대신, 문제가 된 특정 문장만을 원본 형태로 되돌리고(revert) 반복 프로세스를 수행합니다.

주요 기여

LLM을 활용한 최초의 RTL 추상화 적용: 본 논문은 정적 규칙 기반 접근법을 넘어, RTL 추상화를 위해 LLM을 사용하는 최초의 프레임워크인 NeuroAbs를 소개합니다.
신경-심볼릭 워크플로우: 신경 구성 요소(LLM)가 시나리오 인지적 후보를 제안하고, 심볼릭 구성 요소(AST 순회 및 SMT)가 정밀한 구조적 타겟으로 재작성을 제한하며 정당성을 검증하는 새로운 흐름을 제안합니다.
맞춤형 정제 (R-CEGAR): 반례 축소를 사용하여 허위 반례를 일으키는 특정 추상화 문장만을 효율적으로 식별하고 되돌리는 정제 루프를 도입하여, 필요한 반복 횟수를 최소화합니다.

실험 결과

프레임워크는 RISC-V 프로세서 코어(PicoRV32, Piccolo, Flute) 및 I2C 주변 장치를 포함한 벤치마크 세트에서 평가되었으며, 총 55개의 검증 시나리오를 다루었습니다. 결과는 고급 추상화 메커니즘을 이미 포함하고 있는 최첨단 모델 체커(AVR 및 RIC3)와 비교되었습니다.

형식 증명 가속화: AVR과 통합되었을 때, NeuroAbs는 형식 증명 구축을 위한 평균 실행 시간을 44.89% 단축했습니다. AVR의 기존 추상화 능력에도 불구하고 NeuroAbs는 상당한 추가 가속을 제공했습니다.
버그 탐색 효율성 (BMC): 시간 제한 내에 형식 증명을 완료할 수 없는 경우, NeuroAbs는 유한 모델 체킹(BMC) 프로세스를 크게 가속화했습니다.
- "Piccolo" 케이스의 경우, 평균 언롤링 깊이(unrolling depth)가 109.36에서 125.36 사이클로 증가했습니다.
- "Flute" 케이스의 경우, 베이스라인의 최대 깊이에 도달하는 데 걸리는 시간이 75.98% 감소했습니다.
절제 연구(Ablation Studies): 실험을 통해 **퓨샷 학습(Few-shot learning)**과 **커스텀 지침(Custom instructions)**이 모두 매우 중요하다는 것이 확인되었습니다. 퓨샷 학습을 제거하면 과잉 근사율이 95.27%에서 83.51%로 떨어졌습니다. 커스텀 지침을 제거하면 "엄격한(strict)" 과잉 근사 비율이 98.38% 급감했습니다(즉, 모델이 추상화하기보다 원본 문장을 그대로 재현하는 경향을 보였습니다).
복잡도 감소: 결과물인 And-Inverter-Gate (AIG) 회로 분석 결과, 최대 변수 인덱스가 실질적으로 감소함을 보여주었으며, 이는 NeuroAbs가 회로 구조를 효과적으로 단순화함을 입증합니다.

의의 및 주장

본 논문은 NeuroAbs가 전통적인 규칙 기반 추상화의 경직성과 수동 방식의 높은 노동 집약도 문제를 해결한다고 주장합니다. LLM의 의미론적 추론 능력과 심볼릭 검증의 엄격함을 결합함으로써, NeuroAbs는 정적 규칙이 놓칠 수 있는 컨텍스트 특화된 추상화 기회를 식별할 수 있습니다.

저자들은 NeuroAbs를 기존 모델 체커를 대체하는 도구가 아니라, 그 효율성을 높여주는 보완적인 프레임워크로 정의합니다. 실험 결과는 고도로 최적화된 경쟁 모델 체커(AVR 및 RIC3)와 결합했을 때도 신경-심볼릭 접근 방식이 증명 구축 속도와 버그 탐색 깊이 모두에서 측정 가능한 개선을 가져온다는 것을 보여줍니다. 이 프레임워크는 전문가의 수동 개입 의존도를 낮추는, 보다 자동화되고 시나리오 인지적인 하드웨어 검증을 향한 단계로 제시됩니다.