RTL 의도를 검증 가능한 넷리스트로 만들기

입력

• 엘라보레이션된 RTL, 최상위 모듈, 리셋·클록 의도
• Liberty 타이밍·전력 뷰와 기술 매핑 규칙
• 버전 관리되는 SDC와 모드·코너 가정

작업

• 릴리스 대상 RTL을 lint·엘라보레이션하고 최적화 전에 파라미터, 블랙박스, 생성 클록을 기록합니다.
• 인터페이스 의도에서 SDC를 작성합니다. 클록, 생성 클록, I/O 지연, 불확실성 및 검토된 예외만 포함합니다.
• 합성을 실행해 면적, 미매핑 로직, 추론 래치, 미제약 경로를 점검하고 보고서를 가리지 말고 RTL 또는 제약의 원인을 수정합니다.
• 리셋/X 및 블랙박스 가정을 명시적으로 맞춰 RTL과 매핑 넷리스트를 비교하고 미증명 항목을 모두 분류합니다.
• 명명된 입력 버전을 동결하고 waiver 담당자·만료일을 포함한 제약 커버리지 검토본을 발행합니다.

산출물

• 매핑 넷리스트와 합성 QoR 보고서
• 검토된 SDC와 제약 커버리지 보고서
• LEC 결과, 가정, 범위가 정해진 waiver 로그

주의할 점

• 깨끗한 타이밍 보고서도 미제약 경로를 누락할 수 있으므로 명시적으로 검사합니다.
• 오픈소스 formal 통과는 파운드리·고객 플로우가 요구하는 인증 라이브러리와 formal signoff 방법론을 대체하지 않습니다.

원문 출처

Debugging timing ↗
OpenSTA · Constrained and unconstrained timing reports

equiv_make — prepare a circuit for equivalence checking ↗
YosysHQ · Equivalence-check construction

OpenLane Architecture ↗
OpenLane · Open-source RTL-to-GDS stages and checks