18 / 37 · 이해 확인

설계 확인: 폭·우선순위·순환의 경계

주어진 상태 전이 명세로 경계값과 동시 제어 입력을 판단합니다.

modulo-10 카운터의 계약

4비트 unsigned^{unsigned 비트열을 음수가 없는 정수로 해석하는 규칙입니다. n비트의 범위는 0부터 2^n−1이며, 같은 비트열의 signed 해석과 다를 수 있습니다. 자세히 보기} count에 대해 우선순위는 reset, enable, hold 순서입니다. reset이 1이면 0으로, enable이 1이면 9 이상에서 0으로 돌아가고 나머지 상태에서는 1 증가합니다.

N=\lceil\log_2 10\rceil=4

4비트라는 사실은 저장 가능한 상태가 16개임을 뜻합니다. 사용하려는 상태가 10개라는 명세까지 자동으로 구현해 주지는 않습니다. 특히 count=9에서 enable=0일 때는 0으로 돌아가면 안 됩니다.

각 열은 한 상승 에지^{상승 에지 클록이 0에서 1로 바뀌는 순간입니다. CLK=1인 구간 전체를 뜻하는 레벨과 구별합니다. 자세히 보기}의 관찰 기록입니다. 입력은 에지 직전, 이름에 after가 붙은 상태는 갱신 직후 값입니다. 열의 정렬은 샘플 순서를 나타내며 물리적인 전파 지연^{전파 지연 입력이 바뀐 뒤 출력이 올바른 값으로 안정되기까지 걸리는 시간입니다. 논리식의 등가성과 시간 특성은 별개입니다. 자세히 보기}을 그린 것이 아닙니다. 초기 count=9입니다. reset이 없는 첫 열에서 enable=0이면 9를 유지하고, 다음 열에서 enable=1일 때만 0으로 돌아갑니다.

경계값에서도 hold는 유지되어야 합니다

파형 데이터 보기

파형 데이터: 각 문자는 한 구간, 점은 이전 상태 유지, p는 클록 한 주기입니다.
신호	파형	버스 값
edge	`2345`	E0 → E1 → E2 → E3
reset	`0.10`
enable	`01..`
count after	`23.4`	9 → 0 → 1

추가 설계 문제

count=9, reset=0, enable=0일 때 다음 값을 구하세요.
count=15에서 enable=1을 넣었을 때 복귀 정책을 설명하세요.
count=9, reset=1, enable=1이면 종료 펄스가 나와야 하는지 명세를 정하세요. 리셋^{리셋 상태를 명세한 초기값으로 돌리는 제어입니다. 동기식인지 비동기식인지, 다른 제어보다 우선하는지를 함께 정해야 합니다. 자세히 보기} 중 출력은 0으로 정의했다고 가정합니다.

직접 생각해 보기

0~15의 모든 count 값과 reset·enable 조합을 전수 검사하려면 몇 개의 한 단계 전이 사례가 필요합니까? 이 검사만으로 긴 상태열 전체의 요구사항이 자동 증명됩니까?

해설 보기

$16\times2\times2=64$ 개입니다. 이 설계처럼 완전한 상태를 count가 표현하고 다음 상태·출력 명세가 정확하면 한 단계 검사가 강한 근거가 됩니다. 다만 초기화, 입력 가정, 종료 펄스의 별도 상태, 실제 타이밍 등 누락된 요구사항까지 증명하지는 않습니다.

현재 count=9에서 reset=1과 enable=1이 동시에 샘플링됐습니다. 리셋 우선 명세에 맞는 다음 count와 종료 펄스는?

답 선택count=0, 종료 펄스=1: 정상 순환으로 처리합니다.count=10, 종료 펄스=0: enable이 우선입니다.count=0, 종료 펄스=0: 리셋이 상태와 펄스를 초기화합니다.