 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/1/b/solution

Split each input into its more and less significant

n

-bit halves:

a = 2^{n} a_{H} + a_{L}

and

b = 2^{n} b_{H} + b_{L}

. Let the two digital comparators produce

(L_{H}, G_{H})

and

(L_{L}, G_{L})

. The more significant halves are equal exactly when

E_{H} = \neg (L_{H} \lor G_{H})

L = L_{H} \lor (E_{H} \land L_{L}), G = G_{H} \lor (E_{H} \land G_{L}) .

Implement

E_{H}

a_{H} \neq = b_{H}

2^{n} (a_{H} - b_{H})

has magnitude at least

2^{n}

, whereas

∣ a_{L} - b_{L} ∣ \leq 2^{n} - 1

; hence the more significant comparison decides the result. If

a_{H} = b_{H}

, the lower comparison decides it. This proves correctness in every case using a constant number of extra logic gates.

 New to topics? Read the docs here!