카운터 디버깅과 최소 반례

최종값이 맞아도 순서가 틀릴 수 있습니다

카운터가 0으로 끝났다는 사실만으로 reset과 wraparound가 맞았다고 결론 내릴 수 없습니다. 계속 0에 멈춘 회로도 같은 결과를 냅니다. 정상 증가, 유지, 리셋^{i리셋 상태를 명세한 초기값으로 돌리는 제어입니다. 동기식인지 비동기식인지, 다른 제어보다 우선하는지를 함께 정해야 합니다. 자세히 보기}, 경계 순환을 각각 드러내는 관찰점이 필요합니다.

두 기능을 일부러 충돌시킵니다

우선순위 오류는 제어를 따로 하나씩만 시험하면 발견하기 어렵습니다.

각 열은 한 상승 에지^{i상승 에지 클록이 0에서 1로 바뀌는 순간입니다. CLK=1인 구간 전체를 뜻하는 레벨과 구별합니다. 자세히 보기}의 관찰 기록입니다. 입력은 에지 직전, 이름에 after가 붙은 상태는 갱신 직후 값입니다. 열의 정렬은 샘플 순서를 나타내며 물리적인 전파 지연^{i전파 지연 입력이 바뀐 뒤 출력이 올바른 값으로 안정되기까지 걸리는 시간입니다. 논리식의 등가성과 시간 특성은 별개입니다. 자세히 보기}을 그린 것이 아닙니다. 초기 count=5입니다. 잘못된 회로는 enable 안쪽에서만 reset을 검사하므로 첫 에지에 5를 유지합니다. 마지막 값은 같아도 첫 불일치가 결함을 드러냅니다.

modulo-8 참조 회로를 초기 101에서 시작합니다. enable=0, reset=1을 고르고 클록을 진행하세요. 올바른 값은 000입니다. reset을 enable 안에 넣은 잘못된 RTL은 101을 유지합니다. reset을 해제한 뒤 enable=0에서의 유지와 enable=1에서의 증가도 구분하세요.

참조 모델로 첫 불일치 찾기

이 식은 0~M-1의 정상 상태를 전제로 한 기능 모델입니다. 범위 밖 상태 복구는 별도 정책으로 추가합니다. 매 에지에 기대값을 계산하고 실제값과 비교하세요. 불일치가 처음 난 직전 에지의 입력과 상태가 원인을 찾는 가장 작은 출발점입니다.

실패가 1000사이클 뒤 나타났다면 필요 없는 입력 구간을 줄여 같은 오류를 3~5에지로 재현해 보세요. RTL 수정 후에는 그 최소 반례를 회귀 테스트에 남깁니다. 설계와 테스트를 동시에 같은 잘못된 조건으로 바꾸지 않도록, 수정한 명세와 코드를 따로 검토합니다.