// 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