40Verification

Finish only after readiness

Goal and current failure

waitForReady is a three-phase protocol: wait for an external condition, commit 8'h2a to result, and only then publish completion through done. The starter places the completion write first. Its public finish rule can therefore terminate as soon as that first write commits, while ready is still false and result is still zero.

Before editing, predict which statement runs first, which later statements are still pending when finish becomes enabled, and which result the current run can display. This is an ordering failure, not a bad result literal.

Navigate the starter

Read the three register arguments of waitForReady, then label every statement inside its seq as wait, useful work, or publication of completion. Next read mkTop: advance raises ready only after several transitions, while finish watches the learner-controlled done flag rather than the FSM interface's done method.

The editable repair is the ordering inside waitForReady. Keep its signature, the existing await and writes, and the supplied mkTop module unchanged. Do not add another flag or make the environment ready earlier to hide the defect.

Reason about the minimal repair

A completion flag is a promise to its consumer. When done is true, every state named by the protocol must already be valid. Reorder the existing statements so the wait forms the first control boundary, useful work occurs after release, and completion is published only after that work has committed. No statement needs a new expression.

Predict the repaired phases before Run:

1. After start and while ready is false, result remains zero, done remains false, and the FSM remains active.
2. Once the environment commits ready == True, the await can advance.
3. A later action commits result == 8'h2a.
4. Completion becomes visible only after the valid result is observable.

Observable completion contract

The process must expose no result or completion before readiness. It must make forward progress after readiness, write 8'h2a, then set the completion flag. When the public finish rule fires, the result must already be valid. Delaying readiness may change latency, but it must never change this state ordering or allow the FSM to report completion while waiting.

Progressive hints

Transfer experiment

After the required repair works, temporarily change the cycle at which advance raises ready. Predict what changes and what cannot: total waiting time should move, while result must remain zero before release and completion must still follow the result commit. Restore the supplied environment before grading.