 Solution

ID: 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 \leq i \leq 15

, and sets every output bit

16 \leq i \leq 31

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 is

- s 2^{31} + s \sum_{i = 16}^{30} 2^{i} + \sum_{i = 0}^{15} b_{i} 2^{i} = - s 2^{16} + s 2^{15} + \sum_{i = 0}^{14} b_{i} 2^{i} = - s 2^{15} + i = 0 \sum 14 b_{i} 2^{i} .

The 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}

 New to topics? Read the docs here!