서문 ... 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<NOBR><?import namespace ... m ur 9 1.4 공평성 제한조건 ... 481 9 1.5 CTL, CT<m:math xmlns ... '"htt 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