// lift_ctrl_fv.sv — exploration wrapper for the lift controller
module lift_ctrl_fv #(
  parameter bit ANTI_STARVE = 1'b1
) (
  input logic       clk,
  input logic       rst,
  input logic [3:0] call
);
  logic [1:0] floor;
  logic       door_open, moving, dir_up;
  logic [3:0] pending;

  lift_ctrl #(.DOOR_CYCLES(3), .ANTI_STARVE(ANTI_STARVE)) dut (.*);

  initial assume (rst);
  default clocking cb @(posedge clk); endclocking
  default disable iff (rst);

  // ------------------------------------------------ exploration covers
  c_door_at_3:  cover property (door_open && floor == 2'd3);
  c_round_trip: cover property (door_open && floor == 2'd3 ##[1:$] door_open && floor == 2'd0);
  c_pass_by:    cover property (moving && floor == 2'd1 ##1 floor == 2'd2 && !door_open
                                ##1 moving);   // passes floor 2 without stopping
  c_reverse:    cover property (moving && dir_up ##[1:$] moving && !dir_up);

  // ------------------------------------------------ safety
  a_door_not_moving: assert property (moving |-> !door_open);
  a_no_wrap:         assert property (moving |-> (dir_up ? floor != 2'd3 : floor != 2'd0));
  a_one_floor:       assert property (moving |=> floor == ($past(dir_up) ? $past(floor) + 2'd1
                                                                         : $past(floor) - 2'd1));
  a_open_for_call:   assert property ($rose(door_open) |-> $past(pending[floor] || call[floor]));

  for (genvar f = 0; f < 4; f++) begin : g_floor
    // a call is only forgotten when it is served
    a_clear_served: assert property ($fell(pending[f]) |-> door_open && floor == 2'(f));
    // ------------------------------------------------ liveness
    a_served:       assert property (pending[f] |-> s_eventually (door_open && floor == 2'(f)));
  end
endmodule