서문 = 9
감사의 글 = 14
저자에 대하여 = 15
1장 설계 검증으로 초대 = 1
1.1 설계 검증이란 무엇인가? = 2
1.2 기본 검증 원리 = 4
1.3 검증 방법론 = 7
1.3.1 시뮬레이션 기반 검증 = 8
1.3.2 공식적 방법 기반 검증 = 11
1.4 시뮬레이션 기반 검증 대 공식적 검증 = 14
1.5 공식적 검증의 제한 = 16
1.6 Verilog 스케줄링과 실행 의미의 개요 = 16
1.6.1 동시 프로세스 = 16
1.6.2 비결정성(Nondeterminism) = 18
1.6.3 스케줄링 의미 = 20
1.7 요약 = 21
2장 검증을 위한 코딩 = 39
2.1 기능적 정확성 = 41
2.1 1 구문 검사(syntactical checks) = 42
2.1.2 구조 검사 = 50
2.2 타이밍 정확성 = 53
2.2.1 레이스 문제(Race problem) = 53
2.2.2 클록 게이팅(Clock Gating) = 55
2.2.3 시간 0과 0 시간 글리치 = 56
2.2.4 도메인간 글리치 = 57
2.3 시뮬레이션 성능 = 58
2.3.1 상위 레벨 추상 = 58
2.3.2 시뮬레이터 인식가능 요소 = 60
2.3.3 벡터 대 스칼라 = 62
2.3.4 다른 시뮬레이션 시스템에 대한 인터페이스의 최소화 = 65
2.3.5 하위 레벨／요소 레벨 최적화 = 66
2.3.6 코드 프로파일링 = 66
2.4 이식성 및 유지보수성 = 67
2.4.1 프로젝트 코드 레이아웃 = 67
2.4.2 중앙집중 자원 = 68
2.4.3 RTL 설계 파일 형식 = 69
2.5 "합성가능성" "디버그 가능성" 및 일반 도구 호환성 = 70
2.5.1 합성가능성 = 71
2.5.2 디버그 가능성 = 71
2.6 주기 기반 시뮬레이션 = 73
2.7 하드웨어 시뮬레이션／에뮬레이션 = 76
2.8. 2상 및 4상 시뮬레이션(Two-state and Four-state simulation) = 78
2.9 설계 및 린터의 이용 = 80
2.10 요약 = 80
2.11 연습문제 = 81
3장 시뮬레이터 구조 및 동작 = 87
3.1 컴파일러 = 89
3.2 시뮬레이터 = 93
3.2.1 이벤트 반응 시뮬레이터(Event-Driven Simulator) = 93
3.2.2 주기 기반 시뮬레이터 = 101
3.2.3 하이브리드 시뮬레이터 = 114
3.2.4 하드웨어 시뮬레이터와 에뮬레이터 = 118
3.3 시뮬레이터 분류 및 비교 = 120
3.3.1. 2상 및 4상 시뮬레이터 = 121
3.3.2. 0 지연 대 단위 지연 시뮬레이터 = 122
3.3.3 이벤트 반응 대 주기 기반 시뮬레이터 = 123
3.3.4 인터프리트 대 컴파일 시뮬레이터 = 133
3.3.5 하드웨어 시뮬레이터 = 123
3.4 시뮬레이터 동작 및 응용 = 124
3.4.1 기본 시뮬레이션 파일 구조 = 125
3.4.2 성능과 디버깅 = 126
3.4.3 타이밍 검증 = 129
3.4.4 설계 프로파일링(Design Profiling) = 133
3.4.5. 2상과 4상(Two-State and Four-State) = 134
3.4.6 캡슐화된 모델과의 코시뮬레이션 = 136
3.5 점진적 컴파일 = 137
3.6 시뮬레이터 콘솔 = 138
3.7 요약 = 139
3.8 연습문제 = 140
4장 검사 벤치 구성 및 설계 = 149
4.1 검사 벤치와 검사 환경의 해부학 = 150
4.2 초기화 메커니즘 = 154
4.2.1 RTL 초기화 = 155
4.2.2 PLI 초기화 = 157
4.2.3 시간 0에서의 초기화 = 159
4.3 클록 생성 및 동기화 = 159
4.3.1 명시적 및 토글 방법 = 160
4.3.2 절대 천이 지연(Absolute Transition Delay) = 161
4.3.3 시간 0 클록 천이 = 162
4.3.4 시간 단위 및 해상도 = 162
4.3.5 클록 곱셈기 및 나눗셈기 = 162
4.3.5 클록 독립성 및 지터(Jitter) = 164
4.3.7 클록 동기화 및 델타 지연 = 165
4.3.8 클록 생성기 구성 = 166
4.4 자극 생성 = 167
4.4.1 비동기 자극 응용 = 171
4.4.2 명령 코드 또는 프로그램된 자극 = 172
4.5 응답 평가(Response Assessment) = 173
4.5.1 설계 상태 덤프 = 173
4.5.2 최적 응답(Golden response) = 178
4.5.3 임시 규격 검사 = 188
4.6 검증 유틸리티 = 192
4.6.1 오류 주사기(Error Injector) = 194
4.6.2 오류 및 경고 알림 메커니즘 = 195
4.6.3 메모리 로드 및 덤프 메커니즘 = 196
4.6.4 스파스 메모리와 내용 주소지정가능 메모리(CAM) = 200
4.6.5 어설션 루틴(Assertion Routines) = 204
4.7 검사 벤치-설계 인터페이스 = 204
4.8 공통 실무 기술 및 방법론 = 205
4.8.1 검증 환경 구성 = 205
4.8.2 버스 기능 모델 = 208
4.9 요약 = 212
4.10 연습문제 = 213
5장 검사 시나리오, 어설션 및 적용범위 = 219
5.1 계층적 검증 = 222
5.1 1 시스템 레벨 = 222
5.1.2 장치 레벨 = 224
5.1.3 모듈 레벨 = 224
5.2 검사 계획 = 224
5.2.1 구조적 규격으로부터 기능을 추출 = 225
5.2.2 기능을 우선순위화 = 229
5.2.3 검사 사례를 생성 = 230
5.2.4 진행과정을 추적 = 230
5.3 의사난수 검사 생성기 = 233
5.3.1 사용자 인터페이스 = 235
5.3.2 레지스터와 메모리 할당 = 236
5.3.3 프로그램 구조 = 236
5.3.4 자가 검사 메커니즘 = 236
5.4 어설션(Assertion) = 238
5.4.1 어설션을 위해 무엇을 정의하는가 = 238
5.4.2 어설션 요소 = 239
5.4.3 어설션 작성 = 240
5.4.4 내장 상용 어설션(Built-in Commercial Assertions) = 252
5.5 System Verilog 어설션 = 253
5.5.1 즉시 어설션(Immediate Assertions) = 254
5.5.2 동시 어설션(Concurrent Assertions) = 254
5.6 검증 적용범위 = 264
5.6.1 코드 범위 = 266
5.6.2 파라미터 범위 = 274
5.6.3 기능 범위 = 276
5.6.4 항목 범위 및 교차 범위 = 282
5.7 요약 = 283
5.8 연습문제 = 283
6장 디버깅 프로세스 및 검증 주기 = 293
6.1 실패 캡쳐, 범위 축소 및 버그 추적 = 294
6.1.1 실패 캡쳐 = 294
6.1.2 범위 축소 = 295
6.1.3 오류 추적 시스템 = 300
6.2 시뮬레이션 데이터 덤프 = 302
6.2.1 공간적 이웃(Spatial Neighborhood) = 303
6.2.2 임시 창(Temporal Window) = 303
6.3 근본적인 원인들의 격리 = 305
6.3.1 참조 값, 전파 및 분기(Bifurcation) = 305
6.3.2 순방향 및 역방향 디버깅 = 306
6.3.3 추적 다이어그램 = 307
6.3.4 시간 프레임 = 309
6.3.5 로드, 드라이버, 콘 추적 = 310
6.3.6 메모리 및 배열 추적 = 313
6.3.7. 0 시간 루프 구조 = 314
6.3.8 설계에 대한 4가지 기본 관점 = 315
6.3.9 전형적인 디버거 기능 = 316
6.4 설계 갱신 및 유지보수: 개정 제어 = 320
6.5 회귀, 릴리즈 메커니즘 및 테이프 아웃 기준 = 322
6.6 요약 = 324
6.7 연습문제 = 325
7장 공식 검증 전제조건 = 337
7.1 집합과 연산 = 338
7.2 관계, 분할, 부분적으로 순서화된 집합 및 래티스 = 340
7.3 불리언 함수 및 표현 = 348
7.3.1 대칭적 불리언 함수 = 352
7.3.2 불완전하게 규정된 불리언 함수 = 355
7.3.3 특성 함수 = 356
7.4 불리언 함수 연산자 = 359
7.5 유한 상태 오토마타 및 언어 = 364
7.5.1 곱 오토마타 및 머신 = 367
7.5.2 상태 등가 및 머신 최소화 = 369
7.5.3 FSM 등가 = 373
7.5.4 그래프 알고리즘 = 375
7.5.5 깊이 우선 조사(Depth-First Search) = 377
7.5.6 너비 우선 조사(Branch-First Search) = 380
7.6 요약 = 382
7.7 연습문제 = 384
8장 결정 다이어그램, 등가 검사 및 기호 시뮬레이션 = 391
8.1 이진 결정 다이어그램 (Binary Decision Diagram) = 393
8.1.1 BDD에 대한 연산 = 398
8.1.2 변수 순서화(variable ordering) = 407
8.2 결정 다이어그램 변형들 = 414
8.2.1 공유 BDD(Shared BDD, SBDD) = 414
8.2.2 에지 속성 BDD(Edge-Attribute BDD) = 414
8.2.3. 0-억제 BDD(Zero-Suppressed BDD, ZBDD) = 416
8.2.4 순서화된 함수 결정 다이어그램(Ordered Functional Decision Diagram, OFDD) = 418
8.2.5 의사 불리언 함수(Pseudo Boolean Function)와 결정 다이어그램 = 421
8.2.6 이진 모멘트 다이어그램(Binary Moment Diagram) = 424
8.3 결정 다이어그램 기반 등가 검사(Equivalence checking) = 425
8.3.1 노드 사상과 제한(Node Mapping and Constraining) = 427
8.4 불리언 만족성(Boolean Satisfiability) = 431
8.4.1 분해 알고리즘(Resolvent Algorithm) = 432
8.4.2 검색 기반 알고리즘(Search-based Algorithm) = 435
8.4.3 내포 그래프 및 학습(Implication Graph and Learning) = 439
8.5 기호 시뮬레이션 = 443
8.5.1 기호 검증(Symbolic Verification) = 447
8.5.2 입력 제한 = 447
8.5.3 특성 함수를 이용한 기호 시뮬레이션 = 451
8.5.4 파라미터화(Parameterization) = 453
8.6 요약 = 456
8.7 연습문제 = 457
9장 모델 검사와 기호 연산 = 465
9.1 특성 규격 및 논리 = 466
9.1 1 오토마타를 사용한 순차적인 규격 = 467
9.1.2 일시적 구조와 연산 트리(tree) = 469
9.1.3 명제 임시 논리 (Propositional Temporal Logic) : LT L* , CTL 그리고 CTL = 474
9 1.4 공평성 제한조건 = 481
9 1.5 CTL, CT L* 및 LTL의 상대적인 표현성 = 482
9.1.6 SystemVerilog 어설션 언어 = 483
9.2 특성 검사 = 483
9.2.1 오토마타를 이용한 특성 규격 = 483
9.2.2 언어 포함(Language Containment) = 485
9.2.3 CTL 식 검사하기 = 488
9.2.4 공평성 제한조건을 가진 검사 = 491
9.3 기호 연산과 모델 검사 = 493
9.3.1 기호적인 FSM 표현과 상태 순례 = 493
9.3.2 반례(counterexample) 생성 = 499
9.3.3 등가성 검사 = 500
9.3.4 언어 포함과 공평성 제한조건 = 504
9.4 기호 CTL 모델 검사 = 511
9.4.1 고정점 연산 = 511
9.4.2 공평성 제한사항을 가지는 CTL 검증 = 518
9.5 연산의 개선점 = 521
9.5.1 조기 정량화(early quantification) = 522
9.5.2 일반화된 공통인수 = 525
9.6 모델 검사 도구의 사용 = 527
9.7 요약 = 528
9.8 연습문제 = 529
인용문헌 = 535
