검증 계획: 실행 가능한 계약, 커버리지, 포멀

입력

• 요구사항·인터페이스 계약·결함 이력
• 합법적 환경 동작 및 리셋 가정
• 위험도 순위 상태공간 및 커버리지 목표

작업

• 각 요구사항을 관측 가능한 속성·스코어보드 규칙·커버포인트로 번역하고 담당자와 완료 근거를 지정합니다.
• 인터페이스 근처에 assertion을 두고 DUT 보장(assert)과 합법 자극 제약(assume)을 구분합니다.
• 상호작용에는 제약 랜덤 테스트, 프로토콜 사실에는 모니터를 사용하며 위험에 영향을 주는 결정에만 교차 커버리지를 둡니다.
• 작은 제어 불변식을 일찍 증명하고 cover 속성으로 의도한 진행을 보이며 반례는 파형으로 검토합니다.
• 과제약과 공허성을 위해 가정을 검토하고 선행조건과 핵심 코너 상태의 도달성을 보이는 cover를 추가합니다.

산출물

• 요구사항-테스트·속성·커버리지 매트릭스
• 재사용 가능한 인터페이스 assertion과 모니터
• 가정 검토를 포함한 포멀 증명·cover 보고서

주의할 점

• DUT가 거부하거나 복구해야 할 불법 동작을 assume으로 없애는 오류.
• 커버리지 비율을 정확성 속성 검증의 근거로 사용하는 오류.

원문 출처

UVM 1.1 User’s Guide ↗
Accellera · §3.12.2 Implementing Checks and Coverage in Interfaces

Formal extensions to Verilog ↗
YosysHQ · §6.1 SystemVerilog Immediate Assertions

Getting started ↗
YosysHQ · SymbiYosys