Lesson 5.2 · Exploring New RTL with Formal

The example: a 4-floor lift controller

Our design controls a lift in a four-storey building. It is small enough to read in one sitting but has the sequential, decision-heavy behaviour where formal shines.

Specification (informal, as designers usually get it)

Each floor has a call button call[f]. A press is remembered in pending[f] until that floor is served.
The lift moves one floor per MOVE step and never moves with the door open.
When the lift is at a floor with a pending call, it opens the door for DOOR_CYCLES cycles. That serves the call.
The lift keeps its direction while there are calls ahead of it, then reverses (the classic "elevator algorithm").
Every call is eventually served.

lift_ctrl.sv

// lift_ctrl.sv — 4-floor lift controller
// ANTI_STARVE = 0 reproduces the first version of the design (see lesson 5.6).
module lift_ctrl #(
  parameter int DOOR_CYCLES = 3,
  parameter bit ANTI_STARVE = 1'b1
) (
  input  logic       clk,
  input  logic       rst,
  input  logic [3:0] call,        // floor call buttons
  output logic [1:0] floor,       // current floor
  output logic       door_open,
  output logic       moving,
  output logic       dir_up,      // direction of travel
  output logic [3:0] pending      // remembered calls
);
  typedef enum logic [1:0] {IDLE, MOVE, DOOR} state_t;
  state_t     state;
  logic [1:0] door_cnt;
  logic       served_here;        // door just closed at this floor
  logic [3:0] above, below;       // pending calls above / below the lift

  always_comb begin
    above = '0;
    below = '0;
    for (int f = 0; f < 4; f++) begin
      if (f > int'(floor)) above[f] = pending[f];
      if (f < int'(floor)) below[f] = pending[f];
    end
  end

  always_ff @(posedge clk) begin
    if (rst) begin
      state       <= IDLE;
      floor       <= 2'd0;
      door_cnt    <= 2'd0;
      dir_up      <= 1'b1;
      pending     <= 4'd0;
      served_here <= 1'b0;
    end else begin
      pending <= pending | call;                    // remember new calls
      case (state)
        IDLE: begin
          if ((pending[floor] || call[floor]) &&
              !(ANTI_STARVE && served_here && (|above || |below))) begin
            state          <= DOOR;                  // serve this floor
            door_cnt       <= 2'(DOOR_CYCLES - 1);
            pending[floor] <= 1'b0;
          end else if (|above || |below) begin
            if (!(dir_up ? |above : |below))
              dir_up <= !dir_up;                     // nothing ahead: reverse
            state       <= MOVE;
            served_here <= 1'b0;
          end
        end
        MOVE: begin
          floor <= dir_up ? floor + 2'd1 : floor - 2'd1;
          state <= IDLE;                             // arrive, then decide
        end
        DOOR: begin
          pending[floor] <= 1'b0;                    // presses here are served now
          if (door_cnt == 2'd0) begin
            state       <= IDLE;
            served_here <= 1'b1;
          end else begin
            door_cnt <= door_cnt - 2'd1;
          end
        end
        default: state <= IDLE;
      endcase
    end
  end

  assign door_open = (state == DOOR);
  assign moving    = (state == MOVE);
endmodule