43Verification

Report when a FIFOF can accept data

Problem

ElasticQueue.canEnq must report whether the two-entry queue has room for one more value, so a producer can hold back instead of attempting an enqueue that cannot proceed. The starter reports the opposite in the two edge states: false while empty and true while full. canDeq and the data methods are already correct.

Fix only the expression of canEnq. Keep the interface, canDeq, enq, deq, the queue depth, and mkTop unchanged.

Read and predict

1. Read the four interface methods and sort them into producer side (enq, canEnq) and consumer side (deq, canDeq).
2. Read the two status methods in mkElasticQueue. Note that both are connected to the same FIFOF status.
3. Trace mkTop. Each labeled line prints the status pair before that step's action: empty, one entry, full, after one dequeue, and drained.

Before pressing Run, write the required pair for each label.

Then run the starter and mark the lines where its canEnq disagrees with your table.

Make the repair

Producer readiness depends on free capacity; consumer readiness depends on stored data. These are different conditions that happen to agree in the middle states, which is why the starter looks right on two lines. Connect canEnq to the status that describes capacity, run again, and check every row. Explain why the one and after deq rows could not catch the defect.

Completion contract

• canEnq is true whenever at least one slot is free and false only when both entries are occupied.
• canDeq still reports whether an entry is available.
• Every labeled line matches the table, not only the initial empty state.
• The status follows the actual queue state, so it also holds for other sequences of enqueues and dequeues.

Progressive hints

Transfer experiment

On paper, change mkTop so that it enqueues three times before any dequeue. Predict which rule would wait, and explain why that rule prints nothing while it waits: its $display belongs to the same atomic action as the blocked enqueue.