reference model 독립성: 두 구현이 같은 4를 내도 틀릴 수 있다

8비트 덧셈 회로가 250과 10을 더해 4를 내놓았다. 참조 모델도 4라고 답해 테스트는 통과했다. 그런데 명세는 unsigned saturating addition이다. 범위를 넘으면 최댓값 255가 나와야 한다. DUT와 모델이 같은 계산 오류를 공유하면 비교 횟수가 많아도 오류는 드러나지 않는다.

reference model 독립성은 코드 파일을 따로 두는 것보다 깊은 조건이다. 같은 잘못된 계산 순서나 폭 해석을 두 구현에 복사하지 않아야 한다.

비교할 계약부터 분명히 한다

예제의 입력 a와 b는 각각 0~255이고 정답은 min(255, a+b)다. 보통의 8비트 modulo 덧셈과 다른 계약이다. modulo라면 250+10의 하위 8비트인 4가 맞지만, 여기서는 범위 초과를 최댓값으로 제한한다.

잘못된 RTL이 합을 먼저 8비트 변수에 저장한 뒤 그 변수를 255와 비교한다고 하자. 260이 이미 4로 잘려 있으므로 범위 초과를 알아낼 수 없다. 참조 모델도 8비트 변수로 같은 순서를 옮겼다면 똑같이 실패한다.

두 코드가 비슷할수록 읽기 편할 수 있지만, 오류를 발견할 독립적인 경로가 줄어든다. RTL의 중간 신호를 그대로 Python 객체로 옮기는 방식은 다른 언어를 사용해도 같은 문제를 남긴다.

다른 추상 수준에서 정답을 만든다

이 명세의 참조 모델은 하드웨어의 carry chain이나 pipeline을 흉내 낼 필요가 없다. 충분한 정밀도의 정수로 의미를 직접 계산할 수 있다.

def reference_add(a, b):
    if not (0 <= a <= 255 and 0 <= b <= 255):
        raise ValueError("8-bit unsigned inputs required")
    return min(255, a + b)

DUT에서는 합을 9비트로 계산하고 carry 또는 범위 초과 조건을 사용해 구현할 수 있다. 모델은 명세 수식으로, DUT는 하드웨어 구조로 구현하면 같은 폭 축소 실수를 무심코 공유할 가능성을 줄인다. 그러나 모델도 입력 의미와 출력 폭은 명세에 맞게 처리해야 한다.

이 작은 입력 공간에는 256×256=65,536개 쌍이 있다. 설명용으로 잘못된 함수 (a+b)&255와 위 명세 수식을 전수 비교하면, 합이 255를 넘는 32,640개에서 결과가 다르다. 이는 두 정수 함수의 직접 계산이며 실제 RTL을 실행한 측정은 아니다. 더 큰 DUT에서 전수 검사가 불가능하더라도, 이런 작은 성질과 경계값으로 모델 자체를 먼저 점검할 수 있다.

0+0, 255+0, 254+1은 정상 범위와 경계다. 255+1과 255+255는 초과 처리다. 각각의 기대값을 모델 구현과 별도로 손으로 계산해 놓으면 단순한 모델 버그도 검출할 기회를 얻는다.

검증된 라이브러리도 설정과 범위를 맞춘다

복잡한 부동소수점에서는 명세 수식을 직접 구현하기보다 기존 소프트웨어 구현을 사용할 수 있다. Berkeley TestFloat의 testfloat_gen은 연산 이름으로 실행하면 SoftFloat가 계산한 결과와 exception flag를 test case에 포함한다. 숫자 결과만 맞추는 시험과 flag까지 맞추는 시험은 다르다. Berkeley TestFloat, testfloat_gen

TestFloat의 일반 문서는 SoftFloat 자체를 시험할 때 더 단순하고 느리며 독립적인 두 번째 구현을 사용한다고 설명한다. 한 구현이 다른 구현의 오류를 그대로 재현할 가능성을 줄이는 접근이다. 하지만 독립적인 구현도 오류가 없다고 보장할 수는 없다고 함께 밝힌다. Berkeley TestFloat, §4 What TestFloat Does

독립성은 결과가 다를 때 어느 쪽이 틀렸는지 자동으로 알려 주지는 않는다. 먼저 입력 인코딩과 정밀도, rounding mode, 예외 flag 정책을 맞추어야 한다. TestFloat 문서도 명세에서 허용하는 선택이나 참조 구현·검사 프로그램의 문제 때문에 차이가 보고될 수 있음을 설명한다. 차이를 무조건 DUT 오류로 단정하지 않는 이유다.

예를 들어 서로 다른 NaN encoding을 허용하는 계약에서 모든 결과 bit를 강제로 같게 비교하면 합법적인 차이를 오류로 볼 수 있다. 반대로 실제 ISA가 특정 NaN 동작을 요구한다면 느슨한 비교로 그 요구를 지워서는 안 된다. 독립 모델의 일반 설정과 대상 명세의 비교 정책을 구분한다.

모델이 회로의 우연한 구조를 따라가지 않게 한다

기능 정답을 계산하는 모델이 DUT와 같은 pipeline 단계와 임시 register 폭을 사용할 필요는 없다. 예상값을 실제 수락 요청에서 만들고, 응답의 식별과 완료 시점은 별도의 비교 경로에서 처리하면 계산 의미를 더 단순하게 유지할 수 있다.

반면 latency가 명세의 일부인 회로라면 값만 같아도 충분하지 않다. 정답 계산을 독립적으로 하면서 요구하는 시간 조건은 별도로 검사한다. 독립성을 높인다는 이유로 계약의 일부를 생략하지 않는다.

250+10에서 두 구현이 모두 4를 답한 것은 정답의 증거가 아니다. unsigned saturating addition이라는 계약으로 돌아가 충분한 폭에서 260을 구하면 255가 필요하다는 것을 알 수 있다. 참조 모델은 DUT의 코드를 번역하는 데서 멈추지 않고, 다른 추상 수준과 독립적인 경계 검산으로 그 계약을 확인해야 한다.