29Verification

Preserve a register's upper byte

Situation and starter reading

patchLow should replace only the low byte of stored word. The starter is legal BSV, but it zero-extends the replacement and writes all sixteen bits, so an existing upper byte is discarded.

Read BytePatcher first to identify each method's contract. In mkBytePatcher, compare the whole-register write in load with the write in patchLow; only the latter is defective. Then trace mkTop by step: load, patch, and observation happen on separate clock cycles. Edit only the patchLow implementation. Keep the interface, load, word, and mkTop unchanged.

Predict before editing

The starter compiles. Starting from 16'habcd, load commits that complete word at one edge. On the next edge, the current patchLow write replaces it with the zero-extended byte, so Run reports 16'h0034, not 16'hab34. This is a runtime state-transition defect rather than a compile-time error.

The minimal reasoning is a bit-preservation equation: the next state's low eight bits come from replacement, while its high eight bits come from the current register. A selected register write expresses that read-modify-write without rebuilding the complete value manually.

Required change and observable completion

• Replace bits 7 through 0 and preserve bits 15 through 8.
• Use a selection on the destination of the existing register write.
• Preserve all public method names and types.

Run is observably correct when the supplied sequence finishes with 16'hab34. Completion must also hold for arbitrary upper bytes and repeated patches; hard-coding 16'hab34 does not preserve current state.

Progressive hints

Transfer experiment

After completion, temporarily add one more state-machine step that calls patchLow with a different byte before show. Predict that the upper byte still comes from the original load while the low byte comes from the newest patch. Remove the extra step after the experiment.