Digital Circuit Verification

Intro to Proofs · Axiom Academy

Proving a Circuit Can't Be Wrong A voting machine confirms your vote only when the logic is exactly right — and a truth table can prove it works for every possible input. You're designing the "Vote Confirm" logic for a voting machine. A single wrong combination of inputs could miscount a vote — so "we tested it" isn't enough. You need to prove it's right for every input. Turn the requirement into a circuit The spec is a sentence; a circuit is wires and gates. Flip the four inputs and watch the signal flow — the lamp confirms the vote only when the logic says it should. the voter is authenticated ( A ), and the ballot is complete ( B ), and the voter pressed confirm ( C ) or the timer expired ( T ) Check every possible input — all 16 Four yes/no inputs make exactly 2⁴ = 16 combinations. Walk the dial through all of them: when every row matches the spec, you haven't just tested the circuit — you've proven it. That's proof by exhaustion. Could a simpler formula do the job? Three formulas were proposed for the spec. Only one is right. Pick each one — the verifier hunts for an input where it disagrees with the requirement, and shows you exactly how that bug would let a bad vote through. A truth table is a proof by exhaustion : check all the cases and you've covered every case there is. The same logic certifies aircraft flight controls , pacemaker timing , and bank authentication — anywhere "it usually works" isn't good enough, you prove it works for every input.

This is the written version of the interactive lesson above. See the full Intro to Proofs course.