검증 계획, 커버리지와 독립 참조 모델

검증 계획은 명세를 검사 가능한 주장으로 바꿉니다

'잘 동작한다' 대신 reset 뒤 상태, 정상 입력의 출력, 정지 시 유지, 허용하지 않는 입력의 처리, 완료 시점처럼 구체적인 주장을 적습니다. 각 주장에 적어도 하나의 테스트와 관찰점을 연결하면 빠진 조건을 찾기 쉽습니다.

독립 참조 모델이 필요한 이유

시프트 연결 RTL의 참조 모델을 똑같은 슬라이스^{i슬라이스 벡터에서 연속된 비트 범위를 선택하는 연산입니다. 선택한 범위가 결과의 폭과 비트 순서를 정합니다. 자세히 보기}로 복사하면 인덱스 오류까지 복사할 수 있습니다. 정수의 곱셈·modulo 모델이나 문자열의 접미부 비교처럼 다른 표현으로 명세를 구현하면 서로 검토하는 데 도움이 됩니다. 다만 표현만 다르다고 자동으로 독립성이 증명되는 것은 아니므로 작은 사례를 손으로 확인합니다.

커버리지는 통과 개수가 아닙니다

코드 줄이 실행됐다는 coverage는 기능적 경우가 검사됐다는 것과 다릅니다. reset×enable, state×input, full×push×pop 같은 교차 조건이 오류를 드러낼 수 있습니다. 랜덤 테스트에만 맡기지 말고 드물고 중요한 조합을 directed test로 추가하세요.

입력 N개짜리 조합회로는 $2^N$개 입력을 전수 검사할 수 있지만, 순차회로는 입력의 시간열도 존재합니다. 모든 상태가 도달 가능한지, 불변식^{i불변식 모든 허용 실행에서 항상 참이어야 하는 조건입니다. 예를 들어 깊이 4인 FIFO의 저장 개수는 항상 0 이상 4 이하입니다.}이 모든 전이에서 유지되는지 분석해야 합니다. 시뮬레이션의 유한한 통과 기록을 무제한 시간의 수학적 증명으로 표현하지 않습니다.

구현을 복사한 예상값 대신 명세에서 독립적으로 정답을 만듭니다. 실패를 발견하면 실제 값만 저장하지 말고 그 직전 입력·상태도 기록하세요.

실패는 작게 만들고 기록합니다

첫 mismatch의 이전 상태·입력·기대값·실제값을 저장합니다. 필요 없는 자극을 줄여 실패가 유지되는 최소 반례를 만든 뒤 수정합니다. 수정한 테스트만 통과시키지 말고 기존 경계·리셋^{i리셋 상태를 명세한 초기값으로 돌리는 제어입니다. 동기식인지 비동기식인지, 다른 제어보다 우선하는지를 함께 정해야 합니다. 자세히 보기} 검사를 함께 회귀 실행하세요.