Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof / 2 / b / Solution

Let the stored bits be $b_{15},\dots ,b_0$ and let $s=b_{15}$. The sign extension performed by ldrsh keeps output bit $i$ equal to $b_i$ for $0\le i\le 15$, and sets every output bit $16\le i\le 31$ to $s$. Thus a nonnegative halfword gets sixteen leading zero bits, while a negative halfword gets sixteen leading one bits.

Its signed 32-bit two's complement value isThe last expression is exactly the original signed 16-bit value. The equality uses the finite geometric series ${\sum }_{i=16}^{30}{2}^i=2^{31}-2^{16}$. In particular, simply inserting zero bits would be wrong for a negative halfword: its unsigned interpretation differs from its signed value by $2^{16}$.