Tutorial: Ripple-Carry Adder

In this tutorial, we verify a ripple-carry adder — a fundamental digital circuit that adds two binary numbers. This demonstrates ImandraX's ability to reason about hardware designs at the bit level.

The circuit components

A full adder computes a sum bit and a carry-out bit from two input bits and a carry-in:

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)

Bit-vector representation

We represent binary numbers as lists of booleans (least-significant bit first):

(* The integer value of a single bit *)
let val_bit (a : bool) =
  if a then 1 else 0
 
(* The integer value of a bit vector *)
let rec val_bits (a : bool list) =
  match a with
  | [] -> 0
  | a1 :: a' -> val_bit a1 + val_bits a' * 2

For example, val_bits [true; false; true] = 1 + 0 + 4 = 5 (binary 101).

The ripple-carry adder

Chain full adders together, propagating carries:

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]

The final carry-out appears as the last bit of the result.

The correctness theorem

The main theorem states that the ripple-carry adder computes the sum of its inputs:

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]

ImandraX proves this fully automatically with [@@by auto]. The waterfall:

1. Performs induction on the bit vectors a and b
2. In the base case, both are empty, and the result is just [cin] with value val_bit cin
3. In the inductive step, it uses the properties of adder_sum and adder_carry_out together with the inductive hypothesis about the remaining bits

A bonus lemma

We can also prove correctness of a single adder stage independently:

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 says: the sum bit equals the total minus twice the carry. While not needed for the main theorem (ImandraX handles it automatically!), it's a nice modular verification of the individual full adder.

What makes this impressive

The ripple-carry adder theorem is notable because:

• No lemmas needed — [@@by auto] handles the entire proof
• Bit-level reasoning — ImandraX reasons about boolean operations and their relationship to integer arithmetic
• Arbitrary width — The theorem holds for bit vectors of any length, not just fixed widths
• Real hardware — This is exactly the circuit used in basic arithmetic logic units

Compare this with model checking approaches that can only verify fixed bit widths. ImandraX proves correctness for all widths simultaneously through induction.

What you've learned

• Hardware verification using boolean functions and bit vectors
• How ImandraX automatically handles complex inductive proofs
• Bit-level to integer-level correspondence — relating boolean circuits to arithmetic
• The power of [@@by auto] on well-structured problems

Next steps

The Majority Vote tutorial shows a more complex algorithm verification requiring explicit lemma usage.