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

Put $M=2^n$ for an $n$-bit processor register. The carry flag for addition satisfies $\mathrm{bin}(x)+\mathrm{bin}(y)=\mathrm{bin}(z)+MC$: the result retains the low $n$ bits and $C=1$ records an arithmetic carry beyond them.

For the ARM architecture family subtraction convention, $\mathrm{bin}(x)-\mathrm{bin}(y)=\mathrm{bin}(z)-M(1-C)$. Thus $C=1$ means no borrow, equivalently the unsigned minuend is at least the subtrahend. This flag is different from signed overflow: an arithmetic carry decision is not a test of the signed result.