scoreboard와 국소 불변식 함께 사용하기

검증의 기준점은 입력 수락이다

scoreboard는 수락한 입력에서 기대 결과를 계산해 큐에 넣고, 출력이 전달될 때 가장 오래된 기대 결과와 비교하는 검사 장치입니다. 회로와 똑같이 단계 레지스터를 흉내 내기보다 입력 계약에서 수학적 결과를 직접 계산하면 공통 오류를 줄일 수 있습니다. 에지마다 제시된 입력을 모두 기대 큐에 넣으면 ready=0인 거절 입력도 처리한 것으로 오해하므로 반드시 수락 이벤트에서만 추가합니다.

예를 들어 ADD 입력 tag10:(250,10), tag11:(3,5)가 수락되면 기대 큐는 [(10,4,carry1),(11,8,carry0)]입니다. 출력 valid=1,ready=0이면 큐를 건드리지 않습니다. tag10이 실제 전달될 때 그 항목만 꺼냅니다. 이후 tag11 대신 tag10이 다시 나왔거나 값 8에 tag12가 붙으면 숫자 일부가 맞아도 실패입니다. scoreboard에는 tag, 데이터와 필요한 flag를 모두 저장합니다.

최종 비교만 있으면 어디서 틀렸는지 찾기 어렵습니다. 국소 불변식은 에지마다 확인하여 가장 먼저 깨진 순간을 기록합니다. 내부 점유는 FIFO count와 각 단계 valid의 합입니다. 한 입력을 수락하고 아직 전달하지 않은 거래 수와 같아야 합니다. reset이나 flush가 있는 구간은 canceled도 빼고, 그 에지에 무슨 사건을 세는지 양쪽 모니터가 같은 계약을 사용해야 합니다.

시험 입력은 기능과 시간 조건을 함께 덮어야 합니다. 산술 경계 0,255,carry·borrow 발생 쌍과 연속 거래, 입력 bubble, 긴 출력 정지, full 교체, 마지막 항목 drain을 조합합니다. 난수 시험에는 seed와 거래 수를 기록하여 같은 실패를 재현할 수 있게 합니다. 작은 제어 공간에서는 모든 ready 패턴을 열거할 수도 있습니다. 많은 반복 횟수만 적는 것보다 어느 경계를 실행했는지 확인하는 것이 중요합니다.

정상 완료를 요구하는 시험에는 timeout과 진행 가정을 명시합니다. 소비자가 일정 시간 뒤 항상 ready가 된다는 drain 조건에서 남은 출력이 모두 나와야 합니다. 소비자가 영원히 정지하는 시험에는 완료 대신 값 보존과 점유 한계를 요구합니다. 이 두 목표를 섞으면 정상 보존을 deadlock으로 잘못 판정할 수 있습니다.

검증 코드에도 오류가 있을 수 있습니다. 의도적으로 carry를 뒤집거나 tag를 한 단계 덜 지연하는 변형을 넣고 검사가 실제 실패하는지 확인하는 mutation 검사는 검사 감도를 보여 줍니다. 다만 여기서 제공하는 Node 모델 통과는 실제 HDL 연결, X/Z, 클록 도메인 교차, 합성 후 timing의 증거가 아닙니다. 같은 계약을 HDL 테스트벤치에 적용할 수 있지만 실제로 실행한 도구와 범위만 보고해야 합니다.