48Verification

Map data from imported RTL

The observed defect

The immutable wrapper successfully writes a value into the external register, then passes ImportedReg.read through the editable mapRead function. The starter compiles, but the displayed value does not reflect what was loaded. This separates a result-mapping defect from a broken RTL port declaration.

Keep mkTop, both interfaces, the wrapper module, and the BVI declaration unchanged. The repair belongs only in the editable function.

Read the starter and predict

Start with the two guarded rules in mkTop. load runs at step 0 and requests an 8-bit pattern; show runs at step 1 and observes reader.read. Then trace that read backward:

RegisterReader.read -> mapRead -> ImportedReg.read -> RTL Q_OUT.

Before editing, predict whether Run will stop at compilation or display an incorrect value. The method and function types agree, so focus on semantic data loss: compare the function argument, which carries Q_OUT, with its result.

Minimal reasoning and observable completion

Preserve the function's Bit#(8) -> Bit#(8) contract and make it retain all eight imported bits. Do not add another register or move either rule; the existing step transition already gives the external register a write cycle before observation.

After Run, the displayed stored value must equal the earlier load input. This must remain true for arbitrary 8-bit patterns, not just the supplied sample. Explain the result in boundary terms: the BVI method still maps Q_OUT; the editable function no longer masks the typed value after it crosses into BSV.

Progressive hints

Transfer experiment

After the required repair, change the loaded pattern to 8'hc3. Predict which rule runs in each step and what show will observe. A correct result mapping needs no further edit for the new value.