14검증 문제

카운터 현재 값 읽기

1. 문제와 계약

Counter.value는 8비트 레지스터에 저장된 상태를 그대로 반환해야 합니다. 호출 과정에서 상태를 갱신해서도 안 됩니다. starter의 mkTop은 8'h2a를 저장하지만, 공개 실행에서는 십진수 43이 출력됩니다. 저장된 42와 관찰된 값이 다릅니다.

수정 범위는 mkCounter의 value 구현입니다. 인터페이스, set method, 제공된 최상위 모듈은 그대로 두세요. 화면에 보이는 입력 하나를 상수로 반환하면 다른 8비트 상태에서 계약이 깨집니다.

2. Starter 읽기와 실행 예측

다음 순서로 starter/Main.bsv를 읽어 보세요.

interface Counter에서 set과 value의 method 종류를 구분합니다.
사이클 사이에 값을 보존하는 Reg#(Bit#(8)) 인스턴스를 찾습니다.
load rule의 호출이 레지스터 갱신을 예약하는 과정을 추적합니다.
다음 사이클의 show rule이 value에서 평가하는 식을 확인합니다.

첫 사이클이 끝나면 count에는 8'h2a가 저장됩니다. 다음 사이클의 value method 호출은 상태를 바꾸지 않습니다. 현재 구현은 저장값에 별도의 계산을 적용하므로 십진수 43을 보고합니다. 최소 수정은 저장 구조와 스케줄링을 그대로 두고, 관찰 식만 인터페이스 계약에 맞춥니다.

수정한 뒤 공개 실행은 십진수 42를 표시해야 합니다. value의 반환 타입은 계속 Bit#(8)이어야 하며 Action 문맥이 없어야 합니다. 또한 0, 일반적인 중간값, 8비트 최댓값을 설정해도 같은 값을 그대로 읽을 수 있어야 완료입니다.

3. 단계별 힌트

힌트 1 — 상태의 소유자 찾기

사이클 사이의 카운터 상태를 보존하는 선언은 Reg 인스턴스뿐입니다. 지역 계산 결과는 별도의 상태가 아닙니다.

힌트 2 — 수정 위치 좁히기

set은 요청받은 값을 이미 예약하고, show는 다음 사이클에 실행됩니다. 잘못된 관찰값은 value의 대입 형식 정의에서 만들어집니다.

힌트 3 — 반환 식 판단하기

저장된 8비트 상태 자체를 나타내는 이름을 찾아보세요. 그 이름에 산술 연산을 적용하면 정확한 관찰이 아니라 변환된 값이 됩니다.

4. 추가 실험

필수 수정을 마친 뒤 load가 전달하는 값을 8'hff로 바꾸고, 출력될 십진수를 먼저 예측해 보세요. 이 실험으로 원래 예시에만 맞춘 구현과 모든 8비트 상태를 관찰하는 구현을 구분할 수 있습니다. 제출하기 전에는 starter의 입력으로 복원하세요.