12 / 37 · 개념

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는 이전 캡처 상태를 따로 추적하세요. mismatch가 나오면 실패를 유지하는 가장 짧은 입력열로 줄여 보고 원인을 설명합니다.

최종 상태만 비교하는 테스트 대신 매 관찰점의 실제값·예상값·입력을 함께 기록합니다. 이 기록은 '시뮬레이션이 실행됐다'와 '명세를 만족했다'를 구분하는 근거가 됩니다.

직접 생각해 보기

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

해설 보기

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