12Verification

Sign-extend a four-bit integer

Trace the starter before editing

Read asSignedByte from the inside out. Its Bit#(4) input is first widened by zeroExtend; only then does unpack assign the eight-bit pattern the type Int#(8). mkTop supplies 4'b1101, whose four-bit two's-complement meaning is -3.

Predict the current run: zero extension produces an eight-bit pattern beginning with zeros, so signed interpretation sees a positive value. The starter compiles, but the displayed value is 13 rather than -3. The symptom appears only for inputs whose original bit 3 is one; the root cause is that signedness was assigned after the width grew.

Repair only the return expression. Preserve the package, signature, and mkTop observation.

Reason about the minimal repair

Two operations are required, but their order carries the contract. First give the original four bits the signed interpretation that makes bit 3 a sign bit. Then widen that signed value with an operation that copies its sign into the new high positions. There is no need for a conditional, manual mask, register, or rule.

After the repair, Run must still compile and the mixed negative sample must retain its numerical value. Explain the result as an eight-bit two's-complement representation, not as display formatting.

Observable completion contract

The function is complete when it preserves every value representable by Int#(4) while returning Int#(8):

• 0000 remains zero and 0111 remains the largest positive value;
• 1000 remains the smallest four-bit signed value;
• mixed negative patterns such as 1101 remain negative with the same value;
• all newly added high bits equal the original sign bit.

Testing both sides of the 0111/1000 boundary prevents a zero extension from appearing correct.

Progressive hints

Transfer experiment

Temporarily reverse the two conceptual steps again and run once with 1000 and once with 0111. Predict why only one side of the signed boundary exposes the defect. Restore the repaired order afterward.