AutoINV: Automated Invariant Generation Framework for Formal Verification on High-Level Synthesis Designs
이 논문은 고수준 합성(HLS)으로 생성된 RTL 설계의 검증 효율을 높이기 위해, HLS의 설계 특징을 활용한 보조 어설션(helper assertions)을 자동으로 생성하고 최적의 조합을 선택하여 모델 체킹 속도를 최대 6.05배까지 가속화하는 프레임워크인 AutoINV를 제안합니다.
요즘 반도체나 하드웨어를 만들 때, 사람이 일일이 설계도를 그리는 대신 **HLS(고수준 합성)**라는 도구를 사용합니다. 이건 마치 **"레시피(C/C++ 코드)만 넣으면 자동으로 요리(하드웨어 설계도)를 만들어주는 마법의 기계"**와 같습니다.
하지만 문제가 하나 있습니다. 이 기계가 만든 설계도는 사람이 직접 그린 것보다 엄청나게 복잡하고 거대합니다. 마치 수만 개의 갈림길이 있는 거대한 미로와 같죠. 이 미로에 오류(버그)가 없는지 확인하려면 **'모델 체킹(Model Checking)'**이라는 수학적 검증 과정을 거쳐야 하는데, 미로가 너무 복잡하다 보니 검증 컴퓨터가 길을 찾다가 지쳐서 포기해버리는(시간 초과) 일이 빈번합니다.
2. 핵심 아이디어: "미로 탐험가를 위한 '치트키'와 '내비게이션'"
연구팀은 이 문제를 해결하기 위해 AutoINV라는 시스템을 만들었습니다. 이 시스템은 미로 탐험가(검증 알고리즘)에게 두 가지 도움을 줍니다.
① 똑똑한 힌트 생성 (Helper Generation)
탐험가가 미로를 헤맬 때, "이 길은 막다른 길이야" 혹은 "이쪽으로 가면 반드시 보물이 나와" 같은 **힌트(Helper Assertions)**를 미리 주는 것입니다.
하드웨어 패턴 분석: 설계도가 만들어지는 규칙(예: 데이터가 쌓이는 창고, 순차적으로 움직이는 컨베이어 벨트 등)을 분석해서 "창고가 꽉 차면 더 이상 물건을 넣을 수 없다" 같은 상식적인 힌트를 자동으로 만들어냅니다.
소프트웨어 규칙 활용: 원래 레시피(코드)에 적혀 있던 순서(예: 1번 재료를 넣고 나서 2번을 넣는다)를 바탕으로 힌트를 만듭니다.
② 효율적인 힌트 선별 (Helper Ranking)
힌트가 너무 많으면 오히려 헷갈릴 수 있습니다. (마치 길 안내를 해준다고 수만 명의 사람이 동시에 소리를 지르는 것과 같죠.)
AutoINV는 탐험가가 미로를 헤매다가 **어디서 가장 많이 막히는지(CTI)**를 관찰합니다.
그리고 **"아, 탐험가가 지금 이 구역에서 헤매고 있구나! 그럼 이 구역에 딱 맞는 힌트를 줘야겠다!"**라고 판단하여, 가장 효과적인 힌트만 골라서 전달합니다.
3. 결과: "엄청난 속도 향상"
이 시스템을 실제 복잡한 설계도에 적용해 보았더니 놀라운 결과가 나왔습니다.
속도 업그레이드: 기존 방식보다 평균적으로 2.23배, 빠를 때는 무려 6배 이상 빠르게 검증을 끝냈습니다.
불가능을 가능으로: 기존 방식으로는 시간이 너무 오래 걸려 "결과를 알 수 없음(Unknown)"이라고 나왔던 아주 복잡한 설계도도, AutoINV는 힌트를 활용해 **"오류 없음(Proof)"**이라는 결론을 완벽하게 찾아냈습니다.
요약하자면!
AutoINV는 **"너무 복잡해서 길을 잃기 쉬운 하드웨어 설계도라는 미로 속에서, 탐험가가 길을 잃지 않도록 설계 규칙을 바탕으로 '가장 필요한 순간에 딱 맞는 힌트'를 던져주는 똑똑한 내비게이션"**이라고 할 수 있습니다. 이 덕분에 반도체 설계의 오류를 훨씬 빠르고 정확하게 잡아낼 수 있게 된 것입니다.
[기술 요약] AutoINV: HLS 설계의 형식 검증을 위한 자동 불변량 생성 프레임워크
1. 문제 정의 (Problem Statement)
HLS의 한계: 고수준 합성(High-Level Synthesis, HLS)은 C/C++ 코드를 RTL(Register-Transfer Level)로 자동 변환하여 설계 시간을 단축시키지만, 변환 과정에서 도구의 오류나 한계로 인해 기능적 버그나 보안 취약점이 발생할 수 있습니다.
검증의 어려움: 이를 해결하기 위해 모델 체킹(Model Checking)과 같은 형식 검증(Formal Verification)이 사용되지만, HLS로 생성된 RTL은 설계 규모가 매우 크고 복잡하여 상태 공간 폭발(State Space Explosion) 문제로 인해 검증 시간이 기하급수적으로 늘어나는 한계가 있습니다.
기존 방식의 문제: 수동으로 보조 어설션(Helper Assertions)을 작성하는 것은 대규모 HLS 설계에서는 불가능에 가까우며, 기존의 자동 생성 방식들은 HLS 특유의 구조적 패턴을 반영하지 못하거나 검증 속도 향상보다는 커버리지 확보에 치중되어 있습니다.
2. 제안 방법론 (Methodology: AutoINV Framework)
본 논문은 모델 체커(IC3/PDR 알고리즘)를 가이드하여 검증 속도를 가속화하기 위해, HLS 설계의 특징을 활용한 보조 어설션(Helper Assertions) 자동 생성 및 선택 프레임워크인 AutoINV를 제안합니다.
AutoINV는 세 가지 핵심 모듈로 구성됩니다:
AutoINV Helper Generator (보조 어설션 생성기):
HLS 설계에서 반복적으로 나타나는 하드웨어 및 소프트웨어 패턴을 분석하여 고품질의 보조 어설션을 추출합니다.
하드웨어 관련(HW-GEN): FIFO(포인터 및 상태 제어), FSM(One-hot 인코딩 제약), Pipeline(단계별 활성화 및 종료 조건의 순차적 특성) 패턴을 규칙 기반으로 추출합니다.
소프트웨어 관련(SW-GEN): C++ 코드의 실행 순서를 반영합니다. 루프 간의 실행 순서(Loop-level), 함수 간의 호출 순서(Function-level), 그리고 루프 변수의 범위(Loop variable) 제약 조건을 활용합니다.
AutoINV Helper Ranker (보조 어설션 순위 지정기):
생성된 수많은 보조 어설션 중 어떤 것이 검증에 가장 도움이 될지 결정합니다.
CTI(Counterexample to Induction) 기반 평가: 이전 검증 시도에서 발생한 CTI(유도 반례) 정보를 분석합니다. 특정 변수가 CTI에서 자주 등장한다면, 해당 변수를 제약하는 보조 어설션이 검증 속도를 높일 가능성이 크다고 판단하여 높은 점수를 부여합니다.
AutoINV Prover (보조 어설션 증명기):
Ranker가 선정한 최적의 보조 어설션을 반복적으로 가져와 검증합니다.
Clause Side-loading 기술: 증명된 보조 어설션으로부터 얻은 불변량(Invariant)의 절(Clause)들을 타겟 속성(Target Property) 검증 시 초기 제약 조건으로 주입(Side-loading)하여, 모델 체커가 더 효율적인 방향으로 탐색하도록 유도합니다.
3. 주요 기여 (Key Contributions)
HLS 특화 패턴 추출: 템플릿에 의존하지 않고 HLS 설계의 구조적/행동적 패턴을 활용한 자동화된 보조 어설션 생성 기법을 개발했습니다.
동적 헬퍼 선택 메커니즘: 블랙박스 방식(예: 딥러닝)과 달리, 검증 과정에서 발생하는 실시간 데이터(CTI 통계)를 활용하여 검증 오버헤드를 최소화하면서도 가장 유망한 보조 어설션을 선택하는 메커니즘을 구축했습니다.
검증 가속화 프레임워크 구축: HLS 설계의 대규모 RTL 검증 문제를 해결할 수 있는 통합 프레임워크를 제안하고 실효성을 입증했습니다.
4. 실험 결과 (Results)
벤치마크: 다양한 규모의 HLS 설계(vac-e, vsc-e, mac-e 및 대규모 AutoSA 설계)를 대상으로 실험을 진행했습니다.
성능 향상:
일반적인 모델 체킹(Vanilla Model Checking) 대비 평균 2.23배의 속도 향상을 달성했습니다.
특정 벤치마크에서는 최대 6.05배의 속도 향상을 기록했습니다.
대규모 설계인 autosa-mm-f에서는 4.76배의 속도 향상과 함께 FIFO 풀(Full) 상태를 유발하는 카운터예제(Cex)를 성공적으로 찾아냈습니다.
기존 방식으로는 시간 초과(O.O.T.)로 판별할 수 없었던 autosa-cnn-f 설계에 대해 성공적으로 증명(Proof)을 완료했습니다.
5. 의의 (Significance)
본 연구는 HLS를 이용한 현대적 하드웨어 설계 흐름에서 필수적인 '설계 자동화'와 '검증 신뢰성' 사이의 간극을 메우는 중요한 기술적 진보를 보여줍니다. 특히, 사람이 직접 개입하기 어려운 대규모 RTL 설계에 대해 수학적 엄밀성을 유지하면서도 실용적인 시간 내에 검증을 완료할 수 있는 자동화된 경로를 제시했다는 점에서 학술적/산업적 가치가 높습니다.