Case Study: Building a Boolean Circuit Simplifier from the Algebra Laws

DataField.Dev

Case Study: Building a Boolean Circuit Simplifier from the Algebra Laws

"Simplicity is prerequisite for reliability." — Edsger W. Dijkstra

Executive Summary

In this build-focused case study you'll construct a small Boolean expression simplifier — the core idea behind the logic-synthesis tools that shrink real chips — and you'll do it the principled way: every simplification it performs is one of the laws of Boolean algebra from §13.5, and you will be able to point at the law for each rewrite. Where Case Study 1 analyzed an existing structure, here you build a working tool, piece by piece, from an expression representation up through a verified optimizer.

The payoff is the chapter's central claim made executable: the algebraic laws are not decoration, they are circuit-simplification rules, and fewer operations mean fewer gates. You'll represent expressions as small trees, write functions that apply individual laws (identity, domination, idempotence, complement, absorption), compose them into a simplifier, and then — crucially — verify the optimizer against a brute-force truth-table check over all input assignments. That last step is theme four of the book in miniature: the laws prove the rewrite is sound for all inputs; the truth-table test catches any bug in our implementation of them.

Skills applied

Representing a Boolean expression as a tree (the algebraic structure of §13.5–§13.6).
Implementing individual Boolean laws as local rewrite rules, each justified by name.
Composing rewrites into a fixpoint simplifier and counting the gates eliminated.
Verifying behavioral equivalence with an exhaustive truth-table check (theme four).
Connecting absorption and De Morgan to concrete gate deletions (§13.6).

Background

The scenario

You're on a team writing a tiny hardware-description toolchain for a class project. A designer writes a Boolean expression for a circuit's output; your job is to simplify it before it's turned into gates, because each operation becomes a physical AND/OR/NOT gate — and fewer gates mean less silicon, less power, and less delay (§13.6). The designer hands you this expression for an enable signal:

$$ \text{enable} = (a \wedge b) \vee (a \wedge b \wedge c) \vee (a \wedge \overline{a}) \vee (a \wedge 1). $$

A human can eyeball that this collapses dramatically, but you want a tool that does it and a guarantee that the simplified form behaves identically. You will build both.

🔗 Connection. This is §13.6 made tangible: "the algebraic laws are circuit-simplification rules, and fewer operations means fewer gates." We are literally writing the rule engine. And it ties back to Chapter 1: each law is a logical equivalence you once verified by truth table; now we use the laws to transform expressions, which a truth table cannot do.

Why this matters

Real logic-synthesis tools (the software that compiles a hardware design into a gate netlist) apply exactly these laws — plus many more — to circuits with millions of gates. They can only do so because the laws are theorems: guaranteed for every input, not merely tested. A rewrite that were only "usually" valid would be catastrophic in hardware. Building a miniature version teaches both halves: how a rewrite engine is structured, and why its correctness rests on proof rather than testing.

Phase 1: Represent the expression

We'll represent a Boolean expression as a nested tuple — a tiny tree. Leaves are variable names (strings) or the constants 0 and 1; internal nodes are ('and', x, y), ('or', x, y), or ('not', x).

# Constants and leaves: 0, 1, 'a', 'b', ...
# Nodes: ('and', x, y), ('or', x, y), ('not', x)

def show(e):
    """Pretty-print an expression tree as infix, for readability."""
    if e in (0, 1) or isinstance(e, str):
        return str(e)
    if e[0] == 'not':
        return f"~{show(e[1])}"
    op = '&' if e[0] == 'and' else '|'
    return f"({show(e[1])} {op} {show(e[2])})"

# The designer's expression:
enable = ('or',
            ('or',
              ('or', ('and', 'a', 'b'),
                     ('and', ('and', 'a', 'b'), 'c')),
              ('and', 'a', ('not', 'a'))),
            ('and', 'a', 1))

print(show(enable))
# Expected output:
# ((((a & b) | ((a & b) & c)) | (a & ~a)) | (a & 1))

That printed form is the designer's circuit verbatim: count the operations (one per internal tree node) and you have 9 gates — five & (including the nested (a & b) that appears twice), one ~, and three | joining the terms. We'll confirm the count with a tool in the "Your Turn" extensions.

💡 Intuition: An expression tree is a combinational circuit (§13.6): each internal node is a gate, each leaf a wire carrying an input or a constant. Simplifying the tree is deleting gates. Our job is to prune the tree using moves that provably preserve the output on every input.

Phase 2: Implement the laws as rewrite rules

Each rule is a local transformation matching a pattern and returning the simplified subtree, annotated with the law from §13.5 that justifies it. We return the input unchanged if no rule applies.

def simplify_node(e):
    """Apply one Boolean law at the top of e, if any matches. Each branch
    cites the law from section 13.5 that makes the rewrite sound."""
    if not isinstance(e, tuple):
        return e
    op = e[0]
    if op == 'not':
        x = e[1]
        if x == 0: return 1                      # complement of constants
        if x == 1: return 0
        if isinstance(x, tuple) and x[0] == 'not':
            return x[1]                           # double negation: ~~a = a
        return e
    x, y = e[1], e[2]
    if op == 'and':
        if x == 1: return y                       # identity:   1 & y = y
        if y == 1: return x                       # identity:   x & 1 = x
        if x == 0 or y == 0: return 0             # domination: x & 0 = 0
        if x == y: return x                       # idempotent: x & x = x
        if y == ('not', x) or x == ('not', y):    # complement: a & ~a = 0
            return 0
    if op == 'or':
        if x == 0: return y                       # identity:   0 | y = y
        if y == 0: return x                       # identity:   y | 0 = y
        if x == 1 or y == 1: return 1             # domination: x | 1 = 1
        if x == y: return x                       # idempotent: x | x = x
        if y == ('not', x) or x == ('not', y):    # complement: a | ~a = 1
            return 1
    return e

Each line is a law you can name. 1 & y = y is identity; x & 0 = 0 is domination; x | x = x is idempotence; a & ~a = 0 and a | ~a = 1 are the complement laws; ~~a = a is double negation (derivable from the complement and De Morgan laws). No rule here is invented — each is a theorem of §13.5, so each rewrite is sound for every assignment of the variables.

⚠️ Common Pitfall: A rewrite rule that is not a law would silently corrupt the circuit. For instance, "simplify" $a \vee (b \wedge c)$ to $(a \vee b) \wedge c$ looks plausible but is false — the real distributive law is $a \vee (b \wedge c) = (a \vee b) \wedge (a \vee c)$, with $a$ appearing in both factors. Dropping the second $a$ changes the function. Every rule you add must be a named law (or provably derived from them); "looks right" is exactly what proof exists to replace.

Phase 3: Compose into a recursive fixpoint simplifier

simplify_node only fires at the top of a tree. To simplify everywhere, recurse into children first (bottom-up), then apply rules at the current node, and repeat until nothing changes (a fixpoint).

def simplify(e):
    """Fully simplify by rewriting bottom-up to a fixpoint."""
    if not isinstance(e, tuple):
        return e
    if e[0] == 'not':
        e = ('not', simplify(e[1]))
    else:
        e = (e[0], simplify(e[1]), simplify(e[2]))
    new = simplify_node(e)
    return simplify(new) if new != e else new

print(show(simplify(enable)))
# Expected output:
# (((a & b) | ((a & b) & c)) | a)

Hand-trace the collapse, bottom-up. Two subterms simplify by the rules we have:

$a \wedge \overline{a}$ → $0$ by the complement law.
$a \wedge 1$ → $a$ by the identity law.
The $0$ then disappears: $X \vee 0 = X$ by identity.

After those, the expression is $(a \wedge b) \vee \big((a \wedge b) \wedge c\big) \vee a$ — and there our tool stops. None of its rules (identity, domination, idempotence, complement) matches an OR of two different terms, so the three remaining terms cannot be combined. The printed result is (((a & b) | ((a & b) & c)) | a) — still several gates, where the true answer is one wire.

But a human sees more. The law that combines those terms is absorption: $(a \wedge b) \vee \big((a \wedge b) \wedge c\big) = a \wedge b$ (treat $a \wedge b$ as one element $u$: $u \vee (u \wedge c) = u$), and then $(a \wedge b) \vee a = a$ (since $a \vee (a \wedge b) = a$). So the true minimum is the bare wire $a$.

🐛 Find the Error (a real gap in our tool). Our printed output, (((a & b) | ((a & b) & c)) | a), is correct but not minimal — the true minimum is a. The simplifier is sound but not complete: every rewrite it makes is valid, so it never returns a wrong circuit, but it lacks the absorption rule, so it halts with gates it could have deleted. This is the honest situation for every real simplifier: soundness (never wrong) is mandatory; completeness (always minimal) is an aspiration. Let's add absorption and watch it finish the job.

def absorb(e):
    """Add the absorption laws:  x | (x & y) = x   and   x & (x | y) = x
    (and their commuted forms). Section 13.5, proved from identity +
    distributive + domination."""
    if not isinstance(e, tuple) or e[0] == 'not':
        return e
    op, x, y = e
    def is_and(t): return isinstance(t, tuple) and t[0] == 'and'
    def is_or(t):  return isinstance(t, tuple) and t[0] == 'or'
    if op == 'or':                          # x | (x & y) = x
        for a, b in ((x, y), (y, x)):
            if is_and(b) and a in (b[1], b[2]):
                return a
    if op == 'and':                         # x & (x | y) = x
        for a, b in ((x, y), (y, x)):
            if is_or(b) and a in (b[1], b[2]):
                return a
    return e

Now fold absorb into the node-level pass so the fixpoint loop applies it too:

def simplify_node_v2(e):
    return absorb(simplify_node(e))

def simplify_v2(e):
    if not isinstance(e, tuple):
        return e
    if e[0] == 'not':
        e = ('not', simplify_v2(e[1]))
    else:
        e = (e[0], simplify_v2(e[1]), simplify_v2(e[2]))
    new = simplify_node_v2(e)
    return simplify_v2(new) if new != e else new

print(show(simplify_v2(enable)))
# Expected output:
# a

The whole 9-gate expression collapses to the bare wire a. Every step was a named law, so the result is guaranteed to compute the same function as the original on all inputs — we never tested our way to it.

🚪 Threshold Concept. Watch what absorption did to the circuit: $a \vee (a \wedge b) = a$ means an OR gate and an AND gate were deleted and replaced by a wire carrying $a$ — and §13.5 guarantees identical behavior on every one of the inputs. That is the entire business model of logic synthesis: the eight law-pairs are theorems, so a tool can delete gates by the million and prove it changed nothing observable. The algebra is the optimizer.

Phase 4: Verify against the truth table (theme four)

We proved each rewrite sound, but did we implement the rules correctly? A typo (e.g. returning the wrong branch) could make simplify_v2 produce a non-equivalent expression. So we check behavioral equivalence the brute-force way: evaluate the original and the simplified expression on every assignment of the variables and confirm they always agree. For 3 variables that's $2^3 = 8$ rows — an exhaustive check.

def evaluate(e, env):
    """Evaluate an expression tree under env = {var: 0/1}."""
    if e in (0, 1): return e
    if isinstance(e, str): return env[e]
    if e[0] == 'not': return 1 - evaluate(e[1], env)
    a, b = evaluate(e[1], env), evaluate(e[2], env)
    return (a & b) if e[0] == 'and' else (a | b)

def equivalent(e1, e2, variables):
    """True iff e1 and e2 agree on every assignment (exhaustive)."""
    n = len(variables)
    for bits in range(2 ** n):
        env = {v: (bits >> i) & 1 for i, v in enumerate(variables)}
        if evaluate(e1, env) != evaluate(e2, env):
            return False, env
    return True, None

print(equivalent(enable, simplify_v2(enable), ['a', 'b', 'c']))
# Expected output:
# (True, None)

Hand-verify a couple of rows. The original enable on $a=1, b=0, c=0$: $(1\wedge0)\vee(\dots)\vee (1\wedge\overline1)\vee(1\wedge1) = 0 \vee 0 \vee 0 \vee 1 = 1$; the simplified `a` is $1$. Agree. On $a=0, b=1, c=1$: original $= (0)\vee(0)\vee(0\wedge1)\vee(0) = 0$; simplified a $= 0$. Agree. The function checks all 8 rows and finds no disagreement, returning (True, None).

💡 Intuition: This is the chapter's theme four, executable. The laws guarantee the rewrite is correct on the infinitely many Boolean algebras where it could be applied; the truth-table test guarantees we coded the laws correctly on this concrete two-element algebra. Because 3 variables give only 8 rows, the test here is exhaustive — for this expression it is as good as a proof of behavioral equality, and it would instantly catch a mis-implemented rule.

⚠️ Common Pitfall: Exhaustive checking is only feasible for few variables: $n$ variables need $2^n$ rows, so 30 inputs is already a billion. This is exactly why hardware verification cannot rely on truth tables alone and leans on the algebra (and more advanced methods like BDDs and SAT). The $2^n$ blow-up is the same exponential you met counting subsets in Chapter 8 — and it is the reason proof, not enumeration, is the scalable tool.

Discussion Questions

Our simplifier is sound (never returns a non-equivalent expression) but was not complete until we added absorption — and it still isn't fully complete (no simplifier using a fixed rule set is, in general). Give a small expression that simplify_v2 still fails to fully minimize, and name a law it would need.
The equivalent check is exhaustive for 3 variables (8 rows) but infeasible for 30. Explain, using the $2^n$ growth, why this pushes industrial tools toward algebraic and symbolic methods. Which chapter concept is the $2^n$?
We justified ~~a = a (double negation) as "derivable from complement and De Morgan." Sketch the derivation: starting from $a \vee \overline{a} = 1$ and $a \wedge \overline{a} = 0$, argue that $\overline{\overline{a}} = a$ (uniqueness of complements).
Phase 2 warned that "simplifying" $a \vee (b \wedge c)$ to $(a \vee b) \wedge c$ is wrong. Use a single truth-table row (one assignment of $a, b, c$) to prove the two expressions are not equivalent, and state the correct distributive law.

Your Turn: Extensions

Option A (gate counter + report). Write gate_count(e) that counts internal nodes (gates) in an expression tree, and print "before → after" for enable (9 gates → 0 gates: a bare wire). Then run it on three expressions of your own and report the reduction. This is the metric a synthesis tool optimizes.
Option B (De Morgan normalizer). Add a rewrite that pushes not inward using De Morgan's laws ($\overline{a \wedge b} = \overline a \vee \overline b$ and dually), reaching a form where complements sit only on variables (negation normal form). Verify with equivalent that your normalizer preserves behavior on a few expressions you write out.
Option C (random differential test). Generate small random expression trees (by hand, a dozen of them), simplify each, and confirm equivalent returns (True, ...) for every one. Explain what a single (False, env) would tell you — not that a law is wrong, but that your implementation of a law has a bug — and why the returned env is the witness that localizes it.

Key Takeaways

The Boolean laws are an optimizer. Every simplification the tool performs is a named law from §13.5, so each gate it deletes provably preserves the circuit's output on all inputs — exactly what §13.6 promised.
Soundness is mandatory; completeness is hard. A rewrite engine must never produce a non-equivalent result (soundness); reaching the true minimum (completeness) requires ever more rules and is generally unattainable with a fixed set.
Build with proof, verify with computation. The laws certify the rewrites for all inputs; the exhaustive truth-table check certifies that we coded the laws correctly — theme four, with both halves doing work neither could do alone.
Enumeration doesn't scale; algebra does. Truth-table checking is $2^n$ and dies past a few dozen inputs — the same exponential as counting subsets (Chapter 8) — which is precisely why real synthesis relies on the algebraic laws being theorems.