43검증 문제

FIFOF가 데이터를 받을 수 있는지 알리기

1. 문제와 수정 범위

ElasticQueue.canEnq는 항목 두 개짜리 큐에 값을 하나 더 넣을 자리가 있는지 알려야 합니다. 생산자는 이 신호를 보고, 진행할 수 없는 넣기를 시도하지 않고 기다립니다. starter는 양 끝 상태에서 정반대로 보고합니다. 비어 있으면 거짓, 가득 차면 참입니다. canDeq와 데이터 method는 이미 올바릅니다.

canEnq의 식만 수정하세요. 인터페이스, canDeq, enq, deq, 큐 깊이, mkTop은 그대로 둡니다.

2. starter 읽기와 실행 전 예측

1. 인터페이스의 method 네 개를 생산자 쪽(enq, canEnq)과 소비자 쪽(deq, canDeq)으로 나누어 보세요.
2. mkElasticQueue의 상태 method 두 개를 읽어 보세요. 둘 다 같은 FIFOF 상태에 연결되어 있습니다.
3. mkTop을 따라가 보세요. 각 줄은 그 단계의 동작 전에 상태 쌍을 출력합니다. 순서는 비어 있음, 항목 하나, 가득 참, 하나 꺼낸 뒤, 모두 꺼낸 뒤입니다.

실행 전에 출력 라벨마다 요구되는 값을 적어 보세요.

starter를 실행하고, canEnq가 표와 다른 줄을 표시해 보세요.

3. 최소 수정과 완료 조건

생산자 쪽 준비 조건은 남은 자리에, 소비자 쪽 준비 조건은 저장된 데이터에 달려 있습니다. 두 조건은 중간 상태에서 우연히 같은 값이 되므로 starter가 두 줄에서는 맞아 보입니다. canEnq를 남은 자리를 나타내는 상태에 연결하고, 다시 실행해 모든 줄을 확인하세요. one과 after deq 줄로는 결함을 찾을 수 없는 이유도 설명해 보세요.

• 빈 자리가 하나라도 있으면 canEnq가 참이고, 두 항목이 모두 차 있을 때만 거짓입니다.
• canDeq는 계속해서 꺼낼 항목이 있는지를 알립니다.
• 처음의 빈 상태만이 아니라 라벨이 붙은 모든 줄이 표와 일치합니다.
• 상태 신호가 실제 큐 상태를 따르므로 넣기와 꺼내기 순서가 달라도 성립합니다.

4. 단계형 힌트

5. 추가 실험

mkTop이 꺼내기 전에 세 번 넣도록 바뀌었다고 가정해 보세요. 어느 rule이 기다리게 되는지 예측해 보세요. $display는 막힌 넣기와 같은 원자적 동작에 속하므로, 기다리는 동안 그 rule은 아무것도 출력하지 않습니다.