Ripple-Carry Adder Verification

Correctness proof of a ripple-carry adder circuit — verifying that the hardware correctly computes binary addition for arbitrary-width inputs. Proved fully automatically by ImandraX.

Overview

A ripple-carry adder is the simplest form of binary adder circuit. It chains together full adders, each computing a single-bit sum and carry-out from two input bits and a carry-in. While simple in concept, proving its correctness for arbitrary-width inputs requires induction over the bit vector length.

This is a classic hardware verification benchmark — and ImandraX handles it with a single auto tactic.

The Model

Single-Bit Adder Components

let xor (x : bool) (y : bool) : bool = x <> y
 
let adder_sum a b cin =
  xor (xor a b) cin
 
let adder_carry_out a b cin =
  ((xor a b) && cin) || (a && b)

Full Adder Truth Table

Each full adder implements this logic:

The algebraic relationship: val(sum) + 2 * val(cout) = val(a) + val(b) + val(cin).

Composing Full Adders

The ripple-carry adder chains full adders together, propagating the carry from each stage to the next:

let rec ripple_carry_adder (a : bool list) (b : bool list) (cin : bool)
    : bool list =
  match a, b with
  | a1 :: a', b1 :: b' ->
    adder_sum a1 b1 cin ::
    ripple_carry_adder a' b' (adder_carry_out a1 b1 cin)
  | _, _ -> [cin]

Bit Vector Interpretation

let val_bit (a : bool) = if a then 1 else 0
 
(* Least-significant bit first *)
let rec val_bits (a : bool list) =
  match a with
  | [] -> 0
  | a1 :: a' -> val_bit a1 + val_bits a' * 2

Verification

The Main Theorem

The correctness theorem states that the ripple-carry adder computes the sum of its inputs for any input width:

theorem full_ripple_carry_adder_correct a b cin =
  List.length a = List.length b
  ==>
  val_bits (ripple_carry_adder a b cin) =
  val_bits a + val_bits b + val_bit cin
[@@by auto]

This is proved fully automatically — ImandraX's inductive waterfall discovers the correct induction scheme, applies the inductive hypothesis, and discharges all subgoals without any human guidance.

Single-Component Correctness

We can also verify each adder component individually:

lemma single_adder_circuit_correct a b cin =
  val_bit (adder_sum a b cin)
    = val_bit a + val_bit b + val_bit cin
      - val_bit (adder_carry_out a b cin) * 2
[@@rw]

This establishes that each full adder correctly computes sum = a + b + cin - 2 * carry_out — though the main theorem doesn't even need this lemma.

Why Full Automation Works

ImandraX's auto tactic succeeds here because:

1. Structural induction — the ripple-carry adder recurses on the input lists, and ImandraX discovers this as the induction scheme
2. Case splitting — boolean inputs naturally decompose into finitely many cases per induction step
3. Arithmetic simplification — the algebraic identity val_bit(sum) + 2 * val_bit(cout) = val_bit(a) + val_bit(b) + val_bit(cin) is within the simplifier's capabilities
4. No auxiliary lemmas needed — unlike many hardware proofs that require carry propagation lemmas, ImandraX handles the carry chain directly

Results

This case study demonstrates ImandraX's strength in hardware verification:

• Full automation — the main theorem is proved with a single auto, no lemma hints needed
• Arbitrary width — the proof covers all input widths, not just specific sizes
• Bit-level precision — reasoning directly about boolean logic and carry propagation
• Clean specification — the correctness statement is immediately readable: the bit vector output equals the arithmetic sum

References

• Source: adder.iml