점수판과 불변 조건

두 참조를 분리하기

검증 점수판은 행렬 식을 직접 계산하는 산술 참조와 토큰 이동을 계산하는 시간 참조를 구분합니다. 산술 참조는 for i, for j, for k로 넓은 정수 합을 만들고, 시간 참조는 A의 오른쪽 전달과 B의 아래쪽 전달을 모델링합니다. RTL과 같은 배선 함수를 복사해 만든 정답은 같은 인덱스 오류를 공유할 수 있습니다. 손으로 계산한 작은 예제를 먼저 고정한 뒤 난수 범위를 확장합니다.

점수판의 결과 키는 (job, 전역 i, 전역 j)입니다. 실제 출력이 이 키로 도착하면 예상 값과 비교하고 수신 표시를 합니다. 이미 수신된 키는 중복 출력, 예상하지 않은 좌표는 주소 오류, 끝까지 받지 못한 키는 누락입니다. 값이 0인 결과도 반드시 수신해야 하며, 0이라는 이유로 누락 검사를 생략하지 않습니다. 타일 밖 결과는 전송되어서는 안 됩니다.

PE별 불변 조건

한 작업에서 각 PE의 소비 k목록은 정확히 [0,1,...,K−1]이어야 합니다. valid A와 B가 만날 때 job과 k가 일치하고, count는 0..K 범위에서만 움직입니다. advance=0인 에지에는 데이터·valid·태그·누산기·count가 모두 유지됩니다. clear 뒤에는 count=0, acc=0, valid=0입니다. result_valid&& !result_ready이면 다음 에지에도 결과 데이터와 job이 유지됩니다. 이런 조건은 최종 합이 우연히 같아도 오류를 드러냅니다.

구체적인 실패를 만들기

2×2 양수 예제에서 PE(1,1)은 E2에 18, E3에 50입니다. 래퍼가 E2에 전체 done을 올리면 최종 행렬의 해당 원소만 18이 됩니다. 점수판은 수치 실패와 완료 에지 실패를 둘 다 기록해야 합니다. 반대로 k=0을 두 번, k=1을 누락했는데 두 곱이 같은 값인 입력에서는 최종 합이 맞을 수 있습니다. k목록 검사는 이런 우연을 차단합니다.

난수는 재현 가능한 seed를 저장하고 실패 로그에는 seed, N·K·W, A·B, pause 위치, 첫 불일치 PE·k·물리 에지를 포함합니다. 전체 파형만 남기면 사람이 원인을 찾는 비용이 커집니다. 범위 밖 값이나 tag 오류를 의도한 음성 시험은 정상 결과가 아니라 명확한 실패를 기대합니다. 참조 모델이 무조건 데이터를 버려 정상 종료하는 방식으로 오류를 감추지 않습니다.

클록 동작을 검사할 때는 E_t 직후 상태라는 이 과정의 관측 기준을 고정합니다. 컴파일·RTL 시뮬레이션·합성·타이밍 충족·DDS 프로젝트 실행·실물 보드 성공은 서로 다른 증거입니다. 이 과정에 포함된 Node 프로그램은 수치와 스케줄 참조를 검증하며 다른 단계의 성공을 주장하지 않습니다. 추후 RTL 시뮬레이터를 연결하면 같은 fixture를 입력하되, 도구 버전과 명령·로그를 별도로 보관합니다.