ConnChecker: Automated Root-Cause Analysis for Formal Connectivity Check via Graph

ConnChecker 는 포멀 연결성 검증에서 생성된 카운터예제와 의존성 그래프를 통합하여 실패 원인을 자동으로 분류 및 분석함으로써 SoC 설계의 디버깅 시간을 최대 80% 단축하는 자동화된 루트-카즈 분석 도구입니다.

핵심

🏙️ 배경: 거대한 도시의 도로망 (반도체 칩)

상상해 보세요. 우리가 사는 도시가 거대한 반도체 칩이라고 합시다.

• 신호 (Signal) = 자동차
• 연결선 (Connection) = 도로
• 설계자 (Engineer) = 교통 관리관

이 도시에는 수만 개의 도로가 있고, A 지점에서 B 지점으로 차가 잘 갈 수 있어야 합니다. 하지만 설계가 복잡해지면, "어? 이 도로가 끊겨 있네?", "왜 차가 여기서 멈추지?" 같은 문제가 생깁니다.

🚨 문제: 사고 수습은 왜 이렇게 힘들까?

기존에는 교통 관리관 (엔지니어) 이 직접 지도를 펼쳐 들고, "어디서부터 끊겼지?"라고 하나하나 찾아다녔습니다.

• 문제점: 도시가 너무 크고 복잡해서, 사고가 나면 수습하는 데 시간이 너무 오래 걸립니다. 연구에 따르면, 엔지니어들은 일하는 시간의 거의 절반 (약 47%) 을 이런 '사고 수습 (디버깅)'에 보낸다고 합니다.
• 현실: "여기 도로가 끊겼어요"라는 보고서 (Counterexample) 는 받지만, 왜 끊겼는지, 어디서부터 고쳐야 할지는 사람이 직접 찾아야 했습니다.

🚀 해결책: ConnChecker (스마트 교통 관제 시스템)

이때 등장한 것이 ConnChecker입니다. 이는 단순히 사고를 알려주는 게 아니라, 사고 원인을 자동으로 분석하고 해결책을 제안하는 AI 교통 관제 시스템입니다.

ConnChecker 는 사고 보고서를 받자마자 3 가지 상황으로 나누어 자동으로 처리합니다.

1️⃣ 상황 A: "도로는 있는데, 차가 안 가요" (기능적/구조적 연결 존재)

• 비유: 도로가 잘 깔려 있는데, 신호등이 고장 나거나 교통정리가 안 돼서 차가 못 가는 경우입니다.
• ConnChecker 의 역할:
  • 도로 구간을 작은 블록으로 쪼개서 하나하나 검사합니다.
  • "여기 신호등이 고장 났네?", "여기 도로가 막혀있네?"라고 정확한 고장 지점을 찾아냅니다.
  • 효과: 사람이 수천 개의 도로를 일일이 확인할 필요 없이, 고장 난 구간만 딱 집어서 알려줍니다.

2️⃣ 상황 B: "도로 자체가 아예 없어요" (구조적 연결 부재)

• 비유: 지도에는 A 에서 B 로 가는 길이 그려져 있는데, 실제로는 도로가 아예 연결되지 않은 경우입니다.
• ConnChecker 의 역할:
  • 목적지 (B) 에서 출발해서 거꾸로 뒤따라가며 (Fan-in 분석) "누가 이 도로를 만들어야 했지?"라고 추적합니다.
  • "아! 여기 도로를 연결해야 할 '공급자 (Driver)'가 아예 없네!"라고 누가 연결을 안 했는지 찾아냅니다.
  • 효과: "어디서부터 시작해야 하지?"라는 막막함을 없애고, 연결이 끊긴 시작점을 바로 찾아줍니다.

3️⃣ 상황 C: "도로는 있는데, 차가 지나갈 수 없는 규칙이 있어요" (구조적 연결만 존재)

• 비유: 도로는 있는데, "이 길은 밤에만 통행 가능" 같은 복잡한 규칙 (제약 조건) 때문에 차가 못 가는 경우입니다.
• ConnChecker 의 역할:
  • "왜 차가 못 가는지" 그 **규칙 (제약 조건)**을 찾아내어 설명해 줍니다.
  • "아, 이 신호가 0 으로 고정되어 있어서 차가 못 지나가는 구나"라고 원인을 명확히 합니다.

📊 결과: 얼마나 빨라졌을까?

이 도구를 실제 자동차용 칩 (라다 센서, 자동차용 마이크로컨트롤러) 에 적용해 봤습니다.

• 단순한 사고: 기존 방법과 비슷하게 빠릅니다.
• 복잡한 사고 (여러 신호가 섞이거나, 시계가 다른 경우): 최대 80% 까지 시간이 단축되었습니다!
  • 예: 사람이 30 분 걸려서 찾던 문제를 ConnChecker 는 5 분 만에 해결했습니다.
  • 특히 도로가 복잡하게 얽힌 '혼합 신호'나 '여러 시계 영역'이 섞인 경우, ConnChecker 의 효과가 빛을 발했습니다.

💡 핵심 요약 (일상 언어로)

1. 기존 방식: "여기 차가 안 가요"라는 보고서를 받고, 엔지니어가 수백 개의 도로를 직접 걸어 다니며 고장 난 곳을 찾는 것. (매우 힘듦, 시간 걸림)
2. ConnChecker 방식: "여기 차가 안 가요"라는 보고서를 받자마자, AI 가 모든 도로를 스캔해서 "고장 난 곳은 3 번 도로의 5 번째 신호등입니다"라고 정확히 알려주는 것. (매우 빠름, 효율적)

🌟 결론

이 논문은 **"복잡한 반도체 설계에서 연결 오류를 찾는 일을, 사람이 직접 하는 수작업에서 AI 가 자동으로 분석하는 시스템으로 바꿈으로써, 개발 시간을 획기적으로 줄였다"**는 것을 증명합니다.

마치 교통 사고 수습을 위해 경찰이 직접 도시 전체를 돌아다니는 대신, 스마트 관제 시스템이 CCTV 를 통해 사고 지점을 즉시 찾아내어 수습 시간을 단축하는 것과 같은 원리입니다. 이를 통해 반도체 칩을 더 빨리, 더 안전하게 만들 수 있게 되었습니다.

기술 요약

ConnChecker: 그래프 기반 형식 연결성 검사 (Formal Connectivity Check) 를 위한 자동화된 루트-원인 분석

1. 문제 정의 (Problem)

• 배경: SoC(시스템 온 칩) 설계에서 신호 경로와 상호 연결을 검증하는 '형식 연결성 검사 (Formal Connectivity Check)'는 확장성이 뛰어나지만, 검증 실패 시 생성되는 반대 예제 (Counterexample, CEX) 를 디버깅하는 과정은 여전히 수동적이고 시간이 많이 소요됩니다.
• 현황: 2024 년 Wilson Research Group 보고서에 따르면 엔지니어는 전체 기능 검증 시간의 약 47% 를 디버깅에 할애하고 있습니다.
• 핵심 문제: Cadence JasperGold 와 같은 형식 검증 도구를 사용할 때, 연결성 실패가 발생하면 엔지니어는 수동으로 원인을 추적해야 합니다. 설계 복잡도가 증가함에 따라 이 과정은 비효율적이며, 이를 해결할 수 있는 자동화된 루트-원인 분석 (RCA) 솔루션이 부재했습니다.

2. 제안된 방법론 (Methodology)

ConnChecker 는 JasperGold 의 구조적/기능적 의존성 그래프 (Dependency Graph) 와 CEX 보고서를 통합하여 그래프 기반의 자동화된 분석 프레임워크를 제시합니다.

• 기본 모델: DUT(검증 대상 설계) 를 방향성 의존성 그래프 $G=(V, E)$로 모델링합니다. 여기서 노드는 신호/핀/변수를, 에지는 직접적인 의존성 또는 구조적 연결을 나타냅니다.

• 실패 유형 자동 분류 (Failure Categorization): CEX 를 분석하여 다음 3 가지 유형 중 하나로 자동 분류한 후, 각각에 맞는 전용 분석 플로우를 적용합니다.

  1. 유형 1 (기능적 및 구조적 연결 존재): 경로가 존재하지만 연결성 검사에 실패한 경우 (잘못된 연결 맵, RTL 버그, 누락된 제약 조건 등).
  2. 유형 2 (구조적 연결 부재): 소스 (Source) 에서 목적지 (Destination) 로 가는 구조적 경로 자체가 존재하지 않는 경우.
  3. 유형 3 (구조적 연결만 존재): 경로는 존재하지만 신호 전파가 차단된 경우 (과도한 제약 조건, 비활성화된 논리 등).

• 핵심 분석 엔진 (Core Debug Engine):

  • Flow 1 (기능적/구조적 연결): 그래프를 작은 세그먼트로 분해하고, 각 에지에 대해 원자적 (atomic) 인 연결성 어설션 (assertion) 을 생성하여 재검증합니다. JasperGold 의 '역방향 연결성 검사 (Reverse Connectivity Check)'를 세그먼트 단위로 적용하여 실패 지점을 정밀하게 국소화합니다.
  • Flow 2 (구조적 연결 부재): 팬인 (Fan-in) 분석을 사용합니다. 목적지 신호에서 역방향으로 추적하여 영향을 미치는 모든 신호를 식별하고, 클럭/리셋/상위 입력 등을 필터링하여 '루트 드라이버 (Root Drivers)'를 찾습니다. 이를 통해 끊어진 연결이나 누락된 드라이버를 식별합니다.
  • Flow 3 (구조적 연결만 존재): 분할 정복 (Divide-and-Conquer) 전략을 사용하여 구조적 경로를 세그먼트화하고, JasperGold 의 '과도 제약 (Over-constraint)' 분석 기법을 활용하여 기능적 연결이 차단된 원인을 규명합니다.

3. 주요 기여 (Key Contributions)

1. 자동화된 연결성 검사 관점의 전환: 수동 디버깅을 3 가지 자동화된 분석 플로우로 변환하여 확장 가능하고 그래프 기반의 프로세스로 재정의했습니다.
2. 원자적 연결성 검사 자동 생성: 의존성 그래프의 각 세그먼트에 대해 타겟팅된 어설션을 자동 생성하여, 최소한의 수동 개입으로 정확한 루트-원인을 위치시킵니다.
3. 목적지 신호의 영향력 (Cone of Influence) 팬인 분석: 연결이 없는 경우를 위해 상향식 (Upstream) 의존성을 추적하여 누락된 드라이버와 끊어진 세그먼트를 식별하는 구조적 디버깅 프로세스를 정립했습니다.

4. 실험 결과 (Results)

인피니온 (Infineon) 의 두 가지 산업용 SoC 설계 (60GHz 레이더 센서 및 자동차용 마이크로컨트롤러) 를 대상으로 ConnChecker 를 평가했습니다.

• 성능 향상:
  • Flow 1 & 2: 복잡한 경우 (혼합 신호, 멀티 클럭 도메인 등) 에 수동 디버깅 대비 최대 5 배 이상 (약 80% 시간 단축) 의 속도 향상을 보였습니다. 예를 들어, 30 분이 걸리던 복잡한 사례가 약 5 분으로 단축되었습니다.
  • Flow 3: 단순 연결에서는 차이가 적었으나, 40~50 개의 에지를 가진 복잡한 마이크로컨트롤러 경로에서는 약 80% 의 시간 절감을 달성했습니다.
• 확장성: 연결 복잡도 (에지 수, 멀티 클럭, 혼합 신호 등) 가 증가할수록 ConnChecker 의 처리 시간은 거의 일정하게 유지되는 반면, 수동 디버깅 시간은 급격히 증가하는 경향을 보였습니다.
• 특수 케이스 대응:
  • 혼합 신호 (Mixed-Signal): 여러 경로가 존재할 때 후보 경로를 모두 분석하여 엔지니어에게 제시함으로써 추적성을 높였습니다.
  • 멀티 클럭 도메인: 세그먼트 단위 분석을 통해 클럭 제어 관계를 명확히 파악하여 도메인 간 연결성 문제를 효율적으로 해결했습니다.

5. 의의 및 결론 (Significance)

• 산업적 가치: 형식 검증 워크플로우에서 가장 시간 소모적인 '디버깅' 단계를 자동화함으로써, SoC 검증의 생산성을 획기적으로 높이고 Time-to-Market 을 단축할 수 있습니다.
• 기술적 혁신: 기존에 수동으로 수행되던 복잡한 연결성 문제 해결을 체계적인 그래프 기반 알고리즘으로 전환하여, 특히 대규모 SoC 설계에서의 확장성을 입증했습니다.
• 향후 과제: 현재는 버스 (Bus) 연결 처리 시 모든 비트를 개별적으로 분석하는 비효율이 존재하며, 다중 경로 상황에서의 최적 경로 선택 알고리즘이 필요합니다. 하지만 ConnChecker 는 형식 연결성 검증 자동화의 중요한 기반을 마련했다는 점에서 의의가 큽니다.

이 논문은 형식 검증 도구 (JasperGold) 의 출력물을 활용하여 루트-원인 분석을 자동화하는 첫 번째 체계적인 접근법 중 하나로, 복잡한 반도체 설계 검증의 효율성을 크게 개선할 수 있는 솔루션을 제시합니다.