Circuits as Boolean functions

Every combinational circuit computes a Boolean function. Take a door controller for a lab with a badge reader: the door unlocks when a valid badge is presented and either it is office hours or the badge belongs to an administrator. With inputs b (valid badge), t (office hours) and a (admin),

unlock = b · (t + a)

where · is AND and + is OR. A second engineer implements the same rule differently:

unlock₂ = (b · t) + (b · a)

Are they the same? For three inputs we can simply build a truth table:

All eight rows agree, so the two are equivalent — which also follows directly from the distributive law x·(y+z) = x·y + x·z. Truth tables, however, double in size with each input: 64 inputs means 1.8 × 10¹⁹ rows. Engines therefore never build them explicitly.

The laws engines rely on

The miter: turning equivalence into one question

To check whether two circuits compute the same function, connect the same inputs to both, XOR their outputs and ask: "can this XOR ever be 1?" This construction is called a miter. If the answer is "no", the circuits are equivalent; if "yes", the tool hands you the input values that make them differ.

The same idea can be written as an assertion and handed to any FPV tool:

// door_unlock_miter.sv — prove two implementations are equivalent
module door_unlock_miter (
  input logic b,   // valid badge
  input logic t,   // office hours
  input logic a    // administrator
);
  logic unlock_1, unlock_2;

  assign unlock_1 = b & (t | a);
  assign unlock_2 = (b & t) | (b & a);

  // Immediate assertion: checked for every combination of b, t, a
  always_comb a_same: assert (unlock_1 == unlock_2);
endmodule