Skip to content

Two's complement subtraction and overflow

10 fully proved

Subtraction

TheoremSubtraction by addition#✓fully proved

Let \(x\) and \(y\) be \(n\)-bit words and let \(\bar y\) be the bitwise complement of \(y\). Adding \(x\) and \(\bar y\) with carry in \(1\) gives the \(n\)-bit result \(x - y\) (the difference modulo \(2^n\)), and the carry out is \(1\) exactly when there is no unsigned borrow, that is, when \(y \le x\) as unsigned integers.

theorem adc_not_true : BitVec.adc x (~~~y) true = (!x.usubOverflow y, x - y)
Used by 3
Used byThe carry-lookahead adder subtracts · Carry out of ripple-carry subtraction · The ripple-carry adder subtracts

TheoremThe ripple-carry adder subtracts#✓fully proved

Let \(x\) and \(y\) be \(n\)-bit words and let \(\bar y\) be the bitwise complement of \(y\). Evaluate the \(n\)-bit ripple-carry adder, with XOR, AND and OR gates, on the bits of \(x\), the bits of \(\bar y\) and carry in \(1\). Then for every \(i < n\), output \(i\) is bit \(i\) (counting from the least significant bit \(0\)) of \(x - y\) modulo \(2^n\).

theorem rippleCarryAdder_sub (i : ℕ) (hi : i < n) :
    (rippleCarryAdder n).eval arithInterpretation (rcaInput x (~~~y) true) ⟨i, by omega⟩ =
      (x - y).getLsbD i
Uses 6
Statement usesBoolean interpretation of the arithmetic gates · Arithmetic basis · Input of the ripple-carry adder · Ripple-carry adder
Proof usesSubtraction by addition · Sum bits of the ripple-carry adder

TheoremCarry out of ripple-carry subtraction#✓fully proved

Let \(x\) and \(y\) be \(n\)-bit words and let \(\bar y\) be the bitwise complement of \(y\). Evaluate the \(n\)-bit ripple-carry adder, with XOR, AND and OR gates, on the bits of \(x\), the bits of \(\bar y\) and carry in \(1\). Its carry out (output \(n\)) is \(1\) exactly when there is no unsigned borrow in \(x - y\), that is, when \(y \le x\) as unsigned integers.

theorem rippleCarryAdder_noBorrow :
    (rippleCarryAdder n).eval arithInterpretation (rcaInput x (~~~y) true) ⟨n, by omega⟩ =
      !x.usubOverflow y
Uses 6
Statement usesBoolean interpretation of the arithmetic gates · Arithmetic basis · Input of the ripple-carry adder · Ripple-carry adder
Proof usesSubtraction by addition · Carry out of the ripple-carry adder

TheoremThe carry-lookahead adder subtracts#✓fully proved

Let \(x\) and \(y\) be \(n\)-bit words, let \(\bar y\) be the bitwise complement of \(y\), and let \(K\) satisfy \(n \le 2^K\). Evaluate the \(n\)-bit carry-lookahead adder with \(K\) levels, with XOR, AND and OR gates, on the bits of \(x\), the bits of \(\bar y\) and carry in \(1\). Then for every \(i < n\), output \(i\) is bit \(i\) (counting from the least significant bit \(0\)) of \(x - y\) modulo \(2^n\).

theorem carryLookaheadAdder_sub {K : ℕ} (hK : n ≤ 2 ^ K) (i : ℕ) (hi : i < n) :
    (carryLookaheadAdder n K).eval arithInterpretation (rcaInput x (~~~y) true)
        ⟨i, by omega⟩ = (x - y).getLsbD i
Uses 6
Statement usesKogge–Stone carry-lookahead adder · Boolean interpretation of the arithmetic gates · Arithmetic basis · Input of the ripple-carry adder
Proof usesSum bits of the carry-lookahead adder · Subtraction by addition

Signed overflow

TheoremSigned overflow is the XOR of the last two carries#✓fully proved

Let \(n \ge 1\) and let \(x\) and \(y\) be \(n\)-bit words. The two's complement addition \(x + y\) overflows (the sum of the two's complement values of \(x\) and \(y\) is at least \(2^{n-1}\) or less than \(-2^{n-1}\)) exactly when the carry into the sign bit \(n - 1\) differs from the carry out of it, both carries taken when adding \(x\) and \(y\) with carry in \(0\).

theorem saddOverflow_eq_carry_xor (hn : 0 < n) :
    x.saddOverflow y = (BitVec.carry (n - 1) x y false ^^ BitVec.carry n x y false)
Used by 1
Used byThe overflow flag

DefinitionThe overflow adder#✓fully proved

The \(n\)-bit overflow adder is the \(n\)-bit ripple-carry adder with one extra XOR gate. It has the same \(2n + 1\) inputs (the bits of the two summands, then the carry in) and \(5n + 1\) gates: the \(5n\) gates of the ripple-carry adder, followed by an XOR of the carry into bit \(n - 1\) and the carry into bit \(n\) (the carry out). Here the carry into bit \(0\) is the carry in, and for \(n = 0\) the index \(n - 1\) is read as \(0\). Its \(n + 2\) outputs are the ripple-carry adder's \(n\) sum bits and carry out, followed by the new gate, the signed-overflow flag.

def overflowAdder (n : ℕ) : Circuit arithSignature (2 * n + 1) (n + 2) where
  size := 5 * n + 1
  program := (rcaProgram n (5 * n) (Nat.le_refl _)).gate
    (binLine .xor (carryWire n (5 * n) (n - 1) (by omega)) (carryWire n (5 * n) n (Nat.le_refl _)))
  outputs o :=
    if h : o.val < n + 1 then Wire.castSucc ((rippleCarryAdder n).outputs ⟨o.val, h⟩)
    else Wire.gate (Fin.last (5 * n))
Uses 6 · Used by 4
Statement usesArithmetic gate symbols · Carry wire · Arithmetic basis · Binary gate line · Gate program of the ripple-carry adder · Ripple-carry adder
Used byThe overflow adder extends the ripple-carry adder · The overflow flag · Size of the overflow adder · Sum bits of the overflow adder

TheoremThe overflow adder extends the ripple-carry adder#✓fully proved

Let \(x\) and \(y\) be \(n\)-bit words and let \(c\) be a carry-in bit. Evaluate the \(n\)-bit overflow adder and the \(n\)-bit ripple-carry adder, with XOR, AND and OR gates, on the bits of \(x\), the bits of \(y\) and \(c\). Then for every \(o < n + 1\), output \(o\) of the overflow adder equals output \(o\) of the ripple-carry adder: the first \(n + 1\) outputs (the \(n\) sum bits and the carry out) agree.

theorem overflowAdder_eval_of_lt (c : Bool) (o : ℕ) (ho : o < n + 1) :
    (overflowAdder n).eval arithInterpretation (rcaInput x y c) ⟨o, by omega⟩ =
      (rippleCarryAdder n).eval arithInterpretation (rcaInput x y c) ⟨o, ho⟩
Uses 9 · Used by 1
Statement usesBoolean interpretation of the arithmetic gates · Arithmetic basis · The overflow adder · Input of the ripple-carry adder · Ripple-carry adder
Proof usesArithmetic gate symbols · Carry wire · Binary gate line · Gate program of the ripple-carry adder
Used bySum bits of the overflow adder

TheoremThe overflow flag#✓fully proved

Let \(n \ge 1\) and let \(x\) and \(y\) be \(n\)-bit words. Evaluate the \(n\)-bit overflow adder, with XOR, AND and OR gates, on the bits of \(x\), the bits of \(y\) and carry in \(0\). Its last output (output \(n + 1\)) is \(1\) exactly when the two's complement addition \(x + y\) overflows, that is, when the sum of the two's complement values of \(x\) and \(y\) is at least \(2^{n-1}\) or less than \(-2^{n-1}\).

theorem overflowAdder_overflow (hn : 0 < n) :
    (overflowAdder n).eval arithInterpretation (rcaInput x y false) ⟨n + 1, by omega⟩ =
      x.saddOverflow y
Uses 13
Statement usesBoolean interpretation of the arithmetic gates · Arithmetic basis · The overflow adder · Input of the ripple-carry adder
Proof usesArithmetic gate symbols · Carry wire · Binary gate line · Value of the carry wire · Gate program of the ripple-carry adder · Gate values of the ripple-carry adder · Gate-value specification of the ripple-carry adder · Ripple-carry adder · Signed overflow is the XOR of the last two carries

TheoremSum bits of the overflow adder#✓fully proved

Let \(x\) and \(y\) be \(n\)-bit words. Evaluate the \(n\)-bit overflow adder, with XOR, AND and OR gates, on the bits of \(x\), the bits of \(y\) and carry in \(0\). Then for every \(i < n\), output \(i\) is bit \(i\) (counting from the least significant bit \(0\)) of \(x + y\) modulo \(2^n\).

theorem overflowAdder_sum (i : ℕ) (hi : i < n) :
    (overflowAdder n).eval arithInterpretation (rcaInput x y false) ⟨i, by omega⟩ =
      (x + y).getLsbD i
Uses 7
Statement usesBoolean interpretation of the arithmetic gates · Arithmetic basis · The overflow adder · Input of the ripple-carry adder
Proof usesThe overflow adder extends the ripple-carry adder · Ripple-carry adder · Sum bits of the ripple-carry adder

TheoremSize of the overflow adder#✓fully proved

The \(n\)-bit overflow adder has \(5n + 1\) gates.

This is one gate more than the \(5n\) gates of the \(n\)-bit ripple-carry adder.

theorem overflowAdder_size : (overflowAdder n).size = 5 * n + 1
Uses 2
Statement usesArithmetic basis · The overflow adder

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.