27 / 63 · 개념

MUX 검증: 전수 검사와 속성

조합 입력의 검사 범위와 저장 동작을 따로 확인하고, 같은 오류를 재현하는 가장 짧은 입력열을 찾습니다.

검증할 입력 범위 정하기

1비트 데이터 a, b와 선택선 sel에는 총 8개의 조합이 있습니다. 이 정도 크기에서는 모든 경우를 확인하는 것이 효율적입니다. 비트 폭이 W인 MUX^{멀티플렉서 선택 신호에 따라 여러 입력 중 하나를 출력으로 연결하는 조합회로입니다. 선택 비트와 입력 번호의 대응을 명세해야 합니다. 자세히 보기}의 입력을 전수 검사하려면 선택선까지 포함해 $2^{2W+1}$ 개 조합을 검사해야 합니다. 따라서 폭이 조금만 커져도 다른 전략이 필요합니다.

출력 폭이 W일 때 각 비트의 선택 규칙은 다음과 같습니다.

\forall i\in\{0,\ldots,W-1\},\quad y_i=\overline s a_i+s b_i

오류 종류에 맞춰 자극을 고릅니다

검사할 오류	유용한 입력 또는 관찰
a/b 연결 반전	a와 b를 다르게 두고 sel=0과 1 비교
비트 순서 반전	한 비트만 1인 walking-one 패턴
stuck-at 결함	모두 0, 모두 1, 교대 비트 패턴
저장 에지 오류	에지 사이에서 입력을 바꾸고 q의 유지 확인
한 사이클 지연 오류	연속 에지의 예상값을 서로 다르게 구성

테스트 수가 많다는 것만으로 좋은 검증이 되지 않습니다. 어떤 결함을 검출하려는지 설명할 수 있어야 합니다.

아래에서는 a와 b가 다른 경우만 골라 비교합니다. 각 열은 테스트 벡터 하나입니다. 잘못된 선택식은 네 열 모두에서 expected와 반대인 값을 출력합니다.

선택 반전 오류를 찾는 네 조합

파형 데이터 보기

파형 데이터: 각 문자는 한 구간, 점은 이전 상태 유지, p는 클록 한 주기입니다.
신호	파형	버스 값
a	`0.1.`
b	`1.0.`
sel	`0101`
expected	`01.0`
swapped bug	`10.1`

참조 모델은 구현과 독립적으로 만듭니다

DUT 코드를 그대로 복사해 참조 모델을 만들면 같은 오류가 참조 모델에도 들어갈 수 있습니다. 명세의 진리표^{진리표 가능한 입력 조합을 빠짐없이 나열하고 각 조합의 출력을 적은 표입니다. 시간에 따른 변화는 파형으로 따로 확인합니다. 자세히 보기}나 인덱스에 따른 선택 규칙으로 예상값을 만들고, 이전 에지에서 q에 저장한 값은 별도로 추적하세요. 예상값과 다른 결과가 나오면 같은 오류가 재현되는 가장 짧은 입력열을 찾아 원인을 설명합니다.

최종 상태만 비교하지 말고, 값을 관찰할 때마다 실제값·예상값·입력을 함께 기록합니다. 이 기록은 '시뮬레이션이 실행됐다'와 '명세를 만족했다'를 구분하는 근거가 됩니다.

직접 생각해 보기

8비트 MUX에서 a=0x00, b=0xFF만으로 두 선택값을 검사했습니다. 이것으로 출력 비트 순서가 뒤집힌 오류도 찾을 수 있나요?

해설 보기

찾을 수 없습니다. 0x00과 0xFF는 비트 순서를 뒤집어도 그대로입니다. 0x01, 0x02처럼 위치가 드러나는 패턴을 선택하고 각 출력 비트를 비교해야 합니다.