Formal Verification¶
✅
Formal Verification
Formal — SVA, JasperGold, 정형 증명 전략
🎯 학습 목표¶
- Distinguish (분석) Formal Verification과 Simulation의 본질적 차이(증명 vs 샘플)와 각 기법이 잡을 수 있는 버그 종류 구분
- Implement (생성) SVA(System Verilog Assertion)를 사용한 안전성·라이브니스 프로퍼티 작성
- Apply (적용) JasperGold App(JG-Apex/Functional/CDC/Coverage)을 시나리오에 맞게 적용
- Diagnose (분석) BOUNDED → PROVEN 수렴 전략 (Cut Point, Blackbox, Assume, Abstraction)
- Critique (평가) Vacuous Pass / Over-constraint 같은 흔한 함정 식별
📋 사전 지식¶
다음 항목을 알고 있어야 본문이 매끄럽게 읽힙니다:
- SystemVerilog: class, module, interface (IEEE 1800)
- 시뮬레이션 기반 검증 경험 (UVM 또는 directed test)
- 명제 논리 기본: implication (
->), 양화사 (∀, ∃) 개념 - DUT 사양 문서 읽고 protocol 규칙을 추출하는 능력
🗺️ 개념 맵¶
개념 의존성 — 순서대로 학습 권장
각 노드 = 모듈 (클릭하여 이동) · 화살표(→) = 선수 지식 흐름
📚 학습 모듈¶
01
Unit 1: Formal Verification 기본 개념
02
SVA (SystemVerilog Assertions)
03
JasperGold & DV Strategy
★
Quick Reference Card
📊 모듈 흐름¶
M01
Fundamentals
▶
M02
SVA
▶
M03
JasperGold & Strategy
▶
M04
Quick Ref
📖 관련 자료¶
- 📚 용어집 (Glossary) — Formal 핵심 용어 ISO 11179 형식
- 📝 퀴즈 (Quizzes) — 챕터별 5문항 (Bloom mix)
- 📋 코스 개요 & 컨셉 맵 — 학습 단위와 사용처
💡 학습 팁¶
효율적 학습
- Sim 사고에서 벗어나기: Formal은 "내가 생각한 시나리오 + 모든 시나리오"가 대상. 입력을 한정하지 말고 spec rule만 코드로 옮기기
- PROVEN ≠ 충분한 검증: PROVEN이라도 SVA 자체가 잘못되었거나 너무 약하면 의미 없음. Coverage + 다른 검증과 조합
- Vacuous Pass 의심: SVA가 너무 쉽게 PROVEN되면 antecedent가 false인지 항상 확인
흔한 함정
- Over-constraint: assume이 너무 강해 실제 DUT 입력 공간을 좁힘 → false PROVEN
- Vacuous pass: implication의 LHS가 false → 항상 true → 의미 없는 PROVEN
- Blackbox 후 sign-off: 블랙박스된 영역의 동작을 검증한 게 아님을 명시