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

명세에서 무엇을 검사할지 구체적으로 정합니다

'잘 동작한다'고만 쓰지 말고 reset 뒤의 상태, 정상 입력의 출력, 정지 시 값 유지, 허용하지 않는 입력의 처리, 완료 시점처럼 검사할 조건을 구체적으로 적습니다. 각 조건을 확인할 테스트와 관찰 지점을 적어도 하나씩 정하면 빠진 조건을 찾기 쉽습니다.

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

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

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

코드 줄의 실행 여부를 나타내는 커버리지 결과와 필요한 기능을 검사했다는 사실은 다릅니다. reset×enable, state×input, full×push×pop 같은 교차 조건이 오류를 드러낼 수 있습니다. 랜덤 테스트에만 맡기지 말고 드물고 중요한 조합을 directed test로 추가하세요.

입력 N개짜리 조합회로는 $2^N$개 입력을 전수 검사할 수 있지만, 순차회로에서는 입력이 들어오는 순서와 시간도 고려해야 합니다. 모든 상태가 도달 가능한지, 불변식^{i불변식 모든 허용 실행에서 항상 참이어야 하는 조건입니다. 예를 들어 깊이 4인 FIFO의 저장 개수는 항상 0 이상 4 이하입니다.}이 모든 전이에서 유지되는지 분석해야 합니다. 정해진 횟수의 시뮬레이션을 통과한 결과를, 모든 시간에 대해 성립하는 수학적 증명이라고 할 수는 없습니다.

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

실패를 재현하는 입력을 줄이고 기록합니다

처음으로 결과가 일치하지 않은 시점의 직전 상태·입력·기대값·실제값을 저장합니다. 필요 없는 자극을 줄여 실패가 유지되는 최소 반례를 만든 뒤 수정합니다. 수정한 테스트뿐 아니라 기존의 경계 조건·리셋^{i리셋 상태를 미리 정한 초기값으로 되돌리는 제어입니다. 동기식인지 비동기식인지, 다른 제어보다 우선하는지를 함께 정해야 합니다. 자세히 보기} 테스트도 다시 실행해, 다른 동작에 문제가 없는지 확인하세요.